From Foundry Invariants to Lean Proofs
Bridging Foundry invariant testing and formal verification with Lean
Invariant testing in Foundry repeatedly calls the selected contract actions with generated inputs and searches for a state that breaks an assertion. When it finds one, developers get a concrete counterexample they can reproduce.
A passing invariant test means Foundry did not find a violation in the executions it explored. Formal verification asks a stronger question: can we prove that the property holds for every execution represented by a mathematical model? Lean checks that proof step by step.
Bridging the two workflows
We built a programmatic bridge that reads a Foundry invariant suite, identifies the property, state getters, target contracts and callable actions, then connects them to a Verity model.
The bridge carries the property developers already maintain via Foundry into Lean, where the corresponding invariant can be proven and checked. This implementation is a proof of concept (POC). It demonstrates the complete path on a deliberately small example rather than claiming support for every Foundry invariant suite.
How it works
This walkthrough uses a bounded exact-in swap fixture based on Balancer ReClamm contracts. Balancer ReClamm is an automated market maker: users swap one token for another against reserves held by a pool.
1. Define the invariant
The developer writes or reuses a normal Foundry invariant. In the Balancer example, it says that the ReClamm product after a rounded swap quote must be at least as large as it was before.
function invariant_productDoesNotDecrease() public view {
assert(handler.afterProduct() >= handler.beforeProduct() );
}2. Connect Foundry to Verity
The tool finds beforeProduct, afterProduct and swapExactIn, then checks that they match the corresponding getters and action in the Verity model. If it cannot establish an exact match, it stops instead of guessing.
Running the bridge produces a linkage report, then checks the generated artifact and its Lean proofs:
$ make example-balancer-reclamm
{
"schemaVersion": 1,
"toolchain": { "solc": "0.8.33+commit.64118f21", "forge": "1.5.0" },
"invariants": [{
"name": "invariant_productDoesNotDecrease",
"lowered": true,
"getters": ["afterProduct()", "beforeProduct()"],
"actions": ["swapExactIn(uint256)"],
"linkage": [
{ "role": "action", "modelSignature": "swapExactIn(uint256)", "matched": true },
{ "role": "getter", "modelSignature": "afterProduct()", "matched": true },
{ "role": "getter", "modelSignature": "beforeProduct()", "matched": true }
]
}],
"diagnostics": []
}
Build completed successfully (858 jobs).
trust-source check passed: no sorry, admit, or project-defined axioms
Balancer ReClamm importer example checks passed.3. Generate and prove the invariant
The tool generates the Lean invariant stating that the property holds initially and remains true after the modeled swap. A verification engineer completes the model-specific proof, and Lean's kernel checks every proof step.
The resulting specification
After a rounded swap quote, the pool's accounting product must be at least as large as it was before.
The tabs show the same property as a plain-English rule, the original Foundry assertion, and the generated Lean invariant linked to the Verity model.
In the worked example, the bridge reads the Solidity assertion, connects the two product getters and exact-in swap action to the model, and generates the corresponding Lean invariant. The proof then shows that the rounded quote preserves it.
git clone https://github.com/lfglabs-dev/foundry-to-lean cd foundry-to-lean make example-balancer-reclamm
More research
ERC-4337 EntryPoint Execution Invariant
A reproducible two-mode scenario for one modeled EntryPoint v0.9 handleOps execution-count invariant.
Proving the SPHINCS- Post-Quantum Verifiers
A hand-held tour of SPHINCS-, what a correct on-chain verifier must check, and how we proved it in Lean 4 with Verity.
What is a formal proof?
A short explanation for non-specialists.