Show HN: Verity, Formally verified smart contracts from spec to bytecode
1 points
1 hour ago
| 0 comments
| github.com
| HN
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

No one has commented on this post.