Introduction

Verity is the Provable Consensus Client — a formally verified Ethereum consensus client built with Lean 4 by Nyx Foundation.

Where other clients test for correctness, Verity proves it. Every line of consensus logic is mathematically proven correct, closing the gap between specification and implementation — permanently.

Verity is currently under active development and has not been released yet.

Why Verity

• Formally verified. Specification drift is structurally impossible; entire bug classes are ruled out before the code ever runs.
• Built in Lean 4. A modern theorem prover and dependently typed language designed for both proofs and programs.
• Aligned with the Ethereum roadmap. Targets the Lean Consensus specification and post-quantum signature schemes.

Where to go next

• Overview — what Verity does and how the pieces fit together.
• Formal Verification — what "proven correct" actually means here.
• Architecture — module map and crate layout.

Design Philosophy

Verity is the Provable Consensus Client. Where other clients test for correctness, Verity proves it. The point of this document is not to list features or pick libraries — it is to state the beliefs that decide every later question. When two reasonable designs compete, the one that keeps Verity provably faithful to the specification wins.

Everything below assumes the ordinary disciplines of good software — small functions, single responsibility, clear naming, simplicity over cleverness. Those are the floor, not the philosophy. What follows is what makes Verity different from a merely well-engineered client.

Why a provable client

Lean Ethereum is a clean-slate redesign of the consensus layer whose explicit goal is to be small enough to reason about completely. The specification is deliberately minimal so that it can be formally verified, not just reviewed. That is a remarkable foundation — but a verifiable specification does not make a correct client. Between the specification and a running binary sits an implementation, and that is where real consensus bugs have always lived: a misread field, an off-by-one in a transition, an aggregation edge case, a panic on malformed input.

Verity exists to close that gap and keep it closed. Its purpose is to carry the guarantees of a verifiable specification all the way into the software that validators actually run, so that the implementation is not merely believed to match the specification but is shown to. This is the single idea from which the rest of the philosophy follows.

Foundational beliefs

These are the convictions that sit above the design principles. They rarely change; the principles are how we honor them.

• leanSpec is the working source of truth — and it moves. leanSpec, the Python reference implementation, is the most authoritative executable definition of Lean Consensus available, and Verity treats it as the practical ground truth for protocol behavior, container shapes, and constants. Where it fixes a shape, Verity matches it exactly: field order and serialization are consensus-critical, because they determine the values that get hashed and signed, so a "harmless" reordering is a consensus fault. But leanSpec is a reference implementation, not a frozen or complete authority. Lean Consensus is still evolving in both its design and its implementation, and leanSpec does not always reflect the latest specification discussions — it can trail the live design debate. Verity therefore tracks leanSpec closely while holding it loosely: it conforms to the current target for interoperability and treats an interop-breaking divergence as a Verity defect rather than a local improvement, yet it follows the upstream design discussions — not only the code — to anticipate where the reference is heading, and it expects breaking change between devnets (backwards compatibility is explicitly not a goal) rather than freezing a convenient snapshot.

• Proof over test. Conformance vectors and interoperability runs are the floor. A passing test suite shows that the cases we thought of work; it says nothing about the cases we did not. Mathematical proof is the ceiling, and it is the standard Verity holds itself to. "Tested correct" and "proven correct" are different claims, and Verity makes the second one wherever it matters.

• Minimalism in service of verifiability. Keeping things small is not an aesthetic preference here; it is a precondition for proof. Every abstraction, generic, and indirection that Verity Consensus must account for widens the surface a proof has to cover and loosens the correspondence between the Rust implementation and its Lean 4 model. So Verity keeps the proven surface as small as the protocol allows, and adds structure only when a real protocol requirement demands it — never in anticipation of one.

• The verification boundary is a first-class part of the architecture — and it moves. Verity is explicit, at all times, about what lives inside Verity Consensus and what lives outside it. The boundary is designed, documented, and defended — not discovered after the fact. Code crossing into Verity Consensus is held to its standard; code outside it exists to feed it clean, well-typed inputs and to carry its outputs to the network. But where the boundary sits is not fixed. As the proof effort matures and the upstream roadmap evolves, components cross it in both directions: serialization may be pulled inside the proven core once it is verified in Lean, and the state transition may be pushed back out toward a zkVM artifact if real-time proving demands a different language. What is invariant is not the placement but the discipline — whatever is inside is held to the proof standard, the boundary is always explicit and defended, and a component's side is decided by the guarantee it currently meets, never assumed permanent. The architecture is therefore designed so that moving a component across the boundary is a re-binding, not a redesign.

