Small sites. Large ideas.
Self-contained visual essays from the DREGG research process: protocol design, executable semantics, formal methods, and the machinery we learn by rebuilding.
Published
A promise that survives
Inside fn: executable ACL2, durable news, disconnected exchange, and the remaining joins between component proofs and shared infrastructure. An independent report with a source notebook.
Learning while encrypted
Teach a model new examples while its memory stays encrypted. See how its answers change, how it replaces old examples, and what happens after a restart.
The whole way through
Fresh teaching, encrypted memory, a nonlinear answer—and the reader we still need to remove. A new join in the machinery, and a change in how we build.
Keep learning. Keep a secret.
A continuing machine, useful encrypted learning, and the construction that would let it communicate without handing its host a universal reader.
Plan to compost at least three
On building a market protocol three times on purpose—and treating every implementation as compost for the next one.
Fourteen rooms
A map of the workshop, kept current: each room named by the question it exists to answer, and what actually stands in it today.
Two phones
Which promises survive two offline devices meeting · the shopping list that merges free, the shared $100 that provably can't, and the priced menu of exits.
A clutch of eggs
The Dragon's Clutch lexicon: Realms, Hoards, Eggs and the Hatch · a market with no liquidations, claims that are curves, and resolution anyone can recompute.
Make the digest a proof
A 2003 RTS already computes per-turn state checksums to catch desync. The thesis: prove the digest instead of comparing it · and take zk from order books to worlds.
Trust me, in Latin
Six positions on markets becoming software artifacts, prepared for the CFTC · written by an AI system with a human facilitator, quoted from the statement itself.
Green is not true
The proof-system layer nobody mechanizes · where a published theorem failed at a corner case, and every instrument must first demonstrate it can fire.
Prove the turn, not the machine
The zkVM industry proves a machine emulated. Minidregg proves the authorized semantic turn · the statement users actually need · and derives everything else.
The cheat is unsatisfiable
A board game whose whole turn is a theorem: proving it surfaced seven rule bugs, the hand-written engine was deleted, and the known cheat is now UNSAT.
The fix is a theorem
A verified network engine: response splitting found on its own reactor and closed in Lean, a stock tailscale client enrolling against a proven coordinator.
Months in evenings
How the workshop runs: shifts that end at rate-limit walls, handoffs written as letters between machines, and cross-vendor peer review as ordinary practice.
Promises, priced
A language where a stability claim must name its future, a fork cannot be collapsed by accident, and a budget is only ever accepted with a witness.
Which model?
A zk proof of inference proves the computation ran · not which model ran. The missing piece is a public name for the weights, and now the open ones have one.
Reading a millennium proof
A claimed Clay-problem proof, a real error found in review, an honorable erratum within days · and the formal library where the question becomes stateable.