Bend BankSource code

Break this bank.

The private note of the account company holds a secret flag. Read it, read any other account, or make one credit appear or vanish. All the code is open.

Open an account

Log in

Proven laws

  • Privacy. Only you can see your account. Others learn only that it exists, and what you send them.
  • Access. Only your name and your own key open your account.
  • Authority. No one else can take money from your account or change its key, note or loan. Others can only pay into it.
  • Escrow. Money you lock for someone leaves the lock only to them, when you release it, or back to you, when they refund it.
  • Split payments. A payment to several people pays each one exactly, or no one.
  • Loans. Up to 1,000, at 10% rounded up, due in 10 minutes. Each payment lowers the debt by exactly its amount. A late loan can't be repaid, and you can't borrow again.
  • Conservation. There are exactly 1,000,000,000 credits. No request creates or destroys one, and no balance goes below zero.
  • New accounts. Each gets 100 credits and a 1,000 credit line from the vault. Nothing else touches the vault.
  • Atomicity. A request that fails changes nothing.
  • Totality. Web.serve answers every request: Bend accepts only code that always finishes.

Each law is a theorem about Web.serve, the Bend function that answers every request here: LAWS.bend states them, proof/ proves them, and bend PROOF.bend --verdict checks the proofs with a kernel that is itself proven in Lean.