Prove it, don't
just test it.

A bug every web dev has shipped, caught by a compiler that refuses to make human assumptions — and pinned to the real code that ships.

Press → to break something.

The transfer function everyone writes

function withdraw(balance, amount) {
  if (amount <= balance)
    return balance - amount;
  return balance;
}

State the property for every input

-- a withdrawal never grows your balance:
theorem never_grows (balance amount : Int) :
    withdraw balance amount ≤ balance

No test values. balance and amount are variables over all integers — infinitely many pairs, one claim.

#eval withdraw 0 (-50)
50          ← a zero balance became £50. Alice stole money.

The proof fails — and names the bug's address

$ lean Mini.lean
error: omega could not prove the goal:
  a possible counterexample may satisfy:
    b ≤ -1        ← the amount is NEGATIVE
  where a := balance,  b := amount

Nobody typed −£50 as a test case. The failed proof derived that negative amounts are exactly where it breaks.

A failing test says "this one input broke". A rejected proof says the shape of every breaking input — which is why the fix is mechanical.

Add what the human assumed

def withdraw (balance amount : Int) : Int :=
  if 0 ≤ amount ∧ amount ≤ balance
     then balance - amount else balance
-- theorem unchanged:
theorem never_grows ... := by
  unfold withdraw; split <;> omega

$ lean Mini.lean
✓ no output — silence IS the proof
#print axioms never_grows
[propext, Quot.sound]  ← no sorry: no fake proof

The upload guard in the Moss app

if (abs.startsWith(UPLOAD_DIR)) // looks fine

-- careless guard accepts?
true
-- where does it really resolve?
["srv", ".ssh", "id_rsa"]   ← OUT of the vault
-- the shipped guard (resolve FIRST)?
false   ✓ rejected

Shout a filename. Whatever you say — the theorem already covers it.

Every path of length ≤ 4, exhaustively

All six escapes share one shape: a .. right after the managed prefix — the exact condition the proof isolates. We never picked them.

The sweep is exhaustive for the slice. The theorem is what covers the infinity beyond it — by induction, not enumeration.

Same witness, two worlds

✔ accepts a real file inside the managed dir
✔ rejects the Lean counterexample (mid-path ..)
✔ rejects sibling dir "moss-uploads-evil"
✔ rejects missing files, relative, empty
ℹ pass 4 · fail 0

Lean turns "is this safe?" into "is my model faithful?" — a small, attackable question instead of a vibe.

It's one file, not a research project

$ curl https://elan.lean-lang.org/elan-init.sh -sSf | sh   # toolchain
$ lean Mini.lean                                        # 9 lines, seconds
- run: (cd proofs && lake build)   # one line, next to node --test

Unit tests check what you imagined.
Proofs check what's possible.

Proofs: moss/proofs/Uploads.lean · pinned by uploads.test.js — Moss 🪨