Verify it
This page says exactly what "verified" means on this site — no more, no less. dregg's semantics are a Lean 4 kernel, and its guarantees are theorems about that kernel, each machine-pinned to the Lean kernel's three axioms. The same kernel the theorems are about is the executor the node runs. You do not have to take any of this on faith: every claim below links the thing you would check, and the catalogs on this page are generated from the proof sources at build time — the site build fails if they drift.
Why this matters: most systems ask you to trust that the code matches the whitepaper and the deployment matches the code. Here the chain is shorter — the proof is about the artifact that runs, and a light client can check a whole history against one root without trusting any executor, including ours. The named foil is the pale ghost: a server presenting a plausible state it never legitimately produced. The architecture exists so that ghost cannot fool a light client — that is the unfoolability guarantee below.
Unfoolability — ARGUS and the pale ghost
The deepest guarantee is not "some valid state exists" — it is that the circuit witnesses the protocol's correct evolution, so a light client cannot be fooled about what actually happened. This is the ARGUS architecture, and it is what makes the pale ghost impossible.
verify(agg.root) and learns that every turn executed correctly, the chain is correctly ordered (no drop, insert, or reorder), and the final root is the genuine fold of the whole history — conjoined with conservation derived from verification, with no prover-supplied state-continuity hypothesis. The apex is light_client_verifies_whole_history plus conserves_from_verification.
False, so no verifying aggregate exists for it (tampered_aggregate_cannot_bind). Positional pairing means a verifying leaf cannot be re-pointed to a different step. The fooling game is reduced to breaking the named crypto floor — and is therefore impossible under it.
new_root[i] = old_root[i+1]), and a light client seeing only the matching roots learns the adjacent kernels coincide — state-equality, not merely commitment-equality. The proof rotation keeps the cost down without breaking the binding.
What the badge in the explorer means
Objects in the explorer and
playground carry a verification status. It is never
hand-set: a receipt's witness status comes from actually checking the witness bundle,
and a proof's trust tier names which proving path produced it — a real STARK from the
effect VM, or an honest placeholder label where a surface seeded local data
without proving it. A theorem badge in the Studio comes from Lean's own axiom audit
(#assert_axioms), not from a list someone typed. When something is not
proven, the badge says so; that honesty is the feature.
What is proven
The assurance case is organized by guarantee in Dregg2/AssuranceCase.lean:
each names an apex theorem and the keystones that discharge it. Generated from that
file:
A AUTHORITY
Every state change is justified by an unforgeable, non-amplified, fresh token chain.
apex: authority_guarantee · 19 axiom pins
floor: ed25519 (signature on the handoff), HMAC (caveat-chain tags), Poseidon2-CR (in-circuit cap-root openings). No trusted "this was authorized" premise survives.
B CONSERVATION
Per asset, the resource sum is IDENTICALLY ZERO — on every reachable state, always.
apex: conservation_guarantee · 23 axiom pins
floor: NONE beyond integer arithmetic. Conservation is a kernel theorem; the only crypto that touches it is Pedersen (DLog) IF values are committed rather than cleartext, and the case proves committed = cleartext via Spec.committed_iff_cleartext. DEPLOYMENT CORRESPONDENCE (named, not closed — the theorem's hypothesis vs the running node): reachable_total_zero quantifies over states reachable from a VALUE-EMPTY genesis (GenesisState: bal ≡ 0; live cells may pre-exist, value may not). Two deployed paths are TODAY outside that hypothesis, and this case does not claim them: 1. **Devnet genesis seeding** — node/src/genesis.rs mints the faucet (1,000,000) and demo agents (alice/bob/carol) with positive balances and NO issuer well carrying −supply, so the deployed genesis is not value-empty in the model's sense. The W1-faithful fix is to seed via issuer-moves from a genesis issuer cell (then genesis Σ=0 holds by construction). 2. **The legacy atomic-path fee epilogue** — turn/src/executor/atomic.rs (the fee deduct in execute_atomic) debits atomic_turn.fee from the agent with no crediting move: a burn OUTSIDE the issuer-move discipline (DREGG3 staged item: fees become moves to wells). Until both are reshaped, conservation_guarantee is a theorem about the kernel the node RUNS (execFullTurnA — every committed transaction preserves Σ exactly) but the deployed CHAIN's Σ is offset by its genesis seed and decremented by legacy fees. Reported here so the spec SAYS what it covers; the closure lane is the genesis/fee reshape, not a caveat to carry.
C INTEGRITY
A receipt binds the WHOLE post-state; a tampered input is rejected.
apex: integrity_guarantee · 24 axiom pins
floor: Poseidon2-permutation-CR (the recStateCommit/cellCommit/stateCommit injectivity portals reduce to it; the MMR discharge rests on the SAME Poseidon2SpongeCR). A second pre-image would be the only way to forge a receipt for a different state; that is exactly the CR assumption.
D FRESHNESS
No replay / double-spend; a committed spend's nullifier was fresh; revocation at finality.
apex: freshness_guarantee · 12 axiom pins
floor: Poseidon2-CR (the nullifier-set sorted-tree root openings). PostGSTProgress for the revocation-at-finality leg (consensus terminates after GST). KNOWN RESIDUAL (named, out-of-model): the node's MCP gateway binds biscuit-cap temporal caveats to the live attested consensus height (node/src/mcp.rs McpCapContext.block_height) — the height-expiry leg is real — but consults NO revocation registry for MCP-issued biscuit caps (the gateway's own doc names this). An MCP cap dies only by expiry caveat, never by explicit revocation, until a revocation feed is wired. That path is OUTSIDE this guarantee's statement; it is listed here so the case says so rather than implying coverage.
E UNFOOLABILITY
A light client verifying a Q-chain learns A–D for the WHOLE history; re-witnessing nothing.
apex: unfoolability_guarantee · 22 axiom pins
floor: FRI / STARK soundness (EngineSound.recursive_sound, the ONE recursion obligation), Poseidon2-CR (recStateCommit binds the seam roots), ed25519 (strand-block signatures), PostGSTProgress (a FINALIZED — not merely valid — chain, via the finality-cert leg).
R THE RUNNING ENTRY (A∧B∧C hold over what the node actually runs)
The five guarantees above are stated over the abstract kernel: the List Auth attenuation lattice (A), the multi-asset ledger recTransferBal (B), the Argus term IR (C/D), the aggregation fold (E). The honest question ember keeps pressing is: *do those guarantees hold over the executor the deployed node INVOKES* — execFullForestG, the body behind the dregg_exec_full_forest_auth FFI export (Exec.FFI), the one produce_via_lean / lean_shadow call? They do, and this section proves it in ONE statement rather than leaving it as a reader's inference.
apex: running_entry_sound · 8 axiom pins
floor: unchanged from A–C.
#assert_axioms pins,
generated from Dregg2/AssuranceCase.lean. Every pinned theorem rests on the Lean kernel
triple {propext, Classical.choice, Quot.sound} and nothing else.The proofs are about the node, not a model of it
The strongest thing this page can say: the guarantees above are not about a paper
abstraction. The node's state producer is the verified Lean function
execFullForestG — credential- and caveat-gated, proven sound — compiled and
linked into the node over a C ABI (dregg-lean-ffi/). It is not a model of
what the node does; it is the function the node calls. So Authority, Conservation and
Integrity hold over execution itself. One theorem, running_entry_sound,
proves over that exact function: conservation with no zero-net side condition, no
amplification on every delegation edge, and per-node credential + caveat attestation —
with fail-closed teeth (an unauthorized turn does not execute). A running node will tell
you the same fact about itself:
curl -s https://devnet.dregg.fg-goose.online/status
# → "state_producer":"lean", "lean_producer":true, "full_turn_proving":trueAnd the integrity guarantee's load-bearing leg is constructive: the executor is a memory program. Every kernel field and the receipt log project onto one domain-tagged address space, and the executor's post-state equals the fold of the verb's emitted memory trace over the pre-state. "The receipt binds the whole post-state" is therefore a fact with a witness, not an assertion — every field has a universal address, and nothing is left off the map.
What it rests on
No proof rests on nothing. These are the only out-of-kernel carriers any guarantee depends on — they enter as explicit hypotheses, never as axioms, and there are no others:
- Poseidon2-permutation collision-resistance — the arithmetization-friendly hash; the sponge/Merkle/state-commitment/MMR collision-resistance is reduced to permutation-CR (
Crypto.Poseidon2*,Crypto.Merkle, therecStateCommitinjectivity portal, the receipt-indexLightclient.MMR.mroot_binds_position, and the sorted-set/queueApps.QueueRoot.RootCR/LenBindCRand identity-keysetApps.PreRotation.KeySetCRcarriers — every one a named CRPropover aPoseidon2/BLAKE3image, NOT anaxiom). - BLAKE3 collision-resistance — the out-of-circuit content/transcript hash.
- ed25519 EUF-CMA — turn / strand-block signature unforgeability.
- HMAC (PRF/MAC) unforgeability — macaroon caveat-chain tags (
Authority.CaveatChain). - AEAD confidentiality+integrity — sealed-value / disclosure payloads.
- Discrete-log hardness — Pedersen value commitments (
Crypto.Pedersen). - FRI / the STARK soundness chain — a verifying proof attests its statement; the one recursion obligation
RecursiveAggregation.EngineSound.recursive_sound. - PostGSTProgress — the network is eventually synchronous (after GST); the consensus LIVENESS carrier (
World.gst_liveness, derived from a DLS88/HotStuffPacemaker).
Dregg2/AssuranceCase.lean. These enter as Prop-portals (typeclass fields /
hypotheses), never as axioms; no other assumption is load-bearing anywhere in the case.The full delimitation — including the named Rust components inside the trust base and the present limitations, stated plainly — is rung 7 · the trust boundary.
Why the badges stay honest
Assurance here is not a one-time audit; it is a discipline that runs on every change.
lake build enforces it. Three layered mechanisms:
#assert_axioms
Every advertised keystone is pinned to the kernel triple plus the named crypto carriers (which enter as hypotheses, not axioms). A keystone that silently acquires a sorry or an axiom fails its pin — the build goes red.
Non-vacuity, both polarities
A guarantee proved over a := True predicate is broken even if it type-checks. So every load-bearing predicate is shown to discriminate: teeth theorems witness the false side, and concrete checks exercise both the satisfied and the refused case. A predicate that cannot be made false is not a guarantee.
The Convergence gauntlet
Whole-tree rounds catch what per-module verification structurally cannot — feature unification, cross-crate match-arm coverage, the corpus-wide zero-sorry grep, and the Rust↔Lean differential harnesses that pin the deployed code against the model.
What is staged, not yet cut over
The proofs are strong and load-bearing; the deployment is a research-grade devnet with named gaps. A seam the case does not name is a seam the case launders — so these are stated, not hidden. They calibrate, not retract: the guarantees hold over whatever state the executor actually runs on.
Solo federation
The public devnet runs one node, no peers. Consensus is live in the single-machine sense; the Byzantine-fault-tolerant multi-node path, while modeled and proved, is not what the public devnet exercises. Many of dregg's strongest properties are single-machine properties that become topology-bounded under real distribution.
Staged, not auto-attached
On the shared devnet each turn's witness lands immediately, but automatic per-turn STARK attachment is the gap. The proving machinery is real — you can produce and self-verify an EffectVM STARK in the playground — the devnet's automatic attachment is what is staged.
A named subset, not all effects
The verified Lean producer is authoritative for a named set of effect shapes (the node reports producer_covered_effects live). Shapes outside it fall back to the unverified Rust executor — logged, never silent — with the Lean verdict as a differential. The graduation lane burns the fallback set down.
From clone to a checked proof
Build the Lean development — every theorem on this page elaborates under the kernel, and the axiom pins fail the build if a proof smuggles in an assumption:
git clone https://github.com/emberian/dregg && cd dregg/metatheory
lake buildRead a guarantee's apex theorem where it lives — the names in the cards above
are Lean declaration names resolvable in metatheory/Dregg2/.
Ask a running node which semantics produced each turn — the verified-producer split is live API, not documentation:
curl localhost:8420/api/node/producer | jq