Metadata-Version: 2.3
Name: forall
Version: 0.1.0
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.

## Install

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

```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*.

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

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

```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,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](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](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`, 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.
- **[notes/forall-tech-report.md](notes/forall-tech-report.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/11-STRATEGY.md](notes/11-STRATEGY.md)**: the direction and its evidence; **[notes/plans/](notes/plans/)**: the running weekly plans.
- **[notes/09-PROVING-HOP3-ROOTD.md](notes/09-PROVING-HOP3-ROOTD.md)** and **[notes/10-BOUNDED-UNROLLING.md](notes/10-BOUNDED-UNROLLING.md)**: the case-study and BMC design logs.
- **[notes/07-KANI-ROADMAP.md](notes/07-KANI-ROADMAP.md)**: the design arc and what landed.
