Tutorial: from a crash to a security proof¶
This tutorial walks the whole of mcpython in eight steps. Each step is one small file and one command, and each adds exactly one idea to the step before it. By the end you will have found real bugs, proven that a fix is complete, taught the verifier what to assume, and proven a security invariant that holds for strings of any length.
Every command and every block of output on this page is executed on each release. If you can read it here, it ran.
Before you start¶
You need mcpython on your PATH. From a checkout:
Work in an empty directory; each step writes one file into examples/.
Step 1 — Find a crash without running anything¶
Here are two functions from a checkout service. Both are ordinary. Both crash.
"""Step 1 — crashes, found with zero annotation.
Two functions from a checkout service. Both look fine. Both crash.
"""
def share_of(amount: int, total: int) -> int:
"""What percentage of `total` is `amount`?"""
return 100 * amount // total
def cheapest(prices: list) -> int:
"""The lowest price in a sorted list."""
return prices[0]
You get a file:line, the exception, and an input that produces it:
No test was written, no code was executed, and nothing was guessed. mcpython lowered each function to a logical formula and asked a solver for an input that reaches a division by zero. The reproduce: line is that input — paste it into a REPL and it raises. The exit code is 1, so this fails a CI gate.
The idea: a crash is only reported with a witness, so a false alarm is not possible.
Step 2 — Prove the fix is complete¶
Guard both functions and ask again.
"""Step 2 — the same code, guarded, and proven crash-free.
A proof here means: for *every* int and *every* list the annotations allow,
these functions do not raise. Not "we tried a thousand inputs".
"""
def share_of(amount: int, total: int) -> int:
"""What percentage of `total` is `amount`?"""
if total == 0:
return 0
return 100 * amount // total
def cheapest(prices: list) -> int:
"""The lowest price in a sorted list."""
if len(prices) == 0:
return 0
return prices[0]
This is the part a test suite cannot give you. "Proven crash-free" is not "we tried a thousand inputs and none of them broke" — it is a statement about every int and every list. A test suite that misses the empty list stays green; a proof that misses it cannot exist.
The idea: the interesting output is not the crash list, it is the proof list.
Step 3 — Read what it refuses to say¶
Real code is full of things a verifier cannot model. Here is what happens when it hits them.
"""Step 3 — what mcpython does when it *cannot* decide.
Nothing here is proven and nothing is reported as a crash. Each function is
listed as unverified, with an owner: something you can do, or something
mcpython still owes you.
"""
import re
def slugify(name: str) -> str:
"""External call — the body of `re.sub` is not available to the verifier."""
return re.sub(r"\W+", "-", name)
def unique_skus(rows: list) -> int:
"""Method calls on an object mcpython does not model yet."""
seen = set()
for row in rows:
seen.add(row)
return len(seen)
def channel_of(kind: str) -> str:
"""`match`/`case` is not modeled yet."""
match kind:
case "web":
return "online"
case _:
return "offline"
Nothing is proven and nothing is reported as a crash. That "NO claim" line is deliberate: "no crashes found" would be a lie about code that was never modeled.
Look at how the gap is split. Every unverified function has an owner:
Your move is something you can act on today — a flag, an annotation, a harness. mcpython owes you is a modeling feature it does not have yet, ranked by how much coverage it would buy. The report is a burn-down list, not a grade.
The idea: the number counts your whole codebase, and every function missing from it names who can move it.
Step 4 — Buy coverage with an explicit caveat¶
The most common blocker on real code is a single call whose body is not available.
"""Step 4 — trading a little strength for a lot of coverage.
`.strip()` and `.upper()` are calls whose bodies mcpython cannot see, so the
default (sound) run decides nothing here. Run it with --conditional and the
verifier assumes those calls return normally — which decides both functions,
under a caveat that the report states.
"""
def normalize_sku(raw: str) -> str:
return raw.strip().upper()
def normalize_city(raw: str) -> str:
return raw.strip().title()
The default run decides nothing here, but it tells you a flag would:
Take the trade:
Coverage went from 0% to 100% — and every claim it bought is marked:
The idea: a weaker guarantee is fine as long as the report says which one you are getting.
Step 5 — Prove a property, not just the absence of a crash¶
Crash-freedom is a low bar. def clamp_quantity(...): return 0 never crashes either.
A proof harness looks like a unit test and is never executed. any_int() is a symbolic input the proof quantifies over, assume(...) narrows it, and the assert is the property.
"""Step 5 — proving a property, not just the absence of a crash.
The auto-scan already proves `clamp_quantity` cannot crash. That says nothing
about whether it is *right*: a body of `return 0` would be just as crash-free.
A proof harness states the property you actually care about, and proves it for
every input the assumptions admit.
"""
from mcpython.harness import any_int, assume, proof
def clamp_quantity(qty: int, stock: int) -> int:
"""Never sell more than we have."""
if qty < 0:
raise ValueError(f"negative quantity: {qty}")
if qty > stock:
return stock
return qty
@proof
def never_oversells() -> None:
qty = any_int()
stock = any_int()
assume(qty >= 0)
assume(stock >= 0)
assert clamp_quantity(qty, stock) <= stock
@proof
def keeps_what_it_can() -> None:
qty = any_int()
stock = any_int()
assume(0 <= qty <= stock)
assert clamp_quantity(qty, stock) == qty
Two things in that report are worth pausing on. It repeats your assumptions back to you, and it says how much of the target it actually reached:
Five of six, because assume(qty >= 0) excludes the reject path — the harness working as intended. Nothing in the engine can tell a well-chosen assumption from one that quietly assumes the bug away, so it reports what it can: what you assumed, and how far it got. That is the boundary of the claim, printed next to the claim.
Writing a harness also credits the functions it verified toward the coverage number. A score that refused to count your work would earn no second harness.
The idea: you say what "correct" means; mcpython proves it for every input at once.
Step 6 — Prove a loop, for any number of iterations¶
Loops are where bounded checkers give up and start unrolling. An invariant turns the loop into an induction proof instead: it must hold on entry, survive one iteration, and after the loop you may rely on it together with the negated guard.
"""Step 6 — proving a loop, for any number of iterations.
An `invariant` turns a loop into an induction proof: it must hold on entry,
be preserved by one iteration, and after the loop you may rely on it together
with the negated guard. No unrolling, no bound on `n`.
"""
from mcpython.harness import any_int, assume, invariant, proof
@proof
def counting_lines_is_exact() -> None:
n = any_int()
assume(0 <= n <= 1000)
i = 0
counted = 0
while i < n:
invariant(0 <= i <= n)
invariant(counted == i)
counted = counted + 1
i = i + 1
assert counted == n
The loop body was analysed once, not a thousand times. The proof holds for every n the assumption admits, and the cost does not grow with n.
(The headline reads 0 of 0 functions here: the file contains only a harness, and a harness is not something the ledger asks you to verify.)
The idea: one invariant replaces unbounded unrolling.
Step 7 — Make verification scale with contracts¶
So far every call was inlined. That does not scale, and it stops entirely at a body mcpython cannot model. A contract breaks the dependency: verify the function once against its @requires and @ensures, and every call site afterwards reasons about the contract instead of the body.
"""Step 7 — contracts, so verification scales past one function.
Verify `validate_quantity` once against its contract; every caller then
reasons about the *contract* instead of the body. The bug in `reserve` is
found at the call site, without re-verifying the callee.
"""
from mcpython.harness import ensures, requires
@requires(lambda qty: 1 <= qty <= 1000)
@ensures(lambda qty, result: result == qty)
def validate_quantity(qty: int) -> int:
if qty < 1 or qty > 1000:
raise ValueError("quantity out of range")
return qty
def reserve(qty: int) -> int:
"""Forgot to guard `qty` before handing it over."""
return validate_quantity(qty)
The callee is proven against its contract once:
And the caller's missing guard is a crash at the call site, with a witness:
reserve(0) really raises: unlike an assumption made inside the verifier, @requires is checked at runtime too, so a contract violation is a real, replayable bug rather than a modeling artefact.
A call now costs the same whether the callee is three lines or three hundred — and a callee whose body cannot be modeled at all can still carry its callers, once its contract is proven.
The idea: verify once, then reason about the contract everywhere.
Step 8 — Prove a security invariant¶
Everything so far reasoned about numbers and lengths. For a validator, the property that matters is about characters: can anything bad get through?
s[i] is a character and ord(s[i]) is its code point, and two reads at the same index agree — which is exactly what an invariant needs in order to talk about "the character at position i".
The proof below is the contrapositive of "if it returns, the string was clean": assume the string has a control character somewhere, and prove the scan cannot reach the end.
"""Step 8 — proving a security invariant.
`s[i]` is a character, and `ord(s[i])` its code point; two reads at the same
index agree. That is what lets an invariant reason about "the character at
position i", and it turns a scan into a proof that no control character can
ever get past it — for strings of any length, with no quantifier.
The harness restates the scan rather than calling `reject_control_chars`: an
invariant has to sit in the loop the proof walks, and passing a string into an
inlined callee is a limitation mcpython still owes you.
"""
from mcpython.harness import any_int, any_str, assume, invariant, proof
def reject_control_chars(sku: str) -> None:
"""Return normally only if `sku` is free of control characters."""
i = 0
while i < len(sku):
if ord(sku[i]) < 0x20 or ord(sku[i]) == 0x7F:
return
i = i + 1
@proof
def a_control_char_is_always_caught() -> None:
sku = any_str()
bad = any_int()
assume(0 <= bad < len(sku))
assume(ord(sku[bad]) < 0x20)
i = 0
while i < len(sku):
invariant(0 <= i <= bad)
if ord(sku[i]) < 0x20 or ord(sku[i]) == 0x7F:
return
i = i + 1
assert False
assert False is proven unreachable: no string containing a control character can survive the scan. The invariant 0 <= i <= bad is inductive precisely because reaching i == bad forces the guard to fire. There is no quantifier and no bound on the length of the string.
The idea: a validator's real property is a security invariant, and it is provable.
Does the proof actually mean anything?¶
A proof is only worth as much as its ability to refuse. Take the same scan, aim the assumption at DEL (0x7F) instead of the low control characters, and delete the 0x7F check — the classic off-by-one in a character allow-list.
sed -e 's/assume(ord(sku\[bad\]) < 0x20)/assume(ord(sku[bad]) == 0x7F)/' \
-e 's/ or ord(sku\[i\]) == 0x7F//' \
examples/08-security.py > examples/08-broken.py
mcpython check examples/08-broken.py
It does not prove it. The hole is exactly the one the check was there to close, and the verifier declines to bless it. Put the 0x7F check back and the same proof goes through — so the ✓ in the previous step was load-bearing, not decoration.
The whole set¶
Point mcpython at the directory and you get the ledger for all eight files at once:
Fifty-four percent, with three crashes, four proofs, four proven harnesses, and an owner on every remaining line. That is the shape of a real run: not a grade, a work list.
Where to go next¶
- Getting started — installation and the report format in detail.
- The harness API — the full reference for
@proof,any_*,assume,invariant,@requiresand@ensures. - Tiers and guarantees — exactly what each tier proves, what is modeled today, and how soundness is tested rather than asserted.