HN Showcase
Back to browse
GitHub Repository

Formally verified smart contracts gives mathematical certainty across all inputs and execution paths. We bet that agents will make full formal verification practical.

118 starsLean

Verity, Formally verified smart contracts from spec to bytecode

by th0rgal2·Feb 26, 2026·1 point·0 comments
Visit ProjectView on HN

AI Analysis

●●●BangerWizardryBig BrainZero to One

Formally verified EVM bytecode with zero sorries—actually ships working proofs.

Strengths
  • •431 proven theorems with zero unsolved 'sorry' placeholders demonstrates rigor
  • •Native EVM codegen means no intermediate trust boundary or unverified compiler
  • •Zero-to-One: formal verification reaching smart contracts is a genuinely unsolved problem
Weaknesses
  • •Lean 4 has a steep adoption curve; unclear if production teams will learn it
  • •No evidence of real contracts deployed or audited against competitors like Certora
Target Audience

Smart contract developers, blockchain security engineers, formal methods researchers

Similar To

Certora · Runtime Verification

Post Description

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

Similar Projects