Formally Verified · Law-Governed · Optimistic Rollup
A Layer 2 whose rules are written as machine-checked law. A single Lean 4 specification — proven with 1,235 theorems — is lowered into an on-chain Solidity settlement layer and an off-chain Rust runtime, and the three stacks are continuously cross-checked to behave byte-for-byte identically.
One specification. Three stacks. Proven to agree.
Most rollups specify their state machine in prose and a reference client, then hope the contracts match. Knomosis turns that around: the protocol is a formal specification. Its entire state-transition function is a small set of named “laws” — written in Lean 4, machine-checked, and mechanically lowered into the code that actually runs on and off chain.
Every change to L2 state is one of 25 named laws — Mint, Transfer, Deposit, Withdraw, Dispute, Freeze, Reward, an AmmSwap, and more. Each law is admissible only under an explicit signature-and-authority policy, and is proven to touch exactly the state it declares — nothing else.
The Lean LegalKernel is the single source of truth. Solidity contracts settle it on L1, a Rust runtime executes it off-chain, and shared “golden” vectors generated from the spec keep all three implementations producing identical bytes.
Sequencers post state roots under bond. Anyone can challenge a bad root, and an interactive bisection game narrows the disagreement down to a single VM step that is re-executed on-chain. Both the convergence and the termination of that game are proved.
The interesting parts are not any single component but how proof, runtime, and contracts are forced to stay in lockstep. Six ideas carry most of the weight.
Lex DSLProtocol rules are authored in Lex, a Lean-embedded DSL with its own grammar, linter, and formatter. Its code generator renders the action types, the transition function, and the CBOR codecs directly into fenced regions of the real sources; a companion diff tool fails the build if hand-written code ever drifts from the spec.
The spec proves properties, not just types: determinism of the transition function, injectivity of every encoder (so state commitments can’t collide), invariant preservation, and resource conservation. Names like applyVerdict_deterministic, apply_admissible_preserves_bridge, and burn_conserves_other_resource are theorems, not tests.
The dispute bisection game is proved to converge and to terminate within a bounded number of rounds (bisection_converges_after_enough_rounds, bisection_terminates_in_at_most_max_depth_rounds). An honest challenger is guaranteed to win in bounded time — a liveness property, not just safety.
Disputes resolve down to one StepVM instruction re-executed on L1 by KnomosisStepVM. State lives in a Sparse Merkle Tree of cells with typed cell proofs, and Lean proves the on-chain step commitment matches the kernel (StepVMCoherence, SolidityStepVMCommit) — so the contract can’t disagree with the proof.
Keccak-256, secp256k1 ECDSA, CBOR, the SMT, the StepVM, and the entire dispute game exist in Lean, Rust, and Solidity at once. Dedicated knomosis-hash-keccak256 and knomosis-verify-secp256k1 crates plus 16 Solidity CrossCheck suites replay shared golden vectors and assert byte-for-byte agreement.
State and wire formats use canonical CBOR. Lean carries roundtrip and injectivity proofs (cborHeadRoundtrip, cborHeadEncode_injective) and an on-chain decoder (CBEDecode.sol) reads the same bytes — so every participant derives exactly the same Merkle roots.
The same protocol is expressed three times, on purpose. Lean proves it, Rust runs it, Solidity settles it — and codegen plus golden vectors keep the lower layers honest. Every block below opens that component in the codebase map.
A law is written once in Lex. Lean checks it and proves its properties, then the Lex code generator emits the matching action types, transition logic, and CBOR codecs into the Rust and Solidity sources. From the proven model the build also exports golden fixtures — step traces, bisection games, withdrawal roots — that the Rust and Solidity test suites replay verbatim.
The result is a closed loop: if any stack computes a different byte than the specification, a cross-check fails. The contracts can’t silently diverge from the proofs, and the runtime can’t silently diverge from the contracts.
Knomosis is optimistic: state roots are accepted unless challenged. What is unusual is that every step of the challenge has a corresponding theorem in the Lean model.
A sequencer posts a new state root through KnomosisStateRootSubmission, backed by a stake held in KnomosisSequencerStake. Optimistically, that root is taken as canonical.
Any party that computes a different root can open a game in KnomosisFaultProofGame. The Rust knomosis-faultproof-observer does this autonomously, following the honest strategy that the spec models in FaultProof.Strategy.
The two sides repeatedly bisect the disputed execution interval. Lean proves this process converges and terminates in at most the configured maximum depth, so it cannot stall or run forever.
The game lands on a single instruction. KnomosisStepVM re-executes it against Merkle cell proofs of exactly the state it reads and writes. Because the Lean and on-chain StepVMs are proven coherent, this re-execution is the ground truth.
KnomosisDisputeVerifier applies the verdict. The dishonest party’s bond is slashed and the honest challenger is rewarded under a DisputeRewardPolicy. Crucially, applyVerdict_deterministic and applyVerdict_rejected_no_change prove the outcome is reproducible and that a rejected challenge changes nothing else.
Determinism means every honest node computes the same step, so there is always a single correct answer to dispute toward. Injective encoding means two different states can never share a commitment, so a fraudulent root can’t hide behind a hash collision. Bounded termination means an honest challenger always wins within a fixed number of rounds. And StepVM coherence means the contract’s verdict is exactly the specification’s verdict.
Three codemaps are bundled with the site, one per language scope. Open any of them in the adaptive navigator to follow dependencies and call graphs derived directly from the source.
The specification and its proofs: the LegalKernel, the 25 laws, the fault-proof model, and the Lex DSL across the **/*.lean sources.
303 modules · 5,063 declarations · 1,235 theorems
The runtime and benchmarking crates: the host, the L1 ingest pipeline, the fault-proof observer, the indexer, and the cross-checked primitives across **/*.rs.
137 modules · 4,617 declarations · 11 crates
The on-chain settlement layer: the bridge, sequencer staking, the fault-proof game, the StepVM, and the SMT/CBOR libraries across **/*.sol.
83 modules · 1,856 declarations · 11 contracts
Choose a codebase from the toolbar, then search or click to select a module. The selected module sits in the center lane; the modules it depends on appear on the left and the modules that depend on it appear on the right. The interior menu lists every declaration in the module, grouped by kind. Click a declaration to switch into its own call graph, and use the breadcrumb to return.
Counts above reflect the bundled snapshot; the viewer always shows live statistics for the selected codebase.