Verity
Formally verified smart contracts. Mathematical certainty across all inputs and execution paths. Betting that agents will make full formal verification practical. Vires in Numeris.
Install / Use
/learn @lfglabs-dev/VerityREADME
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 exists for the current explicit supported fragment, and its function-level closure now runs by theorem rather than axiom. All Layer 2 proof scripts are fully proved (0 sorry); see docs/VERIFICATION_STATUS.md. The theorem surface explicitly assumes normalized transaction-context fields. Follow-on work in #1510 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 are currently 2 documented Lean axioms in total: the selector axiom and 1 mapping-slot range 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:
-
Link external Yul libraries (e.g., Poseidon hash) at compile time:
lake exe verity-compiler --link examples/external-libs/PoseidonT3.yul -o artifacts/yulThe linked library's correctness is a trust assumption. See examples/external-libs/.
-
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 packag
