Machinic zkVM
Prove an instruction trace.
Compile the program to one fixed machine. Prove every load, branch, and arithmetic instruction that machine performed.
Public proof record 01 / dregg
A proof-native semantic computer
A computer whose programs are meanings.
A parser need not masquerade as a CPU. Nor should a market, a policy, or a world. In dregg, each keeps its natural meaning—and produces a proof that the meaning was respected.
The shift State the claim. Find its witness by any sound means. Check the claim itself.
02
The inversion
Do not simulate first. Say what is true first.
Proof-native dregg
Prove a semantic relation.
Keep the object in its natural shape. Prove the derivation, optimum, decision, or state transition directly.
Machine execution still happens underneath. It may be Rust, a GPU, encrypted arithmetic, or a conventional prover. But that implementation is not the constitution. The relation written in Lean is.
This is not conventional “symbolic execution.” Symbolic means the proof speaks in the symbols of the problem—the grammar, graph, policy, market, or game—rather than in the opcodes of one forever-machine.
03
The object
The cell is not the box.
The box is where the tests ran out.
A cell is not finally a struct, a record, or a place on a chain. It is what remains the same under every admissible way of using it: what it reveals, what it refuses, and which acts it permits.
Observe it by experiment.
Give it an admissible action; receive an observation. Two cells are the same when no permitted experiment can tell them apart.
Describe it by refutation.
An interface is closed under every test that cannot refute it. Attenuation adds refutations: fewer claims, fewer powers, a smaller attack surface.
Coordinate chart The current data structure is useful engineering. It is not the ontology. The laws are meant to survive another representation.
04
One semantic step
The receipt is the universal machine boundary.
old_root
program_root + VK8
proof
new_root + result
same programexact state linkexact next indexrecursively foldable
Different semantic programs share this boundary without sharing an instruction set. A verifier checks the exact program identity, all eight verification-key limbs, the old and new roots, and the authorized public result.
05
Native shapes
One proof fabric. Many kinds of program.
Each relation keeps the structure that makes its certificate small and its statement legible.
Decision
Private preference
Four hidden ballots choose one public winner. Totals remain private; lowest index wins a tie.
scores ⊢ winner
Optimization
Dark Bazaar
A hidden order book proves the uniform price and maximal clearing volume without replaying a solver.
book ⊢ optimal clear
Derivation
Languages and policies
Parses, stack languages, and symbolic policy expressions carry checkable derivations and equivalence decisions.
object ⊢ accepted
Transformation
Graph rewrite
A private rule and match prove that one committed graph validly became another.
graph₀ ⊢ graph₁
World
Games and cells
Moves are admitted by their actual rules, then enacted through capabilities and receipt-linked state.
world₀ ⊢ world₁
Distributed act
N-party hyperedge
Many cells share one turn identity and one conservation equation: the operation happens atomically or not at all.
participants ⊢ one turn
06
The whole organism
Dragon’s Egg is the living arrangement.
The receipt is its common boundary, not its whole body.
Kernel
dregg
Cells, capabilities, turns, and receipts: the small constitution every other layer reduces to.
Inhabited world
deos
A card is a cell and a button is a verified turn. One world can paint through the cockpit, browser, chat, terminal, or seL4. The renderer is only a glass.
Inhabitants
Confined agent grains
Agents can be rented, budgeted, metered, slept, woken, shared, and reaped. Each admitted action binds to a committed executor turn; proving host execution remains the R3 step.
Worlds
Games and offerings
The Descent, multiway-tug, and automatafl exercise kernel teeth, private membership proofs, and custom semantic leaves through one frontend-independent Offering shape.
One egg Not one binary, one chain, or one renderer: a society of sovereign objects whose operations can be exhibited, checked, and composed.
07
Universality, elsewhere
Standardize the receipt, not the reduction system.
A parser should remain a parser. A graph transformation should remain a graph transformation. An optimizer should submit an optimality certificate, not a billion-instruction diary of how it searched.
dregg becomes general through certified composition: independently proved semantic leaves inhabit one faithful receipt and recursive-fold protocol. New meanings can join without pretending to be old ones.
08
The builder
Built in Lean first, accelerated elsewhere.
I’m ember, a systems and proof engineer. dregg brings together work in programming languages, protocol engineering at O(1) Labs, seL4, zero knowledge, games, and distributed systems. It is built in the open with Claude, Codex, Fable, and other agentic collaborators.