architecture.md

title	Verity Architecture
last_updated	2026-08-26
tags	architecture verification-boundary crate-layout storage

Verity Architecture

Status: pre-implementation. This document captures the architectural intent derived from the Design Philosophy. No Lean or Rust source exists yet.

Verity is a provable consensus client: the verified Lean 4 Verity Consensus implementation wrapped in a Rust runtime. That two-language split makes Verity structurally different from single-language clients, so its first-class architectural axis is the verification boundary — what is inside the proven consensus implementation and what is outside it. Everything else, including the concurrency model, follows from that axis.

The architecture is organized into three concentric zones, drawn from the proven consensus implementation outward. A zone is defined by the guarantee level it holds code to — proven-pure, trusted-and-panic-free, or concurrent-IO — not by the specific components that happen to occupy it today. Which component sits in which zone is a current snapshot, expected to change as the verification frontier moves; see boundary migration.

Day-one snapshot — Rust-first. Implementation starts Rust-first (kickoff decision, 2026-07-22): at kickoff every capability contract is bound to its native-Rust implementation, the verity-consensus-sys export set is empty, and no FFI call is made. Lean-compiled logic is adopted per capability later — stable, proved, and measured-within-budget first; the state transition and fork choice last, because they track a volatile upstream spec. The zone diagrams and the inbound-block sequence below therefore show the target state, with Verity Consensus occupying the Verified Core; on day one the same functions run as native Rust in the Runtime Shell, behind the same contracts.

Zones

• Verified Core — Verity Consensus (Lean 4, pure). The proven-pure zone: pure, total functions only — no hidden state, clocks, locks, or scheduling. This is the surface that Lean proofs defend. Its source is the formal-leanSpec Lean 4 model, compiled via Lean's C backend into a static library and exposed to Rust over a C ABI (no Aeneas) — see Formal Verification for the one-model, two-roles split between compiled-and-exported functions and proof-only propositions. Its current occupants are deliberately minimal — only the state transition and the fork-choice transition functions — but that export set is a snapshot, not a definition: it grows as a function (e.g. hash_tree_root) is verified in Lean and pulled in.

• Runtime Shell — Rust, panic-free. The trusted, panic-free zone. Manufactures clean, typed, already-verified inputs for Verity Consensus, owns the consensus state and fork-choice view as a single writer, and threads immutable values through Verity Consensus. Proofs do not reach here, so it is held to the language-level bar instead: memory-safe, strongly typed, and panic-free. Today, SSZ / hash_tree_root and signature verification are realized here as native-Rust implementations of their capability contracts, so Verity Consensus receives precomputed roots and verified signatures rather than recomputing or trusting them itself. That is a placement, not a contract: were a Lean-verified serialization to satisfy the same contract across the FFI seam, Verified Core would compute those roots itself and Runtime Shell's consumers would not change.

• I/O Edge — Rust, concurrent. The only place where concurrency and the outside world live: networking, the slot clock, validator duties, RPC, metrics, and node orchestration. Bounded queues provide backpressure. The choice of concurrency primitive (actor model vs. async tasks) is a later, I/O-Edge-internal decision — it is not an architectural concern, because the consensus state has a single owner in Runtime Shell and Verity Consensus is invoked sequentially regardless.

Component diagram

flowchart TB
    subgraph C["I/O Edge — Rust, concurrent"]
        direction LR
        NET["P2P networking<br/>gossipsub · req/resp"]
        CLK["Slot clock / ticker"]
        VAL["Validator duties<br/>produce · sign · aggregate"]
        RPC["RPC / HTTP API"]
        MET["Metrics<br/>verity-metrics"]
        ORCH["Node orchestrator<br/>lifecycle · bounded queues"]
    end

    subgraph B["Runtime Shell — Rust, panic-free"]
        direction LR
        CODEC["SSZ codec + hash_tree_root<br/>wire bytes ↔ typed values"]
        CRYPTO["Signature verification<br/>verity-crypto: XMSS · leanVM"]
        STORE["State + fork-choice store<br/>single writer · threads immutable values"]
        DB["Database<br/>blocks · states · anchor"]
        FFI["FFI bindings layer"]
    end

    subgraph A["Verified Core · Verity Consensus — Lean 4, pure"]
        direction LR
        STF["State transition<br/>process_slots · process_block"]
        FC["Fork choice<br/>on_block · on_vote · get_head"]
    end

    NET -->|"raw bytes"| CODEC
    CODEC -->|"typed + roots"| CRYPTO
    CRYPTO -->|"verified inputs"| STORE
    CLK --> ORCH --> STORE
    STORE <-->|"immutable values"| FFI
    FFI ==>|"C ABI · Lean C backend"| STF
    FFI ==>|"C ABI"| FC
    STORE --> DB
    STORE -->|"head / state"| VAL
    STORE -->|"head / state"| RPC
    STORE -->|"head / state"| MET
    VAL -->|"signed block/vote"| CODEC

