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.

Type annotations are a prerequisite, not a preference

Type discipline is the low-hanging fruit, and it comes first. forall is the cherry on top.

An unannotated parameter gives forall no domain to draw an input from, and a method on a class with an untyped __init__ gives it no receiver to model. Those are not gaps in the tool; they are outside its claim, and it will honestly say so rather than guess.

If your code is not yet typed, run ty, pyrefly, or mypy and add annotations first. That buys far more, far more cheaply, than anything here. forall earns its keep after that work, on the questions a type checker cannot answer: index bounds, division by zero, a None-deref on a narrowed path, a missing dict key, a stated postcondition.

For calibration: CPython's own stdlib is 64% unannotated parameters, so forall has little to say about it. A modern typed package is 90%+ in domain.

Install

uv sync                # or: uv pip install -e .

Requires Python 3.12+ (3.14 is what the benchmarks run on). (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.

Real output, on a real tree (hop3/core):

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

  proven crash-free — 8, for every input their types allow

WHERE THE TOOL HAS TRACTION — densest modules first
  a tree-wide percentage averages whatever the tree contains; these are where it already decides
    83%     5 of 6     identifiers.py
    11%     1 of 9     credentials.py
     6%     1 of 17    plugins.py

UNVERIFIED — 133 of 141 functions (94%). forall makes NO claim about these.
  → --conditional decides 12 of them right now (assuming external calls return normally).

  YOUR MOVE — 29
      29  external call — body not available
          → if the callee's source is yours, pass its tree (--lib) and a @proof
            harness will inline and verify it for real; for stdlib or third-party
            callees the body exists nowhere we can read, so declare an envelope
            with stub(...) or run --conditional to assume they all return
          measured: --conditional decides 12 of these 29

  FORALL OWES YOU — 104  (ranked by how many functions hit each FIRST)
      41  objects — attribute reads and method calls   [31% of the gap]
      10  a `global` declaration is not modeled yet
       ...
          blockers compound — analysis stops at the first one, so clearing a
          line decides only the functions it was the LAST blocker for

Three things that report does deliberately.

It never lets "no crashes found" be mistaken for "your code is safe." It always says how much it actually looked at.

The remainder is a burn-down with an owner on every line — what you can do (--conditional, --unwind, a harness, an invariant) versus what forall still cannot model. A percentage with no next action is a shrug; a next action with no percentage is a to-do list nobody starts.

6% is not a grade — it is a composition measurement. That tree is the average of identifiers.py at 83% and an imperative shell at 1%, so optimising the average would mean verifying the shell, which is exactly where the boundary lives. WHERE THE TOOL HAS TRACTION exists to say so: it names the modules already mostly decided, so a reader learns where to point a contract instead of inferring a grade. This is the single most important thing to understand about the numbers.

Evaluating it

Run the tests and the lint gate:

uv run pytest         # 1000+ unit/integration/e2e tests
make lint             # ruff (format + 88-col) + ty + pyrefly + zuban + mypy; 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 redteam/, versioned with the engine they police; 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,600 adversarial programs across 80 corpora, all 5 tiers, 0 unsound.

The redteam/make_*.py files are the generators that produced those corpora (multi-agent adversarial generation), and the redteam/gt_fuzz*.py files are the ground-truth harnesses that execute every verdict.

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.

What it is for

Point it at a whole tree and the number will be single digits. Point it at the module where your process boundary is validated and it reads 83–97%. That is not a defect in the tool and not a trick of the corpus — applications have a validating trust boundary and a large imperative shell, and only one of them is a verification target.

So the workflow is:

1. forall check src/ — read WHERE THE TOOL HAS TRACTION, not the headline percentage.
2. Fix any crash it found. Every one carries an input that really raises it.
3. Pick a dense module that matters — a validator, a parser, a limit check — and write a contract for one function in it (@requires / @ensures, out-of-line so your package takes no dependency).
4. Put that contract in CI. It now fails when a refactor breaks the property, naming the contract.

Step 4 is where a verifier stops being a one-time audit. A proven contract on hop3.core.identifiers survived an upstream "parse, don't validate" refactor unchanged; a one-character edit (fullmatch → match) refutes it with a witness.

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, harness_tests (one harness file, two engines: a static proof and a pytest property test), 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.
• CHANGES.md: what changed, and what is stable — forall.harness is; report text and --json are not, before 1.0.
• notes/tech-report-01.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/28-ROADMAP.md: where this is going, 0.2 through 1.0, each version with a kill criterion — plus notes/29-PLAN-0.2.md and notes/30-PLAN-0.3.md.
• notes/26-WHAT-IS-RULED-OUT.md: the directions probed and killed, with the reason for each — read before proposing one. notes/11-STRATEGY.md: the direction and its evidence; notes/plans/: the running weekly plans.
• notes/10-BOUNDED-UNROLLING.md: the BMC design log. Superseded design records live in notes/OLD/.