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,768 theorems — is mirrored by 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 mirrored by the code that actually runs on and off chain.
Every change to L2 state is one of 25 named laws — Transfer, Mint, Deposit, Withdraw, Dispute, Freeze, Reward, a ReserveSwap, 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 commit batched state roots under an ETH bond. Anyone can challenge a bad root within the dispute window, 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. Eight 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, codecs, and event extractors into fenced regions of the Lean sources, and CI re-runs it in --check mode — the build fails if a generated region or the canonical law manifest 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 trusted core is two files, and kernel theorems rest on no custom axioms — only Lean’s three built-ins.
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 KnomosisStepVMRoot. 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, a knomosis-cross-stack fixture loader, and 22 Solidity CrossCheck suites replay shared golden vectors and assert byte-for-byte agreement.
State and wire formats use canonical CBOR (“CBE”). 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.
Gas can be funded in ETH or in Liquity V2’s BOLD stablecoin, flowing through one unified pool; an embedded constant-product AMM prices the ReserveSwap law. The BOLD leg is defensively hardened — a per-currency circuit breaker with a permissionless depeg auto-trigger, a TVL cap, and a one-way AMM kill switch behind a 3-of-N multisig — and none of those controls can move funds or halt withdrawals.
Actions are signed as EIP-712 typed data, and SignInput.sol recomputes the exact L2 signing digest on L1 — a wallet signature means the same thing in every stack. The knomosis-gateway crate serves a browser-facing HTTP/JSON + SSE API with native HTTPS/mTLS and an add-network /rpc shim, so wallets join chain 8357 (test: 83572) and sign L2 actions directly.
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 elaborates it and proves its properties, and the Lex code generator renders the matching action types, codecs, and event extractors into fenced regions of the Lean sources — re-checked in CI so nothing drifts. From the proven model the build exports golden fixtures — step traces, bisection games, deposit and withdrawal roots — that the Rust and Solidity mirrors replay verbatim, and scheduled CI lanes link the production keccak-256 and secp256k1 adaptors to prove Lean↔EVM byte-equivalence.
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 the state root for a whole batch of L2 log entries through KnomosisStateRootSubmission, staking an ETH bond with each submission — batching is what makes the per-action L1 cost a fraction of a submission. Unless challenged inside the dispute window, the root finalises 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. KnomosisStepVMRoot 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.
The game settles: the loser’s bond funds the winner’s reward (less a small treasury share), and on a challenger win the rollback is driven through KnomosisDisputeVerifierV2 into the bridge’s fund-safety gates. 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.
346 modules · 6,064 declarations · 1,768 theorems
The runtime and benchmarking crates: the host, the L1 ingest pipeline, the fault-proof observer, the indexer, the browser-facing gateway, and the cross-checked primitives across **/*.rs.
194 modules · 6,277 declarations · 14 crates
The on-chain settlement layer: the bridge and gas pool, sequencer staking, the fault-proof game, the StepVM, and the SMT/CBE libraries across **/*.sol.
107 modules · 2,182 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 (Knomosis v0.14.1); the viewer always shows live statistics for the selected codebase.