Design principles

These follow directly from the beliefs above. Each is stated as a stance, with the reason it serves verifiability.

• Pure, deterministic Verity Consensus. The state transition and fork choice are expressed as pure functions of their inputs, free of hidden state, clocks, locks, or scheduling. Concurrency and input/output are pushed to the edges of the system. A proof can only reason about a deterministic function; the moment consensus logic depends on shared mutable state or task ordering, it stops being something we can fully verify. Keeping Verity Consensus pure is what makes it provable at all.

• Explicitness over cleverness. Verity prefers concrete, named types and straightforward control flow over macro-generated polymorphism and deep generic hierarchies. The implementation should read like the model it corresponds to, so that a reviewer — and a proof — can see the exact shape of every value and the exact obligation at every step. Cleverness that hides structure is a cost paid twice: once when reasoning about the code, and again when aligning it with the Lean 4 model.

• Panic-freedom as a proof contract. A proof about Verity Consensus is worthless if the surrounding program can still abort on unexpected input. Within the verified paths, fallible operations return explicit results rather than crashing, and the runtime is built so that it cannot diverge from the behavior the proof describes. Abrupt termination is treated as a correctness failure, not as an acceptable last resort handled elsewhere.

• Arithmetic that mirrors proven invariants. Numeric operations in the consensus layer respect the same bounds that the Lean 4 model proves. Overflow, underflow, and truncation are not runtime surprises to be caught downstream; they are conditions the model rules out, and the implementation is written so that its arithmetic corresponds one-to-one with those guarantees.

• Reproducibility and supply-chain integrity are part of the proof. A proof about source code says nothing about a binary that cannot be rebuilt from that source or whose dependencies cannot be audited. Verity treats reproducible builds and a disciplined, pinned, auditable dependency set as extensions of the correctness guarantee, not as operational afterthoughts. The chain of trust runs from the specification, through the proof, to the artifact a validator runs — and no link in it is left implicit.

• Conformance through shared evidence. The same specification-derived test vectors feed both the Rust implementation and the Lean 4 model, so the two are exercised against identical inputs and the gap between them stays visible and small. Beyond fixtures, interoperating with other clients on live devnets is the most demanding test of all, and Verity treats passing that gauntlet as the real measure of conformance.

• Post-quantum security is structural. Verity's signatures are hash-based and its aggregation is proof-based, as the protocol requires; this is not an option to be bolted on but a load-bearing part of the design. Secret key material is handled as the sensitive, stateful resource it is — protected in memory and persisted safely — because for a client real validators stake on, getting this wrong is not negotiable.

Alignment with Lean Ethereum

Verity does not invent its goals; it inherits them from Lean Ethereum and commits to them at the level of implementation.

• Security hardening. Lean Ethereum moves consensus to post-quantum, hash-based signatures. Verity treats that migration as structural, as described above.
• Decentralization. Lean Ethereum lowers the barrier to participation so that ordinary stakers can run a validator. Verity's emphasis on a small, reproducible, panic-free client serves the same end: a client that is realistic to run and to trust.
• Rapid finality. Lean Ethereum finalizes in a few slots through its decoupled, layered consensus. Verity implements those finality rules faithfully and treats their safety conditions as inviolable.
• Minimalism. Lean Ethereum keeps the specification small enough to verify. Verity keeps the implementation small enough to verify.

To these four pillars Verity adds a fifth that is its own: provability. Lean Ethereum makes a consensus layer that can be verified; Verity is the client that carries that verification through to running code.

What Verity deliberately rejects

Stating what we will not do is as important as stating what we will, and the existing Rust clients make the trade-offs concrete.

• Macro-generated fork polymorphism that hides structure. Synthesizing many protocol variants from a single declaration is powerful, but the resulting types are hard to read, hard to analyze, and hard to align with a formal model. Verity prefers explicit definitions per concern and shared behavior expressed through clear abstractions.
• Backwards-compatibility shims. Lean Ethereum advances by clean breaks between devnets. Verity does not accumulate compatibility layers for superseded protocol versions; it tracks the current specification and lets old shapes go.
• Treating panics as acceptable. Relying on a global safety net to absorb crashes is incompatible with proving that Verity Consensus cannot crash. Verity does not adopt that posture.
• Floating or unaudited dependencies. Unpinned versions and unreviewed upstreams break the chain of trust between source and artifact. Verity does not accept them.
• Optimization that trades away verifiability. Performance matters, but not at the price of consensus logic we can no longer reason about. Verity optimizes only behind the verification boundary or in ways that preserve the correspondence with the model, and only once a real bottleneck is shown.
• Unbounded resource growth. Queues and buffers without limits turn load into failure. Verity designs for explicit backpressure and bounded resource use rather than assuming the happy path.

