A literature-review document, not a design doc. Its job is to make 'should we start this' a real decision later, not an open-ended fear.
One Winterfell proof over VmAir, Blake3-hashed, ~5–11 KB for the examples in this repo, growing with trace length. It verifies off-chain in milliseconds. Nothing about it is compact enough, or in a format cheap enough, to check inside an EVM transaction — a STARK is typically tens of KB minimum, too large and too gas-expensive to verify directly. See the On-Chain Verifier page.
(a) Recursive STARK composition. Prove, in a second, smaller STARK, the statement "the first STARK proof verifies." This stays inside STARK-land (no pairing-based trusted setup), but means implementing a STARK verifier as an AIR — encoding FRI folding, Merkle path checks, and out-of-domain constraint evaluation as constraints in a new circuit. Well-trodden elsewhere (SP1, RISC Zero, StarkWare's own construction do this) — but not yet designed for this specific AIR.
(b) External SNARK wrapping. Prove "the STARK verifier accepts this proof" as a Groth16 or PLONK circuit over BN254 — a field switch from the current 128-bit prime, since pairing-friendly curves use different primes. Needs a trusted setup and R1CS/arithmetic-circuit tooling entirely outside what this repo currently touches.
Both paths converge on the same hard sub-problem: implementing this STARK verifier's arithmetic as constraints in some proving system.
This is a 2–3 month research-and-implementation project, done properly.
It does not block the ISA expansion, the MCP endpoint, or anything else in this repo. Nothing here is implemented, and nothing should be started opportunistically alongside other work — it deserves being picked up as its own deliberate effort, after the Keccak-hasher switch and after the AIR has stabilized. See the real roadmap for where this sits relative to everything else.