Loading

Inbound block — crossing the boundary

The boundary crossing over time, for a block arriving from a peer. Decoding, root computation, and signature verification all complete in Runtime Shell before Verity Consensus is touched, so each FFI call into Verity Consensus receives only clean, typed, verified values.

sequenceDiagram
    participant P as Peer
    participant N as Network (C)
    participant K as Codec + Crypto (B)
    participant S as Store (B)
    participant L as Verity Consensus (A)
    participant D as DB (B)
    P->>N: gossip block (bytes)
    N->>K: SSZ decode + hash_tree_root
    K->>K: verify XMSS / aggregate signatures
    K->>S: verified, typed block (+ roots)
    S->>L: process_block(state, block)  [FFI]
    L-->>S: new state
    S->>L: on_block(view, block)  [FFI]
    L-->>S: new view
    S->>L: get_head(view)  [FFI]
    L-->>S: head root
    S->>D: persist block + state

Loading

Crate layout

This layout is the target shape, not the day-one scaffold. Implementation starts with a single verity-consensus crate (kickoff decision, 2026-07-22): the zone boundaries below begin as module boundaries inside that crate, holding the same inward invariant, and split into separate crates only when a second crate earns its existence. The workspace description that follows is what that split grows into.

The Rust runtime is a Cargo workspace. Crates map onto the zones, and calls and dependencies flow inward, from higher-effect / lower-assurance toward lower-effect / higher-assurance — Verified Core never calls outward. Today that ordering reads I/O Edge → Runtime Shell → Verified Core over the current crate snapshot, and the compiler enforces it rather than discipline. The invariant is stated over guarantee levels, not crate identities, so it survives migration: if hash_tree_root moves into Verified Core, verity-types (Runtime Shell) calls inward to Verified Core for it — still Runtime Shell → Verified Core, still legal, with the export set growing but nothing starting to call outward. Names follow the existing verity-* convention (verity-crypto, verity-metrics); the sole exception is the FFI bindings crate, which follows its upstream Lean library name per Rust's -sys convention.

Crates Verity must build itself

• verity-types — consensus container definitions (Block, State, Vote, …) and constants. The Serialization capability (SSZ encode / decode, hash_tree_root) is currently satisfied by an external SSZ library behind an adapter in Runtime Shell; the contract (typed value ↔ bytes / root) is stable whether that implementation is the external Rust library or a Lean implementation reached over FFI. Foundational; depended on by every other crate.
• verity-consensus-sys — raw FFI bindings to Verity Consensus, which is built and proven in formal-leanSpec and consumed here as a static library: Verity Consensus is the compiled, exported subset of that repository's Lean model — the intended mechanism is a dedicated export target (VerityConsensus) holding the @[export] wrappers over the model. Confines all unsafe. Named after that export target. It is the swappable backend behind the capability contracts: its exported function set is exactly whatever Verified Core currently hosts, and is expected to expand or contract as the frontier moves.
• verity-chain — the single writer that owns the consensus state and the fork-choice store, and coordinates the State and Store aggregates under one consistency boundary. The only caller of Verity Consensus; wraps verity-consensus-sys behind a safe API. Reads and writes through verity-db.
• verity-validator — validator duties (production only): block and vote production, signing, and aggregation.
• verity (binary) — the executable validators run: orchestrator, slot clock, wiring, backpressure.

Thin glue over existing libraries

