I built Verity, a Lean 4 framework for writing smart contracts, proving properties, and compiling to EVM bytecode.
Current status:
- 431 proven theorems
- 0 sorry
- 404 Foundry tests across 35 suites
- 5 minute quick start in the README
You can find the repo at https://github.com/th0rgal/verity , documentation at https://verity.thomas.md/ . I’d especially love feedback on:
1) proof ergonomics for contract specs
2) compiler output assumptions/trust boundaries
3) what would block real production adoption