Minidregg · the semantic computer

Prove the turn,
not the machine.

The zero-knowledge VM industry proves, over and over, the same sentence: "a RISC-V machine executed." Users never asked about the machine. They asked whether their transaction happened, whether it was authorized, and what exactly changed. Minidregg is a kernel that proves that sentence instead.

The statement nobody asked for.

Generality is paid for at proving time, forever. Measured in SP1, one general RAM access costs ~502 trace cells; the same value as read-only or write-once memory costs about 6. The instruction being proved costs 39–44. The industry's cost curve is dominated by emulating machinery · instruction fetch, general RAM, an ISA · that exists only because the statement was "a machine ran," not "a thing happened."

A statement-level lever compounds with every prover trick underneath it. So the kernel here proves the smallest statement that is actually true and actually wanted: this authorized semantic turn happened, and here is its receipt.

Founded on an audit.

Minidregg began by auditing its own predecessor: a ~2.89M-line system · 1.82M Rust, 913K Lean · that had built and proved every piece of the derivation machine, demonstrated each at n=1, and wired almost none of them into the load path. An eDSL with a complete verified vertical slice, used exactly once, while 63 apps and ~962 theorems were written by hand beside it. A proof that the kernel is three verbs, never executed. The audit's verdict, verbatim:

The corpus contains its own refactor plan, proved as theorems, and did not execute it.

The founding move is the inversion: the derived path is the only path, so n=1 and n=all coincide by construction. Nothing lands beside; everything replaces. The audit priced the system's actual meaning at a few tens of thousands of lines · semantic core ~25K, irreducible kernel 800–1,200 · and set the successor's budget at a tenth of the original. It is currently well under it.

What a turn is.

The constitution fits in one sentence: a turn is the exercise of an attenuable, proof-carrying token over owned state, leaving a verifiable receipt. The pipeline that realizes it:

typed request + current authority + canonical pre-state
        │
        ▼
Lean-owned effect family
        │
        ▼
accepted effect + exact validated patch
        │
        ▼
one balanced multi-cell semantic hyperedge
        │
   ┌────┴────┐
   ▼         ▼
durable    causal receipt / history
settlement      │
              Selvage proof / checkpoint

No instruction fetch anywhere in the picture. An agent plans several effects and publishes them as one balanced hyperedge; the proof is about the hyperedge; the receipt is what another device checks.

Promises with a ladder.

Every pillar of the system advances through five named levels, and the levels are a public promise-vocabulary · a claim states its rung or it overstates itself:

An S theorem cannot be advertised as D. No consumer is replaced before D, and no performance conclusion is accepted before B. The ladder is not modesty; it is the interface other people's trust plugs into.

Instruments that can fire.

At AI proving speed, the dangerous failures are silent: a soundness theorem quantified over a type nothing inhabits, a bound proved "explicit" and never exhibited, a green build that means nothing. The prover never tires of producing green things. So the tree carries instruments, and every instrument must demonstrate it can fail:

A carrier census mechanically hunts types that are quantified over somewhere and constructed nowhere · the signature of vacuous quantification. It found four provably-uninhabitable schemas in this very tree, and it self-tests against carriers whose status is known by construction, because an instrument that silently stops detecting looks exactly like a clean tree. Keystone theorems ship with a satisfying witness and a falsifying case. "The theorem is conditional on H" is admitted only with a witness for H or a named, tracked obligation. And facts worth asserting are named theorems with pinned axiom footprints · never anonymous compiled checks whose record deletes itself.

Where it stands, plainly.

Lean files          487        (counted fresh, 26 Aug 2026)
lines of Lean       217,341
`sorry` in proofs   0          `axiom` declarations   0
proof system        Selvage · 138 files
axiom footprints    pinned · a regression fails the build

Those numbers are the cheap part, and the tree says so itself. The semantic and admission layers are the mature rungs; physical storage refinement, concrete cryptographic prices, production key custody, and consumer cutover are named open work on lower rungs · held at S or A until they are earned upward. The ladder is doing exactly what it is for.

Status, plainly: a research tree, weeks old, moving fast under instruments built for that speed. Project site: emberian.github.io/minidregg.

Prove the turn,not the machine.