• verity-p2p — gossip and req/resp over libp2p.
• verity-crypto — adapter over the two upstream signature libraries: leansig for per-validator XMSS sign / verify, and leanVM (formerly leanMultisig) for aggregation and aggregate-proof verification. One capability contract, two suppliers behind it.
• verity-db — persistence (Repository): blocks, states, aggregate proofs, and the finalized anchor. Keeps the storage concern out of the single-writer aggregate coordinator. See Storage engine and retention.
• verity-rpc — HTTP API surface.
• verity-metrics — implementation of the leanMetrics contract.

Layer mapping: Verified Core = Verity Consensus (the compiled export subset of formal-leanSpec, not a Cargo crate); Runtime Shell = verity-consensus-sys, verity-types, verity-chain, verity-crypto, verity-db; I/O Edge = verity-p2p, verity-validator, verity-rpc, verity-metrics, verity (binary).

flowchart TB
    subgraph ZC["I/O Edge"]
        BIN["verity (bin)"]
        VAL["verity-validator"]
        RPC["verity-rpc"]
        MET["verity-metrics"]
        P2P["verity-p2p"]
    end
    subgraph ZB["Runtime Shell"]
        CHAIN["verity-chain"]
        CRYPTO["verity-crypto"]
        DB["verity-db"]
        TYPES["verity-types"]
        SYS["verity-consensus-sys"]
    end
    subgraph ZA["Verified Core · Verity Consensus"]
        LEAN["Verity Consensus<br/>(Lean repo)"]
    end
    BIN --> VAL
    BIN --> RPC
    BIN --> MET
    BIN --> P2P
    BIN --> CHAIN
    VAL --> CHAIN
    VAL --> CRYPTO
    RPC --> CHAIN
    MET --> CHAIN
    P2P --> CHAIN
    CHAIN --> SYS
    SYS ==> LEAN
    CHAIN --> DB
    CHAIN --> TYPES
    CRYPTO --> TYPES
    DB --> TYPES

Loading

Storage engine and retention

verity-db stores two workloads with opposite shapes, and the split drives every decision below. Sizes are measured from leanSpec's fixtures-prod-scheme.tar.gz release asset; at SECONDS_PER_SLOT = 4 a day is 21,600 slots. The table layout that follows from these decisions — keys, pruning rules, and the snapshot/diff scheme for state — is in Storage Schema.

Workload	Value size	Volume	Lifetime
Blocks, states, indices, finalized anchor	~100 B – 800 B	~5 MB/day	permanent
Aggregate proofs (MultiMessageAggregate)	155–236 KB, median 190 KB	~4.1 GB/day	pruned after ~1 day

Engine: RocksDB. The proof workload — six-figure-byte values written continuously and dropped en masse a day later — is what an LSM tree with range tombstones is built for, and the same choice is what ethlambda, zeam, and qlean-mini run (gean uses Pebble, the same family). The cost is a C++ dependency in the runtime's build and trust surface; that cost is accepted for Runtime Shell, where the bar is memory-safe, panic-free Rust around a well-exercised store, not proof. It buys nothing in Verified Core and reaches nothing there.

Backend trait. Storage sits behind a backend trait with an in-memory implementation alongside the RocksDB one, following ethlambda's StorageBackend split. Tests and ephemeral nodes run in-memory; the engine stays replaceable if the proof workload later moves out of the database. Anything that leaks one engine's semantics into the trait — range deletes above all — is documented at the trait, not assumed.

Proof retention: 21,600 slots (~1 day). Proofs live in their own table keyed slot ‖ root, so pruning is a slot-ordered range delete rather than a scan. They are dropped only below tip_slot − 21,600 and only when that cutoff is already finalized; non-finalized proofs are never touched. Blocks and states are never pruned by this path.

The floor is not ours to choose: leanSpec sets MIN_SLOTS_FOR_BLOCK_REQUESTS = 3600 (4 hours) and a responder MUST serve BlocksByRange over that window. Everything above it is an operational choice about how far behind a peer can fall and still catch up over P2P instead of needing a checkpoint. One day is that horizon — a node down overnight rejoins by range sync — at 6× the mandated floor. Note that leanSpec's own reference node satisfies the requirement in memory and persists no proofs at all; Verity persists them so the guarantee survives a restart.

Capability contracts

The Verified Core ↔ Runtime Shell boundary is expressed not as a fixed list of FFI functions but as a small set of capability contracts — Rust-side interfaces (traits), one per consensus capability that could be realized on either side of the proof boundary:

