forall

A sound, non-executing verifier for type-annotated Python. forall reads your source, lowers each function's logic to SMT (via pysmt + Z3), and either finds a replayable crash or proves crash-freedom: without ever importing or running your code. Analysing a module that opens sockets, spawns processes, or deletes files is completely safe: there is nothing to sandbox.

Its cardinal guarantee is zero false verdicts: every reported crash comes with a concrete input that actually raises it, and every proof holds for every input the types (or your assumptions) admit. When it can't decide something, it says so; it never guesses.

forall adapts the Kani model checker's methodology from Rust to typed Python. Like Kani, it offers push-button crash-finding and a specification language (proof harnesses, loop invariants, and function contracts), so you can start with zero annotation and scale up to unbounded correctness proofs as needed.

Install

uv sync                # or: uv pip install -e .

Requires Python 3.13. (Z3 is pinned to the last release with a prebuilt wheel for the project's Python/arch; see pyproject.toml.)

Quick start

Point it at a file or directory (directories are walked for *.py):

uv run forall check path/to/module.py
uv run forall check src/                    # walk a whole tree
uv run forall check module.py --conditional # decide more, modulo external calls
uv run forall check a.py b.py --json        # machine/AI-readable output
uv run forall check module.py -dd           # trace the analysis (to stderr)

Given this file:

from forall.harness import ensures, requires


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


@requires(lambda qty: qty >= 1)
@ensures(lambda qty, result: 1 <= result <= qty)
def clamp_batch(qty: int) -> int:
    if qty > 100:
        return 100
    return qty


def dispatch(qty: int) -> int:
    return clamp_batch(qty)

forall reports:

VERIFIED — 3 of 3 functions (100%)

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

  proven crash-free — 1, for every input their types allow
    orders.py
        dispatch
  proven against their contracts — 1, for every input the @requires admits
    orders.py: clamp_batch
        qty >= 1
        1 <= result <= qty

average(0, 0) really does raise. clamp_batch is proven to meet its contract for every valid input, and because that proof exists, dispatch gets it for free. Its body was never re-analysed. Exit code is 1 when any crash is found, 0 otherwise, so it drops into CI like a linter.

The things it can do

They share one report, the ledger (below), and one guarantee: no false crash, no false proof.

Work through the core arc in docs/src/tutorial.md: eight steps, one file each, in examples/.

The report is a ledger

The headline is two numbers over the whole codebase. VERIFIED counts what forall could decide on its own. SPECIFIED counts what is proven against a contract or @proof property you wrote: the number that says the code is correct.

VERIFIED — 12 of 225 functions (5%)
SPECIFIED — 0 of 225 functions (0%), proven against a contract or a @proof property
  → nothing here states what the code should DO; crash-free is not correct

CRASHES — 2, each with an input that triggers it
  ...file:line, exception, and a REAL reproducer each; -v adds the source line...

  proven crash-free — 10, for every input their types allow
    (run with -v to list every proven function by name)

UNVERIFIED — 213 of 225 functions (95%). forall makes NO claim about these.
  → --conditional decides 31 of them right now.

  YOUR MOVE — 29
      29  external call — body not available
          → --conditional, or call it from a @proof harness

  MCPYTHON OWES YOU — 184  (ranked by the coverage each would buy)
     111  objects — attribute reads and method calls   [37% of the gap]
      ...

The unverified remainder is a burn-down with an owner on every line: what you can do (run --conditional/--unwind, write a harness, add an invariant) versus what forall still can't model, ranked by how much coverage each feature would buy. A percentage with no next action is a shrug; a next action with no percentage is a to-do list nobody starts. The report gives both, and it never lets "no crashes found" be mistaken for "your code is safe". It always says how much it actually looked at.

Evaluating it

Run the tests and the lint gate:

uv run pytest         # 900+ unit/integration/e2e tests
make lint             # ruff (format + 88-col) + mypy + ty; zero warnings

Check the soundness guarantee yourself. forall's verdicts are validated by generate-then-execute red-teaming, never by eyeballing. Adversarial programs (LLM-generated, designed to trick the verifier) are stored as JSON corpora in sandbox/; a deterministic ground-truth harness runs every function and every reproducer and flags any disagreement. One command routes every corpus to the tier that decides it:

make red-team

It prints, per corpus, PASS — 0 unsound or names the offending verdict with the input that falsifies it, then an aggregate. The current state: ~4,700 adversarial programs across ~70 corpora, all 5 tiers, 0 unsound. (sandbox/ is gitignored; the corpora live locally.)

The sandbox/redteam_*.mjs files are the generators that produced those corpora (multi-agent adversarial generation).

Run it against the whole Python standard library. The stdlib is the standing external benchmark: make stdlib-sweep verifies all ~14,500 functions in ~30 s, validates every crash claim by executing its reproducer, executes hundreds of its own proofs under type-valid draws, and diffs every claim against the committed baseline (notes/13-STDLIB-LEDGER.md). A lost proof is named, audited, and accepted or fixed. It has found real stdlib crashes (urllib.parse._coerce_args(), every curses.ascii predicate on ''), each reproduced live before entering the ledger.

Where to look next

• docs/src/tutorial.md: the guided tour: eight steps from a first crash to a proven security invariant, built on examples/.
• docs/src/getting-started.md: install, first run, reading the report.
• docs/src/harness-api.md: @proof, any_*, assume, invariant, @requires/@ensures, char-level and composition reasoning, --unwind, worked examples.
• docs/src/tiers-and-guarantees.md: the five tiers, exactly what each proves, and how soundness is enforced and tested.
• notes/forall-tech-report.md: the preliminary technical report.
• notes/12-RESULTS.md: the measured claims on real code, at named commits: the proven contracts, the per-tier story, the stdlib benchmark, and the current limitations.
• notes/11-STRATEGY.md: the direction and its evidence; notes/plans/: the running weekly plans.
• notes/09-PROVING-HOP3-ROOTD.md and notes/10-BOUNDED-UNROLLING.md: the case-study and BMC design logs.
• notes/07-KANI-ROADMAP.md: the design arc and what landed.