# Verification Status

All three pipeline layers (EDSL → CompilationModel → IR → Yul) are complete and machine-checked by `lake build`. Zero `sorry`. For *how* these proofs are built, see [Proof Techniques](/proof-techniques); for *what is trusted vs verified*, see [Trust Model](/trust-model). The authoritative axiom list lives in [AXIOMS.md](https://github.com/lfglabs-dev/verity/blob/main/AXIOMS.md).

## Per-contract proof coverage

Counts are theorems in each module. Read the actual statements in [`Contracts/<Name>/Proofs/`](https://github.com/lfglabs-dev/verity/tree/main/Contracts), Lean is the source of truth.

| Contract | Basic | Correctness | Conservation / Supply | Isolation | Native | Total |
|----------|-------|-------------|----------------------|-----------|--------|-------|
| SimpleStorage | 13 | 7 |, |, |, | 20 |
| Counter | 19 | 9 |, |, |, | 28 |
| SafeCounter | 20 | 8 |, |, |, | 28 |
| Owned | 19 | 4 |, |, |, | 23 |
| OwnedCounter | 33 | 6 |, | 14 |, | 53 |
| Ledger | 24 | 6 | 7 (conservation) |, |, | 37 |
| SimpleToken | 40 | 10 | 6 (supply) | 12 |, | 68 |
| ERC20 | 15 | 7 |, |, | 3 | 25 |
| ERC721 | 6 | 5 |, |, |, | 11 |
| Vault (ERC-4626) | scaffold | scaffold | scaffold |, | 3 | 3 |
| ReentrancyExample | 5 inline (vulnerability witness + safety proofs) | | | | | 5 |

The **Native** column counts theorems that pin the IR / Yul lowering to the EVMYulLean-bridged backend (`Contracts/<Name>/Proofs/Native.lean`).

Vault carries a verified surface spec and full IR-lowering coverage; the spec-level Basic/Correctness/Conservation proofs are intentionally scaffold (issue [#1163](https://github.com/lfglabs-dev/verity/issues/1163)).

## Stdlib

Reusable proof infrastructure in `Verity/Proofs/Stdlib/`:

| Module | Theorems | What it covers |
|--------|----------|----------------|
| `Math` | ~148 | `safeAdd/Sub/Mul/Div`, `mulDivDown/Up`, `wMulDown/wDivUp`, full-precision `mulDiv512Down?/Up?`, `SNARK_SCALAR_FIELD` / `modField` |
| `Automation` | ~108 | Full-result and `runState`/`runValue` lemmas for storage, address storage, context, events, require |
| `MappingAutomation` | ~48 | Mapping, uint-keyed mapping, double-mapping automation |
| `ListSum` | ~8 | Sum reasoning for conservation proofs (`countOcc`, `balanceSum`) |

## Compiler proofs

- **Generic whole-contract Layer 2 theorem**: `Compiler/Proofs/IRGeneration/Contract.lean`, `CompilationModel.compile` correctness for the supported fragment.
- **End-to-end**: `Compiler/Proofs/EndToEnd.lean`.
- **Typed IR**: `Compiler/TypedIRCompilerCorrectness.lean`, 36 supported statement fragments including ABI-head tuples, bytes, fixed/dynamic arrays, and strings as word-typed inputs.
- **Yul semantics + preservation**: `Compiler/Proofs/YulGeneration/`, with an EVMYulLean-bridged native backend in `Compiler/Proofs/YulGeneration/Backends/`.

The Layer 2 `forEach` boundary is intentionally narrow: the generic theorem covers `Stmt.forEach varName (.literal 0) body` when `body` is supported, and `Stmt.forEach varName (.literal n) []` for any literal natural bound `n`. It does not yet prove positive loops with non-empty bodies or nonliteral bounds.

## See also

- [Proof Techniques](/proof-techniques), guard modeling, unfolding, list-sum reasoning.
- [Trust Model](/trust-model), what each theorem rules out, what assumptions remain.
- [Examples Gallery](/examples), sources the theorems apply to.