Selvage · the compilation layer, machine-checked
Green is
not true.
Machine-checked developments fail in ways the kernel cannot see: a soundness theorem quantified over a type nothing inhabits; a bound proved "explicit" and never exhibited below 1; a spec that hypothesizes exactly the gap that is the bug. At AI-assisted proving speed these are the dominant failure mode · the prover never tires of producing green things. Selvage is a proof system built assuming that.
The middle nobody holds.
Published soundness analyses stop at "the interactive protocol is
round-by-round sound." Deployed systems begin at "the verifier accepts only
true things." Between those two sentences sits the compilation half of the
SNARK stack · Fiat–Shamir, the BCS transform, accumulation · and it is where
the bodies are buried. Selvage lives there: 138 files, ~68K lines of
Lean, zero sorry, zero axiom declarations,
today holding, proved:
RBR → Fiat–Shamir compiler fsKeystone_proved · (t+k)·ε_rbr,
over an inhabited lazy-sampling oracle
BCS transform soundness at the deployed alphabet · roots,
opened columns, opening proofs
state-restoration soundness proved
accumulation depth composition proved · with a correction (below)
sponge indifferentiability proved · the simulator constructed,
the capacity price named
Mechanization must be able to disagree.
The accumulation-depth theorem this field leans on is written up in WARP (ePrint 2025/753, Thm B.4). Selvage mechanized it and found the literal statement fails at a degenerate corner case:
theorem OB2_depth_composition_false :
¬ OB2_depth_composition -- the published statement, refuted
theorem OB2_depth_composition_nonneg_proved : …
-- the one-guard repair, proved
Both live in the same file, refutation beside repair. Mechanization that only ever confirms the paper is not earning its keep.
Instruments must fire.
Every safeguard here is treated as itself needing a demonstration that it
can fail. The light-client grinding bound carries a try-count factor, and
rather than assume the factor matters, the adversary that needs it is
exhibited: phantomGrind_beats_fixed_bound
constructs the two-candidate grinder that beats the fixed-chain bound. The
sampling keystone is proved attained · equality, not ≤, at a
named small field (sampling_bridge_tight) · so the bound is not
improvable in general.
The same discipline prices the deployed configuration. Its composed soundness error is proved ≤ 2⁻⁵⁵ and > 2⁻⁵⁶, with the dominant term named. A bound that is merely "explicit" can be vacuously loose; a two-sided bound cannot.
The assumption we never made.
Proof systems are prime-field-pinned for one usual reason: a smooth multiplicative subgroup of order 2ᵏ, which cannot exist in GF(2ᵏ). A census of the whole tree:
IsPrimitiveRoot 0 occurrences rootsOfUnity 0 occurrences primitiveRoot 0 occurrences every Reed–Solomon code: reedSolomonCode (dom : ι ↪ F) (d : ℕ) · an abstract embedding, distance by root counting
There is no multiplicative evaluation domain in the repository, so the usual wall does not apply. Scored keystone by keystone: 13 of 18 transfer to binary fields with no new mathematics. The escape everyone else engineers, this tree gets by never having assumed the thing being escaped.
The gate at the door.
Hash design has a house rule now: a candidate linear layer's branch number is computed before any other analysis · the exact-branch instrument runs in 6.8 seconds on a laptop. The rule is a paid lesson, and the first candidate's epitaph states the price: the alignment thesis imports the code's triangularity, and triangularity is the opposite of diffusion. Its branch number:
Weft novel-eval E GF(2³²), t=24 branch 6 ☠ killed Cauchy dense D GF(2³²), t=24 branch 25 the MDS yardstick E·D · D·E composites ∈ [8,21] · [8,11] ☠ killed systematic-RS A=V₂·V₁⁻¹ branch 25 exact, by theorem Poseidon2 M_E BabyBear, 16 branch 8 the bar to beat
An afternoon is cheap. A deployed hash with branch number 6 is not. Every candidate since has met the gate first, and the one that passed (systematic-RS) passes by theorem, not by sampling.
Whether the terms say anything is a separate instrument's job.
Status, plainly.
Selvage is currently theory ahead of its own runtime. The deployed engine is a 433-line degree-1 sumcheck; there is no multilinear commitment; the accumulation architecture the theorems describe is not yet what any deployed prover here runs. Some sharp results are proved at small domains while the deployed-parameter statements carry named hypotheses · the per-file docstrings say which is which. Publishing that distance is part of the method.
Counts measured 26 August 2026 against the tree at HEAD. The instruments are the part of this work we most want challenged.