Skip to content

Getting started

Install

uv sync

Python 3.13 (the project's .venv). A bare python on this machine may be a different version — always go through uv run.

Your first run

Create example.py:

def average(total: int, count: int) -> int:
    return total // count


def port_of(config: dict) -> int:
    return config["port"]


def first(items: list) -> int:
    return items[0]

Run it:

uv run mcpython check example.py

VERIFIED — 3 of 3 functions (100%)

CRASHES — 3, each with an input that triggers it
  example.py:2: average: ZeroDivisionError: integer division or modulo by zero
      reproduce: average(0, 0)
  example.py:6: port_of: KeyError: 'port'
      reproduce: port_of({})
  example.py:10: first: IndexError: list index out of range
      reproduce: first([])

Every reproducer is a real crash — paste average(0, 0) into a REPL and it raises. Exit code is 1 (a crash was proven), so this fails a CI gate.

Reading the report

The report is a ledger — every function lands in exactly one bucket, and the headline is VERIFIED — n of N, the fraction of the whole codebase mcpython could decide. On a toy file that's 100%; on real code it starts low and you drive it up.

Four sections, in order:

  1. VERIFIED — n of N (p%) — the headline. The goal is 100%.
  2. CRASHES — the findings, each with a file:line and a reproducer.
  3. The proofs — the product. Functions proven crash-free (for every input their types allow), proven against a contract, or proven by one of your @proof harnesses. All are named, so you can check them against what you believed.
  4. UNVERIFIED — n of N — a burn-down of what's left, ranked, with an owner on every line: YOUR MOVE (a flag or an annotation you can add) versus MCPYTHON OWES YOU (a modeling feature it doesn't have yet). This is the part that makes the number a plan instead of a grade.

mcpython makes NO claim about the unverified functions — that line is deliberate. "No crashes found" is not "your code is safe" when most of the code wasn't modeled, and the report never lets those be confused.

The flags

Flag Effect
--conditional Also decide functions whose only blocker is an external call, assuming those calls return normally. Verdicts are tagged CONDITIONAL. Strictly more coverage, weaker guarantee.
--json Per-function detail as JSON (status, reason, reproducer, contract, targets). For tooling and AI agents.
-d / -dd / -ddd Trace the analysis to stderr (the report stays clean on stdout). -d: each verdict with file:line. -dd: parameter models, branches taken, each obligation discharged, and the actual SMT query (SAT/UNSAT + serialized formula). -ddd: also the inconclusive functions and why. The trace never changes a verdict.

Going further

The default run finds crashes and proves what it can with zero annotation. To prove real properties — "this validator returns its input unchanged for every valid port", "this scan rejects every control character" — or to make verification scale across a codebase, you write a few lines using mcpython.harness. See harness-api.md.