A note on KISS, SOLID, and the usual disciplines

These principles are assumed, not argued. Verity keeps functions small, separates concerns, and prefers the simple design — but it does so for a specific reason: simplicity and clear boundaries are what make the verification boundary defensible and the Lean 4 correspondence tight. When a generic best practice and a verifiability concern point in different directions, verifiability decides. The familiar disciplines are the means; a provable client is the end.

Status

Verity is pre-implementation. This document is the north star that the architecture, the crate layout, and every future line of code must answer to. Both Lean Consensus and its reference implementation are still in motion — the protocol's design is under active discussion and leanSpec changes with it — so this document is expected to evolve as the specification advances and as the Lean 4 verification effort teaches us where the real boundaries lie. Its central commitment does not change: the running client is shown to match the specification, not merely believed to.

Overview

This page is a placeholder. Content will be added as the implementation matures.

Planned topics

• What Verity is and what it is not
• Supported networks and devnet roadmap
• Prerequisites (Lean 4 toolchain, Rust toolchain)
• First-run walkthrough

Formal Verification

Verity's headline claim is that the running consensus core is shown to match the specification, not merely believed to. A claim like that is only as strong as its precise form. This page states it precisely: which artifact is proven, against what specification, under which assumptions, and where the guarantee stops.

The specification chain

There is no formal specification upstream. leanSpec — the working source of truth per the design philosophy — is a Python reference implementation, and the Lean Ethereum roadmap's formal-verification track targets cryptographic proof systems (ArkLib), not the consensus protocol. Verity therefore maintains the formal layer itself. The chain from specification to running artifact, with what carries fidelity at each link:

One model, two roles

formal-leanSpec is a single Lean 4 codebase, but its content ships in two different ways — and the distinction is the verification boundary:

• Compiled and exported. The functions that occupy the Verified Core — today the state transition and the fork-choice decision — are compiled by Lean's C backend and exported over the C ABI as Verity Consensus. For these, the theorem and the production code are the same definition: what is proven is what runs.
• Proof-only. The rest of the catalog — validator duties, networking bounds, storage atomicity, the sync FSM — is proven about the model, but the production implementation of those concerns is Rust, in the Runtime Shell and I/O Edge. There the theorem is a design-basis guarantee: it fixes what the Rust must uphold. The model-checking toolchain (Kani, proptest/bolero, Loom, Miri) is what will carry that obligation onto the implementation — it is phased in per the model-checking strategy, not wired in from day one, so until a harness targets a given proposition, that proposition constrains the design but says nothing yet about the running Rust.

Which function sits on which side is a snapshot, not a definition — the same movable-boundary discipline as the architecture: pulling a proof-only function into the export set, or pushing one out, is a re-binding of a capability contract, not a redesign.

The proposition catalog

The unit of proof scope is the proposition: a predicate-form statement extracted from leanSpec, ID-tagged, and proved as a Lean theorem. The catalog lives in formal-leanSpec (docs/lean4-proof-propositions.md) and is the source of truth for what is proven. As of July 2026 it holds 31 propositions across eight domains — 30 proved, one cryptographic axiom, zero sorrys.

The catalog is also where the Partnership with upstream is real, not aspirational: proving VAL-2 exposed that leanSpec documented but never enforced the proposal/attestation key distinction — reported upstream and fixed as leanSpec#1184.

Preconditions are named invariants

The theorems are not unconditional. They are proved relative to explicit well-formedness predicates — Store.WellFormed for the fork-choice store, AnchorWF (discharged by Reachable for every state reachable from genesis) for the state, ValidatorRegistry.WellFormed for validator keys. These predicates are the precise content of the capability contracts' "already-verified inputs": the Runtime Shell owns the mutable store and manufactures the core's inputs, so maintaining these predicates across every mutation is the Rust side's half of the contract — and the primary target for the Kani and property harnesses at the boundary. A theorem about a WellFormed store says nothing about a store the shell has corrupted; keeping the shell honest is what the model-checking strategy is for.

The trust base

What must be trusted for the claim to hold — listed so no link stays implicit:

