Verity
A Formally Verified Smart Contract Compiler in Lean 4.
Verity lets you express smart contract logic in Lean 4, state properties about that logic, and produce machine-checkable proofs that those properties hold for all inputs. The framework compiles to EVM bytecode via Yul, so verified contracts can be deployed directly.
Verity is still early: 431 theorems, 0 unproven steps, 1 axiom (keccak256 collision resistance), 403 Foundry tests, 11 contracts. We are iterating on the framework as we use it on real verification engagements.
Why
Audits check what the auditor thinks to check. Bounded model checking can verify properties up to a search depth. Full formal proofs can prove them universally, but they have historically been too expensive for most teams.
We think this is a tooling problem. If the framework is good enough, formal verification becomes practical, especially as AI gets better at generating proofs.
Links
Research paper draft (PDF, work in progress)