Rewrite patterns, with the proof shape included.
A patch is one instance of a brick at one site. By design, each brick takes a shape of Rust that Aeneas can’t extract, produces one it can, and comes with a proof template: the loop invariant and tactic skeleton for that idiom.
The planned built-in library.
Bumping a brick is designed to re-patch and re-prove its instances. Orgs will be able to add custom bricks; every patch from one will need a person’s approval.
| Brick | Before | After |
|---|---|---|
memo-to-accumulator | Memoized recursion with a HashMap | An accumulator loop |
extract-inner-loop | Nested loops | The inner loop as its own function |
remove-labeled-break | break 'outer / continue 'outer | A helper with an early return |
range-to-while | for i in a..b | while with an explicit index and bound |
isolate-io | A function that computes and does I/O | The pure half as its own function; the I/O half excluded |
Planned: rustproof-std, proven once and reused.
Checked sums, bounded searches, sorted merge. A patch will swap a call to one in, and the proof will compose its existing lemmas.
checked_sum
Will sum a slice with explicit overflow failure; its theorem will state that the result equals the mathematical sum when no overflow occurs.
bounded_search
Will search linearly with an index bound; its theorem will state that a found index is in range and holds the key.
merge_sorted
Will merge two sorted slices; its theorem will state that the result is sorted and a permutation of the concatenation.
An honest limit.
A brick can’t have a general proof that it preserves semantics. Rewrite rules can’t be proven correct without a formal semantics of the source language, and an instance can’t be checked in Lean either, because the “before” is by definition not extractable.
So patches are designed to be validated by differential testing and by the person reading the diff. The proofs are about the patched code, which is what ships. This gap affects confidence in the diff, not the correctness of the artifact.
Write the provable form directly.
The make-provable skill will teach Claude the bricks as idioms, so the patch can stay empty.