• The Lean 4 kernel that checks the proofs.
• The transcription. formal-leanSpec is a hand transcription of a Python spec; its fidelity is evidenced (per-file source tracing, review, shared vectors), not proven.
• The predicate mirrors. The well-formedness predicates the theorems assume (Store.WellFormed, AnchorWF, ValidatorRegistry.WellFormed) are Lean definitions; for the Runtime Shell to maintain them — and for the boundary harnesses to target them — they must be hand-transcribed into Rust. That is a second transcription of the same kind as formal-leanSpec itself, and it is held to the same discipline: each Rust mirror cites the Lean definition it mirrors, and shared vectors exercise both sides. A drifted mirror silently voids the boundary checks, which is why this link is listed rather than assumed.
• The Lean runtime's abort path. The compiled artifact embeds the Lean runtime, which can abort the process on allocation failure. This is an availability residue, classed with a Rust-side OOM abort — the panic-freedom claim asserts that no path returns an incorrect consensus value, not that a linked runtime can never abort (see the error model). Exported functions are total, so no other runtime-panic path exists inside the export set.
• The artifact pipeline. Lean's C backend, the generated C, the C compiler and linker, and the runtime the artifact embeds. No tool in the project checks that the static library computes the proven functions.
• Cryptography. hash_tree_root collision resistance is an axiom (SSZ-7); the algebra of Poseidon / KoalaBear and XMSS is ArkLib's domain and enters the model only at call sites; leanMultisig's implementation is trusted in the Runtime Shell.
• The Rust toolchain and shell. rustc, and the Runtime Shell / I/O Edge code — held to the panic-free bar and model checking rather than proof.
• Hardware and OS, under everything.

What is not trusted: the consensus logic itself. Inside the export set, behavior is either proven or it does not ship.

Out of scope — and where it lives instead

• Protocol-level safety and liveness (e.g. accountable safety of the finality gadget) are properties of the protocol design, not of a client's conformance to it. They are pursued in dedicated research repositories — goldfish-fv (the fork choice planned to replace 3SF-mini at pq-devnet-5), minimmit-fv, simplex-fv — and by upstream researchers (fradamt/verified-consensus; ssf-mc's bounded model checking of full 3SF). Verity consumes the protocol; those efforts justify it.
• ZK execution proofs. Proving that one execution of the STF was faithful is complementary to proving the STF correct for all inputs. verifiable-stf prototypes that direction for the Lean-written STF (zkVM verification of Lean IR execution traces); the full tension is recorded in the Ethlambda notes.
• Cryptographic primitive algebra: ArkLib.

Tracking a moving specification

leanSpec moves — breaking changes between devnets are expected, and pq-devnet-5 plans to replace 3SF-mini with committee voting under the Goldfish fork choice. The proof scope is therefore fork-versioned: the model and catalog are pinned to the lstar fork and re-grounded as upstream advances, with the sync discipline visible in formal-leanSpec's history (upstream fixes #1177–#1184 flowed both ways). Minimalism keeps the re-proof cost of a fork change bounded; the movable boundary keeps the change a re-binding.

Lean 4

This page is a placeholder. Content will be added as the implementation matures.

Planned topics

• Why Lean 4 instead of Coq, Isabelle, or Agda
• Relevant tactics and proof patterns used in Verity
• Integration with the Rust runtime: Lean's C backend, static library, C ABI — and why Aeneas is not used
• External references and learning resources

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 contracts if a function leaves for a zkVM artifact, and grows if 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 · leanMultisig"]
        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

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

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; if the state transition leaves Verified Core, its export set shrinks but nothing starts calling 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 leanMultisig (XMSS verify / sign / aggregate).
• verity-db — persistence (Repository): blocks, states, and the finalized anchor, over an embedded key-value store. Keeps the storage concern out of the single-writer aggregate coordinator.
• 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

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; verifiable-stf demonstrates the strongest form of that evidence — the compiled-Lean and compiled-Rust STF produce byte-identical outputs on the same inputs.

• Measurement. Adopting a Lean implementation behind a contract is gated on measured cost, not assumed cost. Two data sets exist 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).
  • verifiable-stf's compiled-Lean vs compiled-Rust STF comparison (RISC-V zkVM cycles, a proxy for relative native cost): 26.1 M vs 12.5 M cycles at N=10 and 35.3 M vs 14.4 M at N=100 — the Lean runtime's one-time Init accounts for ~15 M of the Lean side, so the steady-state Lean overhead is roughly 1.4× Rust once initialization is amortized across a long-lived process.

  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. Two are foreseen, in opposite directions, alongside two partial placements already in the design:

