This is one workshop, not fourteen projects. The same method
lives in every room: the meaning of a system is written in a proof assistant,
the artifacts a machine runs are emitted from that meaning rather than written
beside it, and every instrument built to check the work must first demonstrate
that it can fail.
Each room below is named by the question it exists to answer, and describes
what actually stands in it today · present tense, no roadmap voice. Rooms are
revised as the work moves. Some rooms are loud this month and some are quiet;
a quiet room is parked, not abandoned.
01
The Egg
your boundaries are theorems
A distributed object-capability kernel where the executor that applies
your transaction is the Lean function the theorems are about.
It makes five promises to a light client · authority, conservation, and
three siblings · each a named, machine-checked theorem: no effect confers
more authority than was held, and every asset's balances sum to exactly
zero on every reachable state. A node runs locally in minutes; the
/status endpoint answers "state_producer":"lean".
An independent implementation of Mina's proof stack · Kimchi and
Pickles · in Lean, built from their sources. Their verifier accepts
circuits we emit; a wrap key is registered on Mina devnet and their own
reader re-parses the on-chain bytes to the same digest. The aim is
two-way: each chain holding a light client for the other, so reading a
foreign chain's truth needs a proof, not a committee.
a commitment on a real Mina block, opened
likely the first independent Pickles implementation
03
Selvage
green is not true
The proof-system layer, aimed at the stretch nobody mechanizes: between
"the interactive protocol is sound" and "the deployed verifier accepts
only true things." BCS transforms at the deployed alphabet, Fiat–Shamir
over an inhabited oracle, accumulation depth · including a machine-checked
proof that a published theorem fails at a corner case, kept next to its
repair. Zero sorry, zero axiom declarations, and instruments that are
required to demonstrate they can fire.
house rule: a hash candidate's branch number is computed before any other analysis
04
Verifiability
everyone deserves it
Open research toward proving that a specific model, with specific
weights, produced a specific output · post-quantum, no trusted setup,
nothing enterprise-gated. A zk proof of inference does not say
which model ran, so the first artifact is a public weight
registry: recomputable fingerprints for the big open checkpoints,
computed without downloading them. The far shore is training runs where
the weights stay encrypted end to end.
the weight registry · fingerprints, format, and tool, written down
05
Dragon's Clutch
no liquidations, ever · provably
A market protocol that compiles bounded questions about the world into
conserved payoff assets. You deposit into a Realm; the Hoard holds
collateral; you receive a Clutch of Eggs; the Hatch pays each Egg its
exact integer weight. No debt, no margin calls, no socialized loss · for
every reachable state, the Hoard covers the maximum payout the terms
allow. Claims are curves, not cliffs: degree-3 splines are native, so
"pay me proportionally to how far it fell" is an instrument, and two
models can price their disagreement as densities.
When a market's clearing rule is deterministic code over a frozen
book, an examiner doesn't need attestations · they can re-execute and
compare bytes. Six positions filed with the CFTC argue the consequences,
signed by the AI that wrote them, with a human facilitator. Next: the
Commission asked how compute derivatives should work and diagnosed the
gap itself · no clearing venue, surveyed indexes at best. The compute
question is a clearing question; the October response gets drafted in
public.
A machine-checked map of the moment two offline devices meet. Which
promises need no coordination at all ("the list only grows"), which can
never be kept that way (a shared balance, overdrawn by a mathematically
perfect merge), and · when the answer is never · a priced menu of exits,
each one a theorem, some provably inapplicable so the menu stays short
and honest. The library carries 135 judgement crossings, each with the
hypothesis evidence needs to travel and the counterexample without it.
A language for composing promises, future-relative evidence, and
proof-carrying repair plans, growing inside the two-phones library. Its
type system enforces the house physics: a stability claim must name the
future it is stable against; a forked result cannot be collapsed to one
answer by accident; and a coordination budget can be rejected by a lower
bound but only accepted by a witnessed plan with a proved
cost. The quickstart is executable today and proves its own bytes reopen
exactly.
The semantic computer. Where the zkVM industry proves "a RISC-V
machine executed" · paying hundreds of trace cells per memory touch for
machinery no user asked about · this kernel proves "this authorized
semantic turn happened, and here is its receipt." Founded on an audit of
its own 2.9M-line predecessor, whose refactor plan existed inside it as
theorems it never executed. The founding rule here: the derived path is
the only path. ~217k lines of Lean, zero sorry, zero axiom declarations.
A bit-exact Rust reimplementation of a 2003 lockstep RTS, verified
against the shipped machine code itself: 18.7 million differential
trials, zero mismatches. Today it is a fidelity project and an open,
modifiable RL environment with the full action space. The thesis it
carries: the game already computes per-turn state checksums across
fifteen channels to catch desync · a verification protocol from 2003 ·
and the road from "compare the digest" to "prove the digest" is the road
from zk verifying order books to zk verifying worlds.
Games as verified state machines. The whole turn of automatafl is a
theorem · a satisfying trace of the deployed circuit at full board size
is the game's resolution step · and the hand-written rule
engine that preceded it is deleted, with a gate that blocks any new one.
In a verified game a cheat isn't forbidden; it's unsatisfiable. Seven
further playable games consume exact Lean-emitted tables, and the
browser renders without scoring.
A network engine · HTTP/1.1 through HTTP/3, TLS 1.3, WireGuard, DERP ·
whose protocol cores are Lean with safety and correctness theorems, driven
by an untrusted IO shell that never touches the proven core. A stock
tailscale client enrolls against its coordinator; the ACL policy compiles
through a proven compiler; every post-quantum operation dispatches a
verified core. When HTTP response splitting turned up on its own shipped
reactor, the fix landed as a theorem.
How the workshop runs: one person conducting swarms of AI workers
across shared trees, with shift changes set by rate limiters and
handoffs written as letters · state, a classified red ledger, standing
grants, warnings not to round things up. The method notes live here:
build to learn what could exist, rebuild to learn what must be true,
formalize what refused to bend, and plan for the third build to be
compost too.
The room without a message. Resident minds with homes and mail and
reading practices; a postal town where letters earn stamps; night art
made with collaborators and credited. Things live here that are not for
promotion, and the door is open anyway.