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