Verity

Formally verified smart contracts. From spec to bytecode.

---

What is Verity?

Verity is a formally verified smart contract compiler written in Lean 4. You write contracts in an embedded DSL (domain-specific language), write specs describing what the contract should do, prove the specs hold, and compile to Yul/EVM bytecode, with machine-checked proofs that compilation preserves semantics.

In short: write a contract, state what it should do, prove it, compile it, and the compiler is proven to not break anything along the way.

---

How it works

1. Write a contract

Contracts are written using the verity_contract macro. It is the canonical contract authoring path, and it generates both an executable Lean specification (Contract monad) and a declarative compilation model (CompilationModel) from one definition, with a machine-checked proof that they agree:

-- Contracts/Counter/Counter.lean
verity_contract Counter where
  storage
    count : Uint256 := slot 0

  function increment () : Unit := do
    let current ← getStorage count
    setStorage count (add current 1)

The macro surface also supports contract-level constants and constructor-bound immutables:

verity_contract FeeVault where
  storage
    owner : Address := slot 0

  constants
    basisPoints : Uint256 := 10000

  immutables
    treasury : Address := seedTreasury
    withdrawFeeBps : Uint256 := 30

  constructor (seedTreasury : Address) := do
    setStorageAddr owner msgSender

  function feeOn (amount : Uint256) : Uint256 := do
    return div (mul amount withdrawFeeBps) basisPoints

  function treasuryAddr () : Address := do
    return treasury

Under the hood, the macro generates a Contract α state monad (ContractState → ContractResult α) with operations like getStorage, setStorage, and require that manipulate blockchain state. Constants are validated as compile-time expressions, and immutables are initialized once from constructor-visible expressions and exposed as read-only values in function bodies. You generally should not hand-write a separate CompilationModel; the macro-generated one is the compiler input.

2. Write a spec

Specs are plain Lean predicates describing what the contract should do:

