Skip to content

Tiers, guarantees, and how soundness is enforced

The cardinal guarantee

mcpython makes zero false verdicts:

  • No false crash. A crash is reported only with a concrete counterexample reached through operations modeled exactly. If it says a function crashes, the reproducer raises.
  • No false proof. A function is called crash-free (or a property proven) only when every relevant path was fully modeled under the stated assumptions.
  • Honest silence. Anything it can't model precisely — an unknown type, an unmodeled call, dynamic magic — is Inconclusive, never a crash and never a proof. It parses everything and rejects nothing.

Coverage grows only by modeling more, never by relaxing this.

The four tiers

Tier Invoked by Guarantee Caveat
Default (sound) mcpython check Sound and precise. A crash reproduces; a proof holds for every input the types allow. —
Conditional (stub) --conditional Sound modulo external calls: an opaque call is replaced by any(return_type), assumed to succeed. Verdicts tagged CONDITIONAL. Holds only if those calls return normally.
Proof harness a @proof function Sound and precise. Proves a real property for every input the assumes admit — no external-call caveat; targets are inlined and run. The claim is bounded by your assumptions (reported verbatim, with reach).
Contract @requires / @ensures Sound and precise. The function meets its contract for every admitted input; call sites reason about the contract. int/bool params. --conditional can take an unproven contract on trust (then CONDITIONAL).

The tiers compose: a @proof harness can call contracted functions; --conditional layers onto any of them.

Why "conditional" exists

On real code, most functions are blocked by a single external call whose body isn't available. The sound tier honestly reports Inconclusive. The conditional tier is Kani's bargain: assume the external world behaves, decide the function, and say so. On hop3-rootd this moves coverage from 5% (12/225) to 18% (41/225) — the same functions, a weaker but explicit guarantee.

What is modeled today

  • Types: int, bool, list, dict, str parameters, Optional/| None of any of them, and dataclass/__init__-record objects with scalar fields.
  • Control flow: straight-line, if/elif/else, try/except (partial), while and for loops (one-shot summary for crash-finding; Floyd-Hoare with an invariant for proofs).
  • Crash classes: ZeroDivisionError, IndexError (list/string), KeyError (literal-key dict access), TypeError from None-misuse and non-callable calls, AssertionError, and the contract errors.
  • Operators: integer arithmetic (with exact floor // and %), comparisons, boolean logic, isinstance narrowing (via a per-value type tag), truthiness, string/list length and indexing, ord() on characters, and the pure builtins len/sum/any/all/bool/ord.
  • Calls: same-module and same-tree imported functions are inlined; contracted functions are abstracted by their contract.

The single biggest unmodeled area, and the top of the burn-down on real code, is general object attribute reads and method calls (~52% of the gap on hop3-rootd). See notes/08-NEXT-STEPS.md in the repository.

How soundness is enforced — and tested

Two mechanisms, one philosophy: never trust a verdict you haven't executed.

1. Structural honesty in the engine

An operation mcpython can't encode exactly raises _Unmodeled internally, which drops the current path to Inconclusive — it can never become a crash or a proof. Imprecise values are over-approximations (a fresh symbol whose domain contains reality), so they can still prove safety via UNSAT but can never report a crash (whose witness might not reproduce). The one rule this rests on: an imprecise term must be a loose value, never a wrong one — an inexact encoding masquerading as imprecise silently licenses false proofs (this is exactly how a subtle floor-division bug slipped through for a while; see the tech report).

2. Generate-then-execute red-teaming

New capabilities are validated adversarially, never by eyeballing:

  1. Generate — an LLM produces programs designed to trick the verifier into a false verdict (sandbox/redteam_*.mjs, multi-agent). Stored as JSON corpora in sandbox/.
  2. Execute — a deterministic ground-truth harness runs every function and every reproducer and flags any disagreement:
  3. sandbox/gt_fuzz.py (default tier): a reported crash must raise the stated exception; a proven function must not raise on any type-valid input (Cartesian product of per-annotation domains).
  4. sandbox/gt_fuzz_stub.py (conditional tier): same, modulo stubbed calls.
  5. sandbox/gt_fuzz_harness.py (proof-harness tier): a proven harness must never fail its assert on drawn inputs; a refuted harness must fail on its witness.

Running them:

uv run python sandbox/gt_fuzz.py sandbox/corpus_assert.json sandbox/corpus_narrow.json   # ...
uv run python sandbox/gt_fuzz_stub.py sandbox/corpus_stub.json
uv run python sandbox/gt_fuzz_harness.py sandbox/corpus_charscan_harness.json

Each prints PASS — 0 unsound or names the offending verdict with the input that falsifies it.

Current state: ~2,950 adversarial programs across 23 corpora, all four tiers, 0 unsound. Plus 503 unit/integration/e2e tests and a clean make lint.

Discipline for future work: re-run every corpus in every tier after any engine change — a soundness bug in the scoping layer is invisible to the loop-invariant corpus. (This is not hypothetical: 22 latent unsound verdicts once hid on main because the fuzzer was only ever run on the newest corpus.) Every new crash class or proof capability gets its own adversarial round before it counts.