Metadata-Version: 2.3
Name: forall
Version: 0.3.1
Summary: A symbolic verifier for typed Python that finds crashes without running your code
Author: Stefane Fermigier
Author-email: Stefane Fermigier <sf@abilian.com>
Requires-Dist: pysmt>=0.9.6
Requires-Dist: z3-solver==4.13.4.0
Requires-Python: >=3.12
Description-Content-Type: text/markdown

# forall

A **sound, non-executing verifier for type-annotated Python.** forall reads your source, lowers each function's logic to SMT (via [pysmt](https://github.com/pysmt/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](https://github.com/model-checking/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](https://github.com/astral-sh/ty), [pyrefly](https://pyrefly.org), or [mypy](https://mypy-lang.org) 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

```sh
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`):

```sh
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:

```python
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

| Mode | What you write | What you get |
|---|---|---|
| **Crash-finding** (default) | nothing | Sound, replayable crashes + proofs of crash-freedom for whatever it can fully model. |
| **`--unwind K`** | nothing | Bounded model checking: unrolls each loop K times to find crashes *inside* loops, with the exact witness. Additive: never costs you a proof. |
| **`--conditional`** | nothing | Also decides functions whose only unknown is an external call, *assuming those calls return normally*. Verdicts tagged CONDITIONAL. |
| **Proof harnesses** | a `@proof` function | Prove a real *property* (`validate_port(p) == p` for all valid `p`), beyond just crash-freedom. Loop invariants prove properties over loops of any length; char-level and composition reasoning proves a validator's security invariants. |
| **Contracts** | `@requires` / `@ensures` | Verify a function once against a spec, then reuse the contract at every call site, skipping re-analysis of the body. This is how verification *scales*. |

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](docs/src/tutorial.md)**: eight steps, one file each, in [`examples/`](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:**

```sh
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:

```sh
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,670 adversarial programs across 89 corpora, all 5 tiers, 0 unsound.**

The corpora check the engine against *programs*. The claims the engine makes about Python itself — "this call cannot raise", this exception hierarchy, this mutator table — are checked by a second instrument: tripwire tests that read the engine's own tables and **execute each claim against CPython** on every test run (`notes/40-CLAIM-AUDIT-LEDGER.md`). Real code does not contain the mistakes an engine's tables make, so no corpus reaches that class; the tripwires exist because reading one table for four minutes once found seven false proofs the whole corpus set had missed.

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](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–90%. 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](docs/src/tutorial.md)**: the guided tour: eight steps from a first crash to a proven security invariant, built on [`examples/`](examples/).
- **[docs/src/getting-started.md](docs/src/getting-started.md)**: install, first run, reading the report.
- **[docs/src/harness-api.md](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](docs/src/tiers-and-guarantees.md)**: the five tiers, exactly what each proves, and how soundness is enforced and tested.
- **[CHANGES.md](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](notes/tech-report-01.md)**: the preliminary technical report.
- **[notes/12-RESULTS.md](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](notes/28-ROADMAP.md)**: where this is going — four releases, each with what ships and the one condition that decides whether it is done.
- **[notes/26-WHAT-IS-RULED-OUT.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](notes/11-STRATEGY.md)**: the direction and its evidence; **[notes/plans/](notes/plans/)**: the running weekly plans.
- **[notes/10-BOUNDED-UNROLLING.md](notes/10-BOUNDED-UNROLLING.md)**: the BMC design log. Superseded design records live in **[notes/OLD/](notes/OLD/)**.