-- Contracts/Counter/Spec.lean
def increment_spec (s s' : ContractState) : Prop :=
  s'.storage 0 = add (s.storage 0) 1 ∧
  storageUnchangedExcept 0 s s' ∧
  sameAddrMapContext s s'

This says: after increment, slot 0 increased by 1, no other slot changed, and context (sender, address maps) is preserved.

3. Prove the spec

Proofs show the contract satisfies its spec. Lean's type checker verifies them:

-- Contracts/Counter/Proofs/Basic.lean
theorem increment_meets_spec (s : ContractState) :
    let s' := ((increment).run s).snd
    increment_spec s s' := by
  refine ⟨?_, ?_, ?_⟩
  · rfl
  · intro slot h_neq; simp [increment, count, ...]; split <;> simp_all
  · simp [sameAddrMapContext, ...]

4. Compile, with proven correctness

The compiler turns contracts into Yul (Solidity's low-level IR) through three layers, each proven to preserve semantics:

EDSL contract (Lean)
  ↓  Layer 1: EDSL ≡ CompilationModel     [PROVEN FOR CURRENT CONTRACTS; GENERIC CORE, CONTRACT BRIDGES]
CompilationModel (declarative IR spec)
  ↓  Layer 2: CompilationModel → IR        [GENERIC WHOLE-CONTRACT THEOREM]
Intermediate Representation
  ↓  Layer 3: IR → Yul                     [GENERIC SURFACE, EXPLICIT BRIDGE HYPOTHESIS]
Yul
  ↓  solc (trusted external compiler)
EVM Bytecode

Layer	What it proves	Key file
1	A generic typed-IR core plus contract-level bridge theorems establish EDSL execution = CompilationModel interpretation for the current supported contracts	TypedIRCompilerCorrectness.lean
2	A generic whole-contract theorem is proved for the current explicit supported fragment, and its function-level closure now runs by theorem rather than axiom. The theorem surface explicitly assumes normalized transaction-context fields. Follow-on work in #1510 now focuses on widening the fragment.	Contract.lean
3	IR → Yul codegen is proved generically at the statement/function level, but the current full dispatch-preservation path still uses 1 documented bridge hypothesis; the checked contract-level theorem surface now makes dispatch-guard safety explicit for each selected function case	Preservation.lean

There is currently 1 documented Lean axiom in total: the selector axiom. Layer 2's former generic body-simulation axiom has been eliminated, and Layer 3 keeps its remaining dispatch bridge as an explicit theorem hypothesis rather than a Lean axiom. See AXIOMS.md.

Layer 1 is the frontend EDSL-to-CompilationModel bridge. The per-contract files in Contracts/<Name>/Proofs/ prove human-readable contract specifications; they are not what "Layer 1" means in the compiler stack. Layer 2 now has a generic whole-contract theorem for the explicit supported fragment. The compiler proves Layer 2 preservation automatically — no manual per-contract bridge proofs are needed. Layers 2 and 3 (CompilationModel → IR → Yul) are verified with the current documented axioms and bridge boundaries; see docs/VERIFICATION_STATUS.md, docs/GENERIC_LAYER2_PLAN.md, and AXIOMS.md.

5. Test the compiled output (belt and suspenders)

Foundry tests validate EDSL = Yul = EVM execution. See docs/VERIFICATION_STATUS.md for the current test count and coverage snapshot. The proofs already guarantee correctness, but the tests confirm it works end-to-end:

FOUNDRY_PROFILE=difftest forge test

---

Verified contracts

Contract	Theorems	What it demonstrates
SimpleStorage	20	Store/retrieve with roundtrip proof
Counter	28	Increment/decrement, composition proofs
SafeCounter	25	Overflow/underflow revert proofs
Owned	23	Access control, ownership transfer
OwnedCounter	48	Cross-pattern composition, lockout proofs
Ledger	33	Deposit/withdraw/transfer, balance conservation
SimpleToken	61	Mint/transfer, supply conservation
ERC20	19	ERC-20 baseline with approve/transfer
ERC721	11	NFT ownership/approval baseline
ReentrancyExample	5	Reentrancy vulnerability vs safe pattern
CryptoHash	—	External library linking demo (no proofs)

Current theorem totals, test counts, coverage, and proof status live in docs/VERIFICATION_STATUS.md.

Current dynamic-type status: ABI-level String support is available for macro parsing, calldata flow, returnBytes, event payloads, custom-error payloads, and direct parameter == / != checks via the dynamic-bytes equality helper. Solidity-style string storage/layout, dynamic linked externals, dynamic local aliases, and broader word-style operators still remain intentionally unsupported while issue #1159 stays open for the remaining work.

---

External calls

Verity's DSL prevents raw external calls for safety. Instead, you can:

1. Link external Yul libraries (e.g., Poseidon hash) at compile time:

   lake exe verity-compiler --link examples/external-libs/PoseidonT3.yul -o artifacts/yul

   The linked library's correctness is a trust assumption. See examples/external-libs/.

2. Use External Call Modules (ECMs) for typed, auditable call patterns (ERC-20 transfers, precompiles, callbacks). See Compiler/Modules/ and docs/EXTERNAL_CALL_MODULES.md.

There is also a bounded tryCatch surface in verity_contract for low-level call-style expressions that return a success word:

tryCatch (call gas target value inOffset inSize outOffset outSize) (do
  setStorage lastFailure 1)

This is intentionally narrower than Solidity's full try/catch: higher-level external-call helpers / ECMs do not lower through tryCatch yet, and catch-payload decoding is not available on the compilation-model path. Issue #1161 remains open for that broader external-call surface.

---

Quick start

# Install Lean 4
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
source ~/.elan/env

# Clone and build; verifies the current proof set
git clone https://github.com/Th0rgal/verity.git && cd verity
lake build

# Compile contracts to Yul
lake exe verity-compiler --manifest packages/verity-examples/contracts.manifest
lake exe verity-compiler --module Contracts.Counter.Counter  # specific contract
lake exe verity-compiler-patched --enable-patches --manifest packages/verity-examples/contracts.manifest

# Run Foundry tests
FOUNDRY_PROFILE=difftest forge test

To reuse trusted CI-built compiler artifacts locally instead of rebuilding Lean native code:

scripts/fetch_prebuilt_compiler_artifacts.sh main
FOUNDRY_PROFILE=difftest DIFFTEST_YUL_DIR=compiler/yul forge test

Scaffold a new contract:

python3 scripts/generate_contract.py MyContract
python3 scripts/generate_contract.py MyToken --fields "balances:mapping,totalSupply:uint256,owner:address"

This creates: implementation, spec, invariants, proofs, and Foundry test files.

---

Verification guarantees

Every claim is enforced by CI on every commit. See docs/VERIFICATION_STATUS.md for the current counts, coverage tables, and proof-status snapshot, then use make verify, make axiom-report, make test-foundry, and make check for local confirmation.

---

How Verity compares

	Certora	Halmos	Verity
Approach	Bounded model checking	Symbolic execution (Z3)	Interactive theorem proving (Lean 4)
Strengths	Great automation, battle-tested	Free, integrates with Foundry	Unbounded proofs, verified compiler
Trade-offs	Bounded (may miss edge cases)	Bounded (path explosion)	Higher per-property effort
Compiler trust	Trusts solc entirely	Trusts solc entirely	Verifies 3 compilation layers
Best for	Production audits at scale	Bug-finding in Foundry	High-assurance contracts

Verity is not a replacement for these tools. It's for cases where you need mathematical certainty across all inputs and execution paths. The effort gap is narrowing as AI improves at interactive theorem proving.

---

Documentation

Document	What it covers
TRUST_ASSUMPTIONS.md	What's verified vs trusted, trust reduction roadmap
AXIOMS.md	All axioms with soundness justifications
docs/VERIFICATION_STATUS.md	Per-contract theorem status, coverage tables
docs/ROADMAP.md	Verification progress, planned features
CONTRIBUTING.md	Coding conventions, PR guidelines
docs/EXTERNAL_CALL_MODULES.md	ECM framework guide
docs/ARITHMETIC_PROFILE.md	Wrapping arithmetic specification
Docs site	Full documentation with guides

---

Project structure

verity/
├── Verity/              # EDSL framework
│   ├── Core/            #   Core types: Contract monad, ContractState, Uint256
│   ├── Macro/           #   verity_contract macro elaborator
│   └── Stdlib/          #   Proven helper lemmas (arithmetic, automation)
├── Contracts/           # Verified contract implementations
│   ├── <Name>/Spec.lean       #   Formal specification
│   ├── <Name>/Proofs/*.lean   #   Correctness proofs
│   ├── <Name>/<Name>.lean      #   Canonical verity_contract definitions
│   └── Proofs/                   # Per-contract specification proofs
├── Compiler/            # Compilation pipeline
│   ├── CompilationModel/      # Declarative compiler-facing model (types, validation, codegen)
│   ├── Proofs/          #   Compilation correctness proofs (Layers 1-3)
│   │   ├── EndToEnd.lean            # Layers 2+3 composition
│   │   └── YulGeneration/           # IR → Yul preservation
│   ├── Yul/             #   Yul code generation
│   └── Modules/         #   External Call Modules (ECMs)
├── packages/            # Independent sub-packages (verity-edsl, verity-compiler, verity-examples)
├── test/                # Foundry tests
├── artifacts/yul/       # Compiled Yul output
└── scripts/             # CI validation scripts

License

MIT - See LICENSE.md.