Skip to content

The mcpython.harness API

Everything here lives in mcpython.harness. It lets you go beyond crash-finding to prove real properties, and to make verification scale. mcpython recognises these constructs statically — it reads your source, it does not import it — with one deliberate exception noted below.

from mcpython.harness import (
    proof, any_int, any_bool, any_str, any_list, assume, invariant,  # proof harnesses
    requires, ensures,                                                # contracts
)

Proof harnesses: @proof

A proof harness looks like a unit test but is never executed — mcpython lowers its body to SMT and proves the property for every input your assumptions admit. This is the sound and precise mode: no "external calls behave" caveat.

from mcpython.harness import proof, any_int, assume
from myapp.validation import validate_port

@proof
def port_round_trips() -> None:
    p = any_int()
    assume(1 <= p <= 65535)
    assert validate_port(p) == p      # proven for all 65,535 values, never run
  • any_int() / any_bool() / any_str() / any_list() introduce a fresh symbolic input the proof quantifies over. (any_str models a string's length and, on demand, its characters — see below. any_list defaults to list[int].)
  • assume(cond) constrains the proof to inputs where cond holds. Everything after runs under that assumption. An assumption mcpython can't model precisely is refused (Inconclusive) — narrowing to an approximate input set could "prove" a property that fails on a real input.
  • assert P is the property. Proven means it holds for every admitted input. A refuted assertion is a Crash with a concrete counterexample (port_round_trips [p=0]).

The harness's target calls (validate_port) are inlined and run for real in SMT, against the actual body. A cross-file harness imports its targets; mcpython pulls in the real function and the module constants it uses.

The report tells you the scope. A @proof verdict prints the assumptions verbatim and, for each function it verified, how many of its statements the proof actually reached:

  ✓ proofs.py: port_round_trips: holds for every admitted input
      assuming: 1 <= p <= 65535
      covers validate_port — ran 2 of its 4 statements

2 of 4 because assume(1 <= p <= 65535) excludes the reject path — the harness working as intended. It's still the boundary of the claim, so it's stated: nothing in the engine can tell a well-chosen assumption from a lazy one, so it reports what it can — what you assumed, and how much you reached.

Writing a harness credits the functions it verified toward the coverage number. A proof that verifies validate_port moves the ledger; if the score refused to count your work, you'd write no more harnesses.

Loop invariants: invariant

A loop with an invariant(...) as the first statement of its body is proven by the Floyd-Hoare rule — base case, one inductive step, continuation — so the proof holds for any number of iterations. No unrolling, no bound.

@proof
def sum_of_ones_is_n() -> None:
    n = any_int()
    assume(0 <= n <= 1000)
    i = 0
    total = 0
    while i < n:
        invariant(0 <= i <= n)
        invariant(total == i)
        total = total + 1
        i = i + 1
    assert total == n            # proven for every n

Both while and for i in range(lo, hi) are supported (the for form is desugared to the equivalent while). The invariant must hold on entry and be preserved by one iteration; after the loop you may rely on invariant ∧ ¬guard.

Char-level strings: ord(s[i])

For a string s, s[i] is a character whose Unicode code point is ord(s[i]). Two reads at the same index agree — the fact a loop invariant needs to reason about "the character at position i". This is what proves a validator's real security invariant, not just crash-freedom.

The canonical example — proving "a string containing a control character is always rejected" (the contrapositive of "if it returns, no control character"), with no quantifier:

@proof
def a_control_char_is_always_caught() -> None:
    s = any_str()
    bad = any_int()
    assume(0 <= bad < len(s))
    assume(ord(s[bad]) < 0x20)          # s HAS a control char at index `bad`
    i = 0
    while i < len(s):
        invariant(0 <= i <= bad)         # can't pass `bad` without returning
        if ord(s[i]) < 0x20 or ord(s[i]) == 0x7F:
            return                        # rejected
        i = i + 1
    assert False                          # PROVEN unreachable

The invariant 0 <= i <= bad is inductive precisely because reaching i == bad forces the guard (ord(s[bad]) < 0x20 by assumption). The proof discriminates: a scan that checks < 0x20 but forgets == 0x7f does not prove when the bad char is 0x7f — exactly the security hole it should refuse to bless.

ord() is modeled only on a single character. ord of a whole string (a ValueError at runtime) stays Inconclusive.

Contracts: @requires / @ensures

Contracts are how verification scales. You verify a function once against its precondition and postcondition; every call site then reasons about the contract instead of the body — check requires, take ensures as known. A call costs the same whether the callee is three lines or three hundred, and a callee whose body mcpython can't model at all can still carry its callers once its contract is proven.

from mcpython.harness import requires, ensures

@requires(lambda port: 1 <= port <= 65535)
@ensures(lambda port, result: result == port)
def validate_port(port: int) -> int:
    if port < 1 or port > 65535:
        raise ValidationError("bad port")
    return port

The lambdas name the function's own parameters (and, for ensures, the special name result), so they read as the condition itself.

Contracts check at runtime — this is the one part of mcpython.harness that is not inert. @requires raises PreconditionError if a caller breaks it; @ensures raises PostconditionError if the function returns a forbidden value. Two reasons:

  1. A precondition that raises makes "the caller violated the contract" a real, replayable crash rather than a silent modeling assumption.
  2. The executable semantics is what lets the soundness harness falsify every contract verdict by running the code.

What mcpython proves and reports:

  • The function against its contract: assume requires, prove the body can't crash and that ensures holds on every path out.
  • At each call site: a caller that can break the requires is a Crash (with the input); otherwise the postcondition is assumed.
  • Only a proven contract may be substituted. Contracts are discharged in a fixpoint pre-pass, so chains (f calls g calls h) work; a cycle simply never proves.
  • Under --conditional, an unproven contract is taken on trust and the verdict tagged CONDITIONAL — this is what makes a contract useful on a body you can't model.

A functional postcondition (result == <expr>) pins the return value exactly, so a caller can prove things through the call (100 // validate_port(p) is safe because p >= 1) — without ever looking at the body. A bounding postcondition (result >= 1) proves crash-freedom downstream without naming a specific value.

Contract abstraction currently supports int/bool parameters.

Worked end-to-end example

net/validation.py:

from mcpython.harness import requires, ensures

@requires(lambda port: 1 <= port <= 65535)
@ensures(lambda port, result: result == port)
def validate_port(port: int) -> int:
    if port < 1 or port > 65535:
        raise ValueError("port out of range")
    return port

def bind(port: int) -> int:
    return validate_port(port)          # forgot to guard `port`!

CRASHES — 1
  net/validation.py:11: bind: PreconditionError: validate_port() requires 1 <= port <= 65535
      reproduce: bind(0)

  proven against their contracts — 1, for every input the @requires admits
    net/validation.py: validate_port
        1 <= port <= 65535
        result == port

bind(0) really raises PreconditionError (any out-of-range port witnesses it — the solver may pick either end). The contract caught a real bug at the call site, and validate_port is proven correct for every valid port.