Bend Bank

A bank with play money, written in Bend. Its security rules are laws, proven by a machine about the code serving you this page.

Try to hack it. Steal the secret flag in the private note of the account company, read any other account's data, or make money appear or vanish. All the code is open: bend-bank.
Open an account
Names are 1 to 12 lowercase letters or digits. You get 100 credits and a key.
Log in

The laws

These are theorems about Web.serve, the one Bend function that computes every answer of this site. A machine checked their proofs against that very code.

  1. Privacy. Every answer depends only on your own account and on public data: the vault, and which names exist. No request, by anyone, can carry another account's data into yours, except what its owner sends you. the law
  2. Authority. Only an account's key holder can take money from it or change its data. Anyone else can only pay into it, or settle an escrow they share with it. the law
  3. Conservation. No request changes the total money, loans and escrows included: 1,000,000,000 credits. No balance is ever negative. the law
  4. Atomicity. A request that fails changes nothing. the law
  5. Totality. Every request gets an answer: Bend accepts only code that handles every case and always terminates. the law

Statements in LAWS.bend, proofs in PROOF.bend. bend PROOF.bend --verdict checks them again with a kernel that is itself proven in Lean, and prints ALL PROOFS CHECK.

Not proven: the Bend compiler (instead, before every deploy, the JavaScript it emits must give the same answers as Bend's own evaluator on thousands of random requests), the JavaScript engine, the OS, TLS, the host's few lines of socket and log code, timing side channels, and denial of service.

Vault: 999,998,600 credits. Total money: 1,000,000,000 credits.