Rust → Charon → Aeneas → Lean → Leanstral → kernel.
rustproof is designed to take a Rust crate, find the functions whose behavior can be proven, patch them at build time into the subset Aeneas accepts, extract them to Lean 4, propose theorems in plain English and Lean, generate proofs with Leanstral, and check every proof with the Lean kernel.
Twelve idempotent steps, keyed by content hash.
The pipeline as it is designed, in order.
I/O is a boundary, not a blocker.
What can be proven
Pure, deterministic, typed functions: validation, parsing, pricing and scoring rules, data transformations, numeric kernels, state machines.
What’s excluded
I/O, network, filesystem, clocks, randomness, global mutable state, concurrency and async, unsafe code, FFI, and anything that depends on library types Aeneas has no model for and no brick can replace. Excluded functions will be visible in every surface, with the reason.
Overflow
Aeneas models arithmetic so that overflow is a failure, matching Rust’s debug builds. Release builds wrap silently. The patched build is designed to set overflow-checks = true, so the shipped binary matches the model everywhere, and a theorem’s precondition is exactly the set of inputs on which the code doesn’t fail.
Where it will live
.rustproof/ manifest.toml obligations, hashes, bricks, approvals patches/ one patch per obligation (may be empty) specs/ theorem statements (CODEOWNERS) proofs/ generated proofs lean/ Lake project; Generated/ is Aeneas output state/ local step cache (never committed)
One set of states, every surface.
Every status shows its glyph and its label, so it reads without color; two pairs share a glyph, and the label tells them apart.
| State | Meaning | Who acts |
|---|---|---|
| Proven | Spec approved; proof checked by the Lean kernel against the current patched tree | No one |
| Checking | Verification running | System |
| Searching | Proof search or repair running | System |
| Needs review | A spec, or a patch that requires approval, is waiting for a person | A person |
| Failing | Proof doesn't check; repair hasn't succeeded | Agent, then a person |
| Counterexample | A concrete input breaks the claim | Agent, then a person |
| Weak spec | Spec still holds for a mutant | A person |
| Stale | The function or a callee changed since its proof was checked; cleared automatically if re-extraction yields the same Lean | System (re-patch, re-prove) |
| Excluded | Outside the proof boundary | No one |
See it on your own crate.
/rustproof:init will report how much is provable as-is, how much with patches, and what is excluded and why.