simplified version ↗

the question everyone asks

what can you
do with it?

Here's the standing answer, as running code. Every app below is in the repo with its tests; the counts are real. And they all share one rule worth knowing before you scroll: the answer is never Effect::FooApp — there are no app-specific kernel primitives. Every one of these composes the same four verified pieces (caveats, conservation, attenuation, receipts), and the refusals happen in the executor, not in app code. An app can't have an auth bug in a layer it doesn't own.

money & markets

Escrow marketTwo strangers swap value with no trusted middleman: list → fund → ship → settle; a ghosting seller is defeated by reclaim. Value can't be minted or lost across the trade — one test drives value across two apps and conservation holds end to end.54 tests
Sealed auctionAgents compete for one award: commit → reveal → award. Overwriting a committed bid isn't caught by the app — it's an executor refusal. Phases can't rewind.52 tests
Compute exchangePost a job with a budget, take bids, settle. Paid + refunded == budget is enforced in-circuit; a bid over budget can't even be committed.51 tests
The auditable fundAn AI trades a bounded budget you audit instead of trust: every trade is a jailed, attested turn against an attested price. An over-mandate trade is refused; a forged track record fails the audit; an unattested price never fills.runnable example

governance & the polis

Non-domination as theorems, then the same shapes as running code. The keystone: verify the cage, never the animal — the governance envelope is proven safe for every possible controller, universally quantified and never inspected.

the proofs

A 67-file, 540-theorem Lean corpus with zero sorry: polis_safety holds for all controllers; operator non-domination and light-client unfoolability are conjoined under one ∀-adversary quantifier; composing a second governance axis provably never weakens the first — refusals only grow.

the arbiter nobody owns

A running demo: an AI arbiter refuses a prompt-injected case (un-censorably), refuses out-of-jurisdiction fail-closed, and puts genuine rulings to a ⅔+1 operator quorum — while a forged ruling ratified by all four operators still tallies zero and never finalizes.

One voting engine, three facesThe same engine drives a federation governing itself, a community poll, and a story's collective choice. Votes are blocks — a dropped ballot fails, a stuffed tally is refused, and liquid-democracy delegation is provably non-amplifying.green
Privacy votingOne vote per person, enforced by the ledger, not the app: your ballot cell is write-once, the tally is monotonic, double votes die on the nullifier, and eligibility commits to a credential set.50 tests
The polis councilA multi-member council that governs by running: propose → vote → certify, with a premature certify refused by the executor. Per-viewer surfaces over HTTP, capability-gated.78 tests
Governed namespaceShared infrastructure whose route table only changes by atomic, vote-gated swap. Its anti-drift test caught a real bug — which is the point.120 tests

Where this is going: a constitution for the polis exists in early draft — a basic law where every clause carries a soundness tag (structural-by-theorem, adjudicated-with-named-cost, or honestly out-of-jurisdiction), and membership is the intersection of exported floors, never souls. Draft 0.1; the mechanisms above are its first organs. A sibling experiment in peace: mediateor.

oracles & attested intelligence

Don't screenshot the web — certify it. And when an AI acts, make its decision a checkable object.

zkOracle — three proofs in one