• StateTransition — state_transition(pre_state, verified_block) -> Result<post_state>
• ForkChoiceDecision — the pure decision: fork_choice_decision(view) -> head / safe_target / updated view
• Serialization / HashTreeRoot — hash_tree_root(value) -> root, encode / decode
• SignatureVerification — verify aggregate (Type-1 / Type-2) proofs

Each contract admits two implementations: a native-Rust implementation (the capability lives in Runtime Shell) or an FFI-into-Lean implementation provided by verity-consensus-sys (the capability lives in Verified Core). Consumers such as verity-chain depend only on the contract and never learn whether it is Lean-backed. Which side hosts a capability is therefore the combination of: (a) which implementation is bound — a wiring decision in the verity binary, constrained by what is actually proven; (b) where the proof obligation sits; and (c) whether that capability's functions appear in the verity-consensus-sys export set.

Error model. Failure is part of the contract, in two strictly separated layers:

• Protocol rejection (an invalid block) is a value. In the Lean model it is a pure Except-style result; in the contract it is the Err arm of the shared Result. The error type is a plain enum (ProcessingError), defined in the contract crate alongside the traits, so the native-Rust and FFI-into-Lean implementations return the same type and a migration leaves the error path untouched. At the C ABI the FFI implementation uses the conventional shape — an int32 status code plus an out-parameter for the result — with the status codes in one-to-one correspondence with the Lean model's rejection reasons; that correspondence table is kept next to the Lean definition it mirrors, and the code→enum conversion is confined to verity-consensus-sys. Rejection reasons are a small closed set (the Runtime Shell delivers already-verified inputs, so FFI-level rejection is rare by design), which is why a code enum suffices and no structured error payload crosses the ABI.
• Runtime failure (Lean runtime allocation failure) is not a value and is not modeled in the contract. The Lean runtime can abort the process on allocation failure, and Verity designs on the assumption that this cannot be hooked. Such an abort is classed with a Rust-side OOM abort: an availability failure, not a safety failure. The panic-freedom claim is precise on this point — it asserts that no code path returns an incorrect consensus value, not that a linked runtime can never abort; the residual abort condition is listed in the trust base.

The contracts' "already-verified inputs" clause has concrete, named content: formal-leanSpec's theorems are proved relative to explicit well-formedness predicates — Store.WellFormed for the fork-choice store, AnchorWF (discharged by Reachable) for the state, and ValidatorRegistry.WellFormed for validator keys. Maintaining those predicates across every mutation is Runtime Shell's half of the contract: Verified Core's theorems speak only about inputs that satisfy them, so the single writer must preserve them, and the boundary harnesses target exactly them (see the Model-Checking Strategy).

The contracts must be defined inner to both their consumers and their implementations — otherwise verity-consensus-sys implementing a contract defined in verity-chain would force a sys → chain edge and break the inward invariant. The recommended home is a thin contract crate (e.g. verity-consensus-api) holding only the trait definitions — the minimal expression of a movable boundary; folding them into verity-types is the alternative but mixes container shape with capability behavior. The final crate placement is an implementation-time decision; what matters architecturally is that the boundary is a contract, not a hardcoded call site.

Settled (kickoff decision, 2026-07-22). Proposer selection lives chain-side — a pure function next to the state transition and fork choice, not a verity-validator concern. Like everything else it starts as native Rust, and its pure-function shape keeps it a candidate for later adoption into the Verified Core.

Open for discussion. Whether duty scheduling, signing, and aggregation should be separate crates rather than folded into verity-validator once the workspace split happens.

The FFI seam — marshalling cost and verification

When a contract is bound FFI-into-Lean, every call marshals its inputs across the C ABI: the Rust value is promoted into the Lean object representation on the way in and the result lowered back on the way out. For StateTransition and ForkChoiceDecision that means the full state or fork-choice view crosses the seam per call. This layer deserves explicit attention, because it is the weakest trusted link in the whole chain: the Lean theorems stop at Lean values, so a conversion bug (a transposed field, an endianness slip, a truncated list) makes the proven function compute correctly on the wrong input — and no proof, on either side, can see it.

Two obligations follow:

