mcpython¶

A sound, non-executing crash verifier for type-annotated Python. It lowers your functions to SMT and either finds a crash with the input that triggers it, or proves the crash cannot happen — without running your code.

The guarantee it is built around is that it never lies in either direction: no false crash, no false proof. Anything it cannot model exactly is reported as unverified, never as a clean bill of health.

def share_of(amount: int, total: int) -> int:
    return 100 * amount // total

CRASHES — 1, each with an input that triggers it
  checkout.py:2: share_of: ZeroDivisionError: integer division or modulo by zero
      reproduce: share_of(0, 0)

Start here¶

Tutorial — eight steps from a first crash to a proven security invariant. Every command on the page is executed on each release.
Getting started — install it, run it, and read the report.
Harness API — @proof, any_*, assume, invariant, @requires / @ensures.
Tiers and guarantees — what each mode proves, what is modeled, and how soundness is tested rather than asserted.

What makes it different¶

It does not execute your code. No fixtures, no fuzzing budget, no flaky reruns.
Every crash comes with a witness. The reproduce: line raises when you paste it into a REPL.
Every proof covers all inputs at once, not a sample of them.
The coverage number counts your whole codebase, and every function it cannot decide names an owner — you, or a modeling feature mcpython still owes you.