An attestation that an HTTPS answer is authentic (a genuine TLS session with the pinned host, your API key redacted), well-formed (a real context-free parse certificate — nested structure a regex provably can't certify), and uninjected ("does not match the template" as a first-class verified object). Any leg fails → refused, with the failing leg named. One Lean theorem, zkOracle_sound, conjoins all three; zero sorries across the corpus. Measured: a 1.2 kB response proves in 318 µs; a million-token conversation in under a second.

an LLM's decision, with receipts

A running demo drives a real hosted LLM through unchanged production code, has it echo a fresh per-run nonce (a recorded fixture could not), and attests the reply — then the teeth bite: an injected turn refused at prove, a flipped byte refused at verify. In the companion demo, a confined agent holds a capability its operator cannot amplify, refuses an instruction from its own operator, and commits its attested turn onto a ledger a light client re-verifies.

Oracles as data, not forksA new verified web oracle is an EndpointSpec, not a new codebase. Shipped: GitHub commit attestation and a Coinbase spot-price oracle behind a clean trait.shipped
Real MPC-TLS underneathBehind a flag, the pipeline runs a genuine two-party TLS presentation — selective disclosure hides the API key, a tampered presentation is refused by real cryptography, and the whole run round-trips locally.live-local
One certificate framework under it allRegex, CFG parsing, and arbitrary graph rewriting are one verified theory: for any reduction relation, a locally-checkable chain certificate exists iff the derivation does. Parsing is just the string instance.proven

Honest seams, named in the source itself: the live demo's model is Nemotron (the rails are Anthropic-shaped; a live pinned-notary session against the real provider is the named remainder); "on-chain" means dregg's own light-client-verifiable ledger; and the fully-jailed live TLS call needs the Linux deployment. The auditable fund that composes all of this is stamped paper trading only — deliberately.

identity & provenance

Verifiable credentialsIssue a credential, present it with selective disclosure — show only what the verifier needs — verify, revoke.71 tests
The nameserviceOwn a name: register → resolve → renew → transfer → revoke. A name is a cell; its owner is whoever can exhibit the capability witness.109 tests
Supply-chain provenanceTrack an item through custody handoffs where "exactly one custodian at a time" is a conservation law, not a database convention. A stale handoff is refused; a verifier can't accept custody.60 tests
Agent provenanceA tamper-evident memory and action log for an AI agent — append-only, with competing overwrites refused by the executor. An agent's history that can't be quietly rewritten, by anyone.47 tests

worlds, stories & documents

the fog-of-war game

The forcing exemplar: a two-player world where fog of war is a cryptographic confinement property, not a rendering trick. You provably cannot peek — projecting enemy tiles requires a proof only their secret-holder can produce, fail-closed. Two AI agents play a full match to a decision entirely through the capability gate; a player cannot even grant a view of the enemy side. Honest seams: turn-paced (no real-time tempo yet), and the vision proof is the signature tier, not yet the ZK tier.

the attested dungeon master

A provably-honest AI storyteller: every narration is a receipted, attested turn. A player's prompt injection is refused as a proven property of the parse, not a heuristic — and an injection smuggled inside a forged attestation is rejected at verify. The DM cannot grant an unearned item; the dice can't be quietly loaded.

Collective fictionA crowd plays a story together: four voters pick each branch through the real voting engine (duplicate ballots die on the nullifier), the winning branch lands as a verified turn, an attested DM narrates — and refuses a prompt injection — and a federation poll ratifies the ending. The whole playthrough re-verifies against a fresh identically-seeded world. One terminal command runs it end to end.runnable demo
Collaborative documentsReal patch theory: a conflict is a first-class object you resolve by clicking — never a merge failure, never a silent overwrite. Offline edits stitch back verifiably; an authority-violating merge is refused at settlement.159 tests
The MUDA two-player dungeon where rooms are cells and every command is a cap-bounded signed turn. The players' timelines genuinely fork, explore, and stitch back — disjoint edits merge; both players grabbing the one sword is a refused conflict, not a silent overwrite. Item duping is structurally inexpressible, and a trade conserves value Σδ = 0.runnable demo
TussleA two-player physical-combat match: both fighters commit sealed moves, reveal, and a referee resolves the frame. Revealing during the commit phase is refused in-band; the whole match is a chain of two-party joint turns.40 tests
The galleryCommit-reveal art curation: a sealed submission is frozen on-ledger the instant it lands — swapping it afterward is an executor refusal.51 tests

Honest scale: these are engine demos, not hosted multiplayer products — the fiction demo plays one short scripted story; the MUD's two players are forked in-process sessions. The refusals, receipts, forks, and merges are entirely real.

agents & services

Tool-access delegationAn agent hands another agent a narrow, rate-limited, expiring tool grant. Over-rate, over-scope, and past-deadline calls are executor refusals even if every in-band check is bypassed. This is the MCP-security story, byte-mirrored against its Lean twin.62 tests
Swarm orchestrationMulti-agent task dispatch where an over-budget dispatch or an amplifying grant is caught on the commit path — plus a durable, auditable task board over HTTP.58 + 68 tests
The grain commonsAn app store for hostable, forkable, pedigreed agents: publish, discover, rent, review, fork. A hatched subagent's capabilities are a strict attenuation of its parent's — forever, provably. Forks keep their pedigree.23 tests
The kv-storeThe hello-world service cell: a rollback-proof key-value store where a replayed write that lowers the version is an executor refusal. Start here if you're building.24 tests
honest floor ▓  test counts are from the tree at time of writing; several suites were spot-run green while writing this page. These are substrate apps — unit- and integration-tested on the real verified executor, still hardening toward scale and adversarial load. Build your own: the guide · the first five minutes.
never Effect::FooApprefusals live in the executor