• Verification. The promote/lower code is boundary code in the Runtime Shell and is the primary target of the boundary harnesses (round-trip properties, no-panic-on-any-input, range enforcement — see the Model-Checking Strategy). Cross-language behavioral equivalence is additionally evidenced by shared leanSpec vectors run on both sides.
• Measurement. Adopting a Lean implementation behind a contract is gated on measured cost, not assumed cost. One data set exists today: leanSSZ's C ABI PoC (Rust-caller round-trip and hash_tree_root match): STF+HTR 27.5 ms at V=4096, within budget; per-op on a ~526 KB state, serialize 33 ms / hash_tree_root 58 ms / deserialize 54 ms (list-based codec, uncached merkleization). These numbers are inputs to the migration triggers below: a capability moves into the Verified Core only when its measured seam cost fits the slot-time budget.

Interchange shape — a conditional design, not an adoption decision. Nothing here decides whether any capability is bound to Lean — that remains gated per capability (stable, proved, measured-within-budget). What is fixed now is only the shape the seam takes if a binding happens, so that a future adoption is a re-binding rather than a redesign:

• Long-lived values stay resident. The consensus state and fork-choice view do not round-trip per call. The Rust side holds an opaque handle to a Lean-resident value (process_block(state_handle, block) -> new_state_handle), which fits Lean's immutable, reference-counted values and eliminates the per-call state marshalling cost entirely. The single-writer discipline makes ownership simple: the store is the only holder. Persistence and crash recovery are defined by SSZ export/import at the DB, not by the handle.
• Inputs cross as SSZ bytes, decoded by the callee. Per-call inputs (blocks, votes) are passed in their SSZ wire form and decoded on the Lean side. This deliberately avoids constructing Lean objects field-by-field from Rust (lean_alloc_ctor-style), which would couple the shell to the Lean object layout and concentrate unsafe exactly where a conversion bug is least detectable. Bytes-as-interchange means the conversion is the consensus-critical wire format itself — already fixture-tested on both sides — and, if the Lean side ever ships a proven decoder, the Lean half of the seam becomes proven code.

Field-by-field construction is not banned outright; it is the last resort, admitted only where measurement shows the byte path cannot fit the budget.

Boundary migration

Because a zone is a guarantee level and placement is a snapshot, components are expected to cross the Verified Core ↔ Runtime Shell boundary over the life of the project — the verification boundary moves. The capability contracts are what make this affordable: a migration is a re-binding plus a move of the proof obligation, not a redesign.

Cost model — what a migration touches, and what it must not. A migration may change:

• which implementation is bound behind the capability contract (native-Rust ↔ FFI-into-Lean);
• where the proof obligation sits (a Lean proof vs. a language-level / external-library guarantee);
• the verity-consensus-sys export set (it grows or shrinks);
• which crate the implementation lives in.

A migration must not change:

• consumer code (verity-chain, verity-validator) — it depends on the contract, not the placement;
• consensus container shapes (the verity-types shared model) — shape is separable from the serialization behavior that may move (see the Domain Model);
• the zone definitions (the guarantee levels);
• the inward invariant (calls still flow toward higher assurance; Verified Core still never calls outward).

Anticipated migrations. One is foreseen — inward — alongside two partial placements already in the design:

Capability	Today	Anticipated move	Trigger	Effect
SSZ / hash_tree_root	Runtime Shell	Runtime Shell → Verified Core	A Lean-verified merkleization becomes available	Verified Core computes its own roots; "Verity Consensus receives precomputed roots" no longer holds; verity-types calls inward to Verified Core for the Serialization contract
Fork choice	Verified Core (decision) + Runtime Shell (Store)	—	—	The worked example of a capability split across the boundary: a pure decision in Verified Core over a mutable Store owned in Runtime Shell
Proposer selection	Runtime Shell (pure function, chain-side)	Runtime Shell → Verified Core (candidate)	Verified in Lean and pulled into the export set	Same pattern as SSZ: a pure decision whose shape is already what the core requires

Notes

• What "proven" means — the artifact chain, the proposition catalog, and the trust base — is defined in Formal Verification.
• Function names in the diagrams (process_block, on_block, get_head, …) are indicative and will be reconciled with leanSpec (lstar HEAD) when implementation begins.