The STF row is not a decision to move it — the working position is that the STF stays in Verity Consensus (Lean 4). It is recorded so the design is shown to withstand the move if the trigger fires; the full tension is in the Ethlambda notes.

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.

Data Representation Across Zones

How Verity represents a value in the host language is not a single decision made once for the whole codebase. It tracks the verification guarantee the value currently lives under. The same protocol quantity — a slot number, a validator index — is a precise, bounded type inside the proven core and a plain machine integer at the unproven edge, with an explicit conversion where the two meet. This page states that policy and the reason it follows from the design philosophy.

This is a consequence of beliefs Verity already holds, not a new rule. It is written down here because it decides the shape of every container and every arithmetic operation that follows.

The principle

Representation precision follows the guarantee. A type that a proof reasons about carries its invariants in the type; a type that only shuttles bytes between the network and the parser does not need to. Because Verity's verification boundary is a first-class, moving part of the architecture rather than a fixed line, the right representation is decided per zone — and is expected to change for a given component when that component crosses the boundary.

In Verity Consensus (the proven core)

Inside the proven core, protocol quantities are concrete, named types, not raw integers. A slot is a Slot, a validator index is a ValidatorIndex, and the two cannot be confused or transposed, because the type system forbids it. This is the same discipline the leanSpec reference applies in Python, where Slot is a distinct subtype of a bounded unsigned integer rather than an alias for it — and Verity holds the proven core to at least that standard.

Two beliefs force this choice:

• Explicitness over cleverness. The implementation must read like the Lean 4 model it corresponds to. The model distinguishes a slot from an index; so does the code. A raw u64 standing for three unrelated quantities loosens exactly the correspondence the proof depends on.
• Arithmetic that mirrors proven invariants. Overflow, underflow, and truncation are conditions the model rules out, not surprises caught downstream. Numeric operations in the core are fallible and explicit where the bound matters, so that the arithmetic corresponds one-to-one with the guarantees the proof discharges. A silently wrapping u64 cannot make that correspondence.

This is also why the core does not lean on macro-generated type machinery to conjure its containers: structure that a macro hides is structure a reviewer and a proof must recover by hand.

At the edges (Runtime Shell / I/O Edge)

Outside the boundary — networking, storage, the RPC surface — none of this applies. Code there exists to feed the core clean, well-typed inputs and to carry its outputs to the network; no proof reasons about its internals. Plain machine integers and a conventional, derive-driven SSZ stack are entirely appropriate, and the edge is free to look like an ordinary high-quality Rust client. Precision here would buy nothing and cost ergonomics.

At the boundary

Values do not drift across the boundary untyped. An input arriving from the edge is validated and converted — promoted — into the core's domain types at the point it enters; a value leaving the core is lowered back to its wire representation on the way out. The boundary is where range checks and well-formedness checks live, so that everything inside the core has already earned its type.

This costs nothing in conformance, because the wire format is independent of the host representation. A Slot newtype and a raw u64 serialize to byte-identical SSZ. leanSpec fixes the serialized shape — field order and encoding are consensus-critical, since they determine what gets hashed and signed — and Verity matches that shape exactly regardless of how richly it types the value in memory. Rich domain types in the core therefore buy proof alignment for free, without moving a single byte on the wire.

Because the boundary moves

The boundary is designed to move: serialization may be pulled into the proven core once it is verified, and a component may be pushed back out if proving demands a different target. Moving a component across is meant to be a re-binding, not a redesign. Representing a boundary-adjacent value in the provable shape from the start is what makes that true — when the component is promoted, its types are already what the core requires, and nothing downstream has to be rewritten to absorb the change.

How the existing clients compare

The Rust Lean clients make the trade-off concrete, and they consistently choose the edge style throughout — because they are uniformly unverified, and because pervasive newtypes in Rust carry real boilerplate. Verity differs only where it must: inside the proven core, where the guarantee changes the calculus.

References for the shapes above: ethlambda's crates/common/types/src/block.rs and checkpoint.rs; ream's crates/common/consensus/lean/src/block.rs and state.rs; leanSpec's src/lean_spec/types/slot.py, uint.py, and checkpoint.py.

The reading is straightforward. The edge style is right for an unverified client and right for Verity's own unproven zones. It is the wrong default for Verity Consensus, where the proof is the product — and there, the leanSpec discipline, or stricter, is the one that pays off. ream's habit of putting collection capacities in the type is the part of the edge style worth carrying inward: a length bound expressed in the type is exactly the kind of invariant the core wants to state once and rely on everywhere.