Verity

A formally verified smart contract compiler for Ethereum, written in Lean 4. Write a contract in an embedded DSL (or import it from Solidity), prove properties about it, and compile it to EVM bytecode through a compiler whose layers are themselves proved. Documentation: veritylang.com · Paper: verity.pdf · MIT licensed.

Guarantees

• Layer 1 (DSL → CompilationModel): per-contract bridge theorems.
• Layer 2 (CompilationModel → IR): a generic whole-contract theorem covers the supported fragment with zero axioms.
• Layer 3 (IR → Yul): every statement form is proved equivalent. The dispatch bridge is an explicit theorem hypothesis, not an axiom.

The compiler proof stack carries 0 axioms and no sorry. Yul → bytecode is done by pinned solc and is trusted. Verification is scoped: the proved fragment and everything trusted are listed in the trust documents below.

Quick start

lake build     # check every proof
make check     # repository checks run in CI (no Lean build)
make test-foundry

Where things are

Path	Contents
Verity/	The DSL (verity_contract), its semantics and proof library
Compiler/	The compiler and its correctness proofs
Compiler/SolidityImport/	Solidity → CompilationModel importer (docs)
Contracts/	Example and smoke contracts with their proofs
docs/	Trust boundary, axioms, verification status, design notes
scripts/, test/, artifacts/	CI checks, Foundry tests, generated reports

What to review

1. docs/TRUST_ASSUMPTIONS.md: what is proved and what is trusted.
2. docs/AXIOMS.md: every axiom, with its justification.
3. docs/VERIFICATION_STATUS.md: theorem and test inventory, regenerated by CI.
4. docs/SOLIDITY_IMPORT.md: the Solidity importer and its differential validation.

Contributions: see CONTRIBUTING.md.