The meaning is source code.
The intended relation is authored in Lean. It can say “this is the optimal clearing,” “this rule matched,” or “this move is legal”—not merely “these opcodes ran.”
Public proof record 02 / the idea
Why proof-native computation
Computation begins with a question, not an instruction set.
A conventional virtual machine asks whether one machine ran. dregg asks whether the claimed relation holds, then accepts any faithful machinery that can exhibit the evidence.
The common language is the proof-bearing receipt—not an eternal instruction set.
01
Three commitments
What “proof-native” means here.
The proof checks that exact meaning.
The relation is lowered to a specialized proof leaf. Its program commitment and full verification key travel with the receipt, so a proof of an easier relation cannot substitute.
The result can act.
Committed state roots, capabilities, cells, and N-party hyperedges turn a proved result into an authorized operation. Receipts compose into recursively checked histories.
02
Objects by use
The struct is just where the cell currently sleeps.
The box is not the thing. It is the shadow the thing casts when you interrogate it.
dregg treats an object extensionally: by its behavior under admissible experiments. A storage layout is one coordinate chart for that behavior. A ledger is one place the experiments can be witnessed. Neither owns the object.
Same observations
If no admitted experiment distinguishes two cells, their representation is irrelevant to the observer.
Same refutations
A guard describes the tests that an offered behavior survives—not a nominal box around some fields.
Same laws, elsewhere
A cell may be local, offline, federated, or finalized. Consensus is a service it can use, not its metaphysical owner.
03
Knowledge by construction
Knowledge is what you can exhibit.
In a proof-native computing system, knowing and being authorized have the same constructive shape: possess a witness, and discharge it against the relevant verifier. Bytes alone are not knowledge. The accepting relation makes them evidence.
One participant can exhibit an accepted witness.
Every participant has such a witness.
Their pockets combine into evidence none need possess alone.
One finalized witness becomes shared and transferable.
The group knows. No member knows.
Zero knowledge A verifier can learn that an accepted witness exists without learning its content. Privacy changes revelation; it does not weaken acceptance.
04
Two forms of universality
A forever-machine, or a forever-legible claim.
Operational monoculture
Everything becomes one machine.
Simple universal evaluator. Rich structures disappear into encodings. Every optimization must later prove it faithfully implements that evaluator.
Certified pluralism
Meanings keep their native form.
Different relations share faithful identity, state linkage, proof verification, and recursive receipts. Each relation carries its own refinement obligation.
05
Why it can be smaller
Prove the certificate, not the search.
Suppose an optimizer searches a million candidates and returns one answer. An instruction-trace proof recounts the search. A semantic proof can instead check a compact certificate that no candidate is better.
Not the control flow of a parsing library.
Not every step taken by the solver.
Not a sample of accepted histories.
Not a generic heap interpreter.
Recursive proofs compress verification and proof size; they do not erase prover work. Memoization, parallel leaves, and compact certificates are what remove repeated computation.
06
Where trust moves
Proof does not abolish a trust boundary. It makes one inspectable.
checked
The semantic rule
Lean checks the reasoning about the stated relation. The statement itself must still be the right one.
bound
The exact program identity
Program commitment and all eight verification-key limbs are part of admission. Prefix matches and retired carriers refuse.
assumption
The cryptographic floor
Commitment binding, signatures, and proof-system soundness remain cryptographic assumptions. dregg names them rather than promoting them to mathematical facts.
scope
The privacy tier
Hiding proofs conceal witnesses from proof consumers. Unless a relation uses distributed proving, FHE, or MPC, the process constructing the trace can still see them.
not audited
The implementation whole
The formal spine is substantial. The complete system has not had an independent external security audit.
07
Plain answers
The questions people ask first.
Is dregg a zkVM?
Yes, in a deliberately different sense. Its common machine layer is the faithful proof-and-receipt protocol. Programs may use different semantic relations instead of compiling first to one public ISA.
Does it still execute ordinary code?
Yes. Rust, GPUs, FHE, MPC, and ordinary algorithms construct witnesses and run services. They sit beneath the authoritative relation rather than defining it.
Is it a blockchain?
It contains distributed history and finality, but one machine can use the same proof-native semantics locally. Consensus is one way receipts become shared history, not the definition of the computer.
Does a zero-knowledge proof make the whole operation private?
Not automatically. It can hide the witness from verifiers. Hiding the witness from every prover requires additional distributed cryptography, which exists for selected lanes and remains unfinished as a universal service.
Can I run it?
The source and development network exist. There is no polished general-purpose release, and several new semantic programs are not mounted on the public arcade yet.