What is built, what is next, and what depends on what.

Bread

The original dregg system: capability tokens, cells, turns, receipts, proof circuits, consensus, worlds and markets.

Primitives

• Identity and authority in progress — Authority held by proof: capability tokens, credentials, hybrid quantum-safe keys.
• Primitives built — Hashes, signatures, post-quantum keys and the Lean proof assistant.
• Credentials and predicates in progress — Proving an attribute without revealing the credential.
• Cross-platform identity link in progress — Links a chat-platform identity to an account without publishing it.
• Cryptography in Lean in progress — Keccak, BLAKE3, Merkle and Pedersen formalised and checked in Lean.
• Lean metatheory built — The Lean 4 corpus stating what the system must do.
• Datalog capability tokens built — Tokens carry their own rules and only narrow when delegated.
• Passkeys wrap the seed in progress — Device passkeys protect the root seed; a passphrase path remains.
• No classical-only crypto in progress — Every signature and key exchange gets a post-quantum partner.
• Post-quantum frontiers built — Formalising threshold lattice signatures, composition and key exchange.
• Presentation leakage theorem planned — States exactly which facts a credential presentation leaks.
• Account survives key rotation in progress — An account keeps its identity when its signing key changes.
• Permissions only narrow built — Delegating a token can restrict it, provably never widen it.
• Axiom-pinned claims ledger built — Build fails if a claimed theorem uses non-standard axioms.
• Biscuits cross vat boundaries built — Biscuit tokens survive crossing between distrusting machines; macaroons do not.
• Borrowed verified-crypto axioms in progress — Twenty-five primitive facts assumed from an externally verified library.
• ML-DSA verify from Lean in progress — Runs the real post-quantum signature check from verified Lean.
• Name every asserted fact built — Facts are named theorems, not one-off checks; a script enforces it.
• Ed25519 plus ML-DSA identity built — An identity is valid only if both signatures verify.
• Token to capability bridge in progress — Proved link from macaroon caveats to the kernel capability graph.
• Remaining classical surfaces in progress — Five node surfaces are hybrid; eight remain classical.
• Post-quantum verifiable randomness in progress — A randomness beacon verifiable without pre-quantum assumptions.
• Predicates over hidden values in progress — Proving statements about hidden attributes; currently refuses rather than answers unsoundly.
• Revocation checked by default in progress — The web edge refuses revoked credentials by default.

Proofs

• One circuit in progress — Rules compile mechanically into proof circuits; no hand-written constraints.
• The floor in progress — The assumptions under the proofs, and attempts to break them.
• Sealed computation in progress — Computing on unreadable data: homomorphic encryption, threshold keys, shielded pool.
• Greens that mean something in progress — Every gate must go red when what it guards breaks.
• Circuit efficiency backlog in progress — Reducing trace width and proof cost by measurement.
• Private convex engine in progress — Private convex optimisation for market clearing and assignments.
• Field-element width repair in progress — Eight 31-bit lanes cannot injectively encode 32 bytes; add a ninth.
• FHE clearing (fhEgg) in progress — Clears markets by summing encrypted orders, then threshold decryption.
• FRI soundness accounting in progress — What the proof system proves: 130 conjectured, 51-73 proven, ceiling 123.6 bits.
• Full-turn proving mode in progress — Node mode attaching a STARK proving each turn a valid kernel step.
• STARK to EVM wrap in progress — Wraps a STARK into a BN254 proof verifiable on Ethereum-style chains.
• Retire the carrier debt in progress — Replace named assumptions with proved theorems or genuine floor items.
• Verified layout optimizer in progress — Proven allocator and peephole optimizer for trace layouts.
• Circuits emitted from Lean in progress — Deployed circuits come from Lean, pinned byte for byte; Rust interprets.
• MPC output boundary in progress — Multi-party computation for threshold keys and output release.
• Hash-in-kernel cost built — The deployed hash is infeasible in-kernel; compiled evaluation is used.
• Premise inhabitability instrument built — Proves a theorem's premise satisfiable, exposing hollow theorems.
• No single viewer planned — A hiding proof that hides the witness from the trace builder too.
• Shielded pool in progress — A private value pool with complete Lean proofs; never held value.
• Pickles in Lean in progress — First independent synthesis of Pickles recursion, authored in Lean.
• Statement audit built — A 2026 audit of what theorems state, not their arithmetic.
• Floors must be refutable in progress — Floor assumptions must be satisfiable and refutable, not provable.
• One frozen verification key in progress — One key per circuit, never silently recomputed; one registry.
• Witness-generator assurance in progress — A STARK proves the trace, not its generator; closing that gap.
• KZG vacuity repair in progress — Repairs a vacuous KZG binding statement in a public library.
• Re-ground 1,925 carriers in progress — Rewrite idealised assumptions as adversary-quantified games.
• Chain-safety apex was vacuous abandoned — The chain-safety theorem rested on an uninhabited hypothesis; since repaired.
• Correlated agreement formalisation built — Machine-checks the proximity lemma under FRI soundness, layers L0-L6.
• Deployed proof runs Lean descriptor built — The devnet history proof runs a Lean-emitted descriptor.
• Compile descriptors from specs in progress — Circuits generated from rules; 26 of 91 descriptors so far.
• 2-of-3 committee, one host built — A threshold committee demonstrated on a single machine.
• Correctness at real modulus built — Homomorphic aggregation correct at a realistic modulus; hiding only bounded.
• Coalition privacy theorem built — Any coalition missing one party learns nothing from threshold decryption.
• Decrypt-share certificate planned — Certifies honest threshold-decryption shares on the live path.
• GPU kernels bit-exact built — GPU encrypted-arithmetic kernels match the reference bit for bit.
• Two hand-written clearing circuits planned — Two Rust clearing circuits must be emitted from Lean.
• Hardware for sealed arithmetic planned — FPGA and RTL accelerators for encrypted arithmetic.
• Malicious-secure key generation planned — Key generation safe against actively cheating participants.
• Sealed orders on ten routes built — Sealed order submission works on ten routes; one bit remains.
• Dead floor binders shed built — Unused assumption binders removed from fourteen theorems.
• FRI adversary object in progress — Formal adversary for the verifier; bound not yet useful at 2^31.
• Convert 1,407 legacy sites planned — Hand-written constraint sites to be converted to emitted ones.
• IPA opening-soundness floor built — Ten theorems stating the opening floor's assumptions.
• Differential fidelity 40/40 built — Lean synthesis matches the reference on 40 of 40 checks.
• Wire binding into acceptance planned — Connects transcript binding to the verifier's acceptance theorem.
• Transcript-equality binding built — 45 theorems binding the recursion transcript to its inputs.
• Proven-regime FRI parameters planned — Deployed parameters moved to provable bounds, about 4x more queries.
• Gate against hand-written rules built — CI blocks new hand-written constraints in Rust.
• Six wounds as theorems built — Theft, inflation, double-spend and wraparound flaws as checked statements.
• Value can enter the pool planned — A mint, shield or genesis path into the pool.
• Join two compiler backends planned — Unify the two spec-to-circuit compiler paths.
• Retracted verified-system claim abandoned — A 149-bit full-stack proof claim covered toy models; retracted.

Kernel

• The kernel built — The Lean-checked program deciding whether a step is allowed.
• Memory and storage in progress — The log is the truth; replay recovers; storage is proven.
• The orb in progress — A verified network and web stack.
• Admission and re-execution built — Turns are admitted against the law; runs verified by re-execution.
• Capability reshape crown in progress — Reshaping a capability tree by attenuation, proved across the stack.
• CapTP object capabilities built — Sends references between machines, with distributed garbage collection.
• Cells and turns built — State lives in cells; turns change it atomically.
• Conditional and temporal guards built — Conditionals are temporal guards; resolution is monotone; breakage propagates.
• Custom effect carve-out in progress — Programmer-defined effects outside the per-effect soundness closure.
• Effect DSL and apps in progress — A language for effects and apps compiling to Lean-checked actions.
• Durable log and replay in progress — State is the log; recovery replays it over a trusted checkpoint.
• Joint turns and hyperedges built — Several parties' legs commit atomically when they share a binding.
• Intents and ring matching in progress — The kernel matches user intents into atomic rings.
• Lean decides runtime verdicts in progress — The Rust node calls verified Lean exports for decisions.
• Proofs found 12 bugs built — Formalising the engine found twelve defects in project code.
• Verified compiler lowering in progress — All fourteen compilation stages lowered and proved, with an allocator.
• Verified HTTP serving in progress — A web server checked against the HTTP specification.
• Stock mesh clients enrol built — Unmodified mesh clients enrol with and ping the node.
• Proven down to metal planned — Extends the proof chain from source to machine code.
• Four protocols, one process built — One process serves four network protocols.
• Partial-turn promises in progress — Commit a transition's shape now; a guarded value fills a slot later.
• Receipts built — Each turn's receipt binds the whole post-state against tampering.
• seL4 abstraction in progress — The verified seL4 microkernel modelled as the lowest authority rung.
• Storage rebuilt in Lean in progress — Storage proven in Lean and exported; the node does not call it.
• Universal memory primitive in progress — A hash-based memory argument for cells, plausibly post-quantum.
• Upgrades never brick cells built — A stale program falls back to the owner's signature.
• Anti-ghost property in progress — Unwritten fields cannot change without breaking provability.
• Only connectivity begets connectivity built — Every new authority edge traces to an authorised generator.
• Value cannot be created built — Each turn's balance changes sum to zero, proved for the machine.
• Transaction-level crash model in progress — Crash recovery described at whole-transaction granularity.
• Death is temporally decidable built — Creation is provable; permanent absence is globally undecidable; leases bound it.
• Lean owns 18/36 effects in progress — The proved Lean kernel computes half the effect verdicts.
• Opt-in caching rules in progress — Nine caching requirements met, on an opt-in path only.
• Core HTTP suite 17/17 built — The core HTTP conformance suite passes by default.
• Receipt chains built — Receipts form an append-only history a light client follows.
• Restart cannot resurrect draws built — A restart cannot replay an already-spent draw.
• Rewind onto disk planned — Time travel to states no longer in memory.
• Sleep captures the image in progress — Suspend captures the full live image.
• Storage floor re-grounded built — A refuted storage assumption re-grounded over a real game.
• Proven storage market planned — Strangers sell storage; erasure coding and retrievability proofs show it holds.
• Delete Rust twins in progress — Remove Rust copies of decisions Lean already proves.
• Wire 24 exports planned — Connect shipped Lean exports that no running code calls.

Network

• Agreement in progress — Consensus and finality: a record no single operator can rewrite.
• The crossing in progress — Reading another chain's facts by proof, not a bridge operator.
• The fold in progress — Compressing a history of steps into one light-client-checkable proof.
• Asynchronous liveness planned — Guaranteed progress under unbounded message delays.
• Leaderless consensus in progress — A block-lattice consensus protocol without a coordinator.
• Committee reconfiguration in progress — Adding and removing validators without breaking safety.
• Dregg settling onto dregg in progress — The chain's own history settles its folded proofs.
• Federation survives restarts in progress — A federation recovers when operators restart.
• Finality gate built — Holds a block until enough enrolled hybrid-key validators sign.
• Five independent operators planned — A committee of five unrelated operators.
• Light client in progress — Holds one root, re-runs nothing, learns history was authorised and fresh.
• STARK-ified light clients built — Four chains' light-client checks emitted as circuits with no-forgery theorems.
• The linking tower built — What a root-holding client may believe, rung by rung, assumptions named.
• Midnight and Tendermint clients built — Light-client verifiers for more chains, formalised in Lean.
• Mina semantic light clients in progress — Mina verifies dregg and dregg verifies Mina, semantically.
• Multichain settlement in progress — Proof-carrying settlement on Solana, EVM and Cosmos.
• Deployed chain: one validator built — The live beta chain runs one validator, tolerating zero faults.
• Token mirror bridge built — A conserved mirror of an external token, minted by trusted oracle.
• True peers on chain in progress — An on-chain peer registry so chains verify each other.
• Light-client unfoolability apex in progress — Verifier acceptance implies a genuine kernel transition to the published state.
• Testnet fixture settlement built — A fixture proof advanced a testnet settlement contract to height two.
• BFT safety proved built — Quorum intersection and Byzantine safety proved abstractly.
• Equivocator eviction built — The node evicts and certifies validators signing conflicting blocks.
• Ethereum light client, mainnet built — An end-to-end Ethereum light client validated on mainnet data.
• Automate fold falsifiers in progress — Only 38 of 132 fold-breaking tests run automatically.
• Health check misses wedges in progress — The health check reads green on a stalled chain.
• Many turns, one proof in progress — Recursively folds a chain of turn proofs into one proof.
• Proof-of-holdings voting in progress — Holders on another chain vote by proof, keeping custody.
• Kimchi accepts our circuit built — Mina's proof layer accepts a dregg-authored circuit.
• Derived key in Mina state built — A dregg-derived verification key is stored in Mina account state.
• Never-ending fold, wired planned — An incrementally verifiable chain proof a running node invokes.
• Close minting and omitting planned — Light clients cannot be fooled by minted or omitted history.
• Anchorless turns refused built — The node rejects turns lacking the foreign chain's anchor.
• Two Pickles verifiers refuse in progress — Making two Pickles verifiers accept genuine proofs.
• Rebuild Mina's prover in progress — Reconstructing Mina's prover from its sources to check fidelity.
• Catches reordering in progress — Light clients detect history reordering, assuming a sound proof system.
• Fault tolerance simulated built — Faulty-validator tolerance shown in simulation at four and seven nodes.
• Summit premises retyped in progress — Two vacuous apex premises restated over satisfiable ground.
• Three bridges to proof in progress — Replace committee-trusted bridges with proof-based ones on three chains.
• Three hosts, 41 blocks built — Three machines agreed on 41 blocks, once.
• Reconcile two orderings planned — Two orderings of one history must agree.
• A verified Ethereum machine planned — Ethereum opcode semantics in Lean; zero of about 140 done.

Worlds

• Agents in progress — Renting a mind inside explicit rules, with a receipt.
• Markets in progress — Checkable fairness: clearing, launchpads and private exchange.
• Outside facts in progress — Makes web pages and oracle answers provable.
• The workspace (DEOS) in progress — A desktop where every action is a checkable fact.
• Worlds and games in progress — Games and shared worlds whose rules are theorems.
• Agent confinement red team built — Adversarial review of agent containment.
• Forkable agent sessions in progress — Confined-session forking library, not yet wired in.
• Hosted agents platform in progress — Hosts user agents as durable, leased services.
• Jailed agent body in progress — Runs an agent with a real model inside a confined body.
• Agent mandates and budgets built — Agents act under a mandate and budget proven in Lean.
• Tool surface reports execution in progress — The tool interface returns exactly what ran, with receipts.
• Offline browser verification built — A browser checks three rungs of an agent claim serverless.
• Public arcade catalogue built — Nineteen shared offerings, including a Telegram mini app.
• Attestation weld in progress — Checks attested web responses are genuine, well-formed, uninjected.
• Automatafl verified game built — 11x11 board game where every move is a theorem.
• Categorical rewriting with freshness in progress — Rewriting framework for effects with freshness conditions.
• Checkable economy planned — Rented compute and storage with provable fees and shares.
• Uniform-price clearing in Lean built — Market clears at one price under a Lean-proven rule.
• Collective fiction platform in progress — Collective storytelling with voting and replayable randomness.
• Creature the server cannot explain planned — The server cannot justify its behaviour afterwards.
• The Dark Bazaar in progress — Private clearing over sealed orders at bounded sizes.
• Affordances as gated turns in progress — UI elements are capability-gated turns returning receipts.
• One card, five backends built — One card description renders on five display backends.
• Desktop turn on verified kernel built — A turn issued from the desktop commits on the verified kernel.
• Documents as cells in progress — Lean document core in the browser; edits commit as turns.
• Embeddable world in progress — Embeds a world and its editor in any web page.
• Replay and branch stitching in progress — Replays sessions from receipts and merges forks.
• Proving what the screen showed in progress — Proves what a user saw when they acted.
• The Descent in progress — Daily dungeon; proof gates the record, host gates play.
• Distributed live image in progress — The live image spread across machines as one world.
• Self-hosting forge in progress — Code hosting and builds as cells, so dregg builds dregg.
• DrEX in progress — Sealed-batch exchange with one proved clearing rule per batch.
• Fair batch auction design in progress — Frequent batch auctions as the market fairness model.
• Game engine roadmap in progress — Game engine plan with a gate that can reject unfun designs.
• Independently published notary planned — A notary run by someone other than the project.
• Injection matcher in Lean in progress — Ports the prompt-injection matcher to proved Lean.
• Launchpad in progress — Token launch whose fairness is a theorem; not yet runnable.
• Live model session in progress — Drives a live model session through the attested channel.
• House cannot look planned — A market whose operator cannot see orders.
• Mobile and Android cell in progress — Runs the workspace on phones as a cell.
• MUD and living world in progress — Text-world substrate for persistent shared play.
• One bridge, six relations in progress — One proved bridge reused across six relations.
• Sandstorm-style app grains in progress — Packaged apps run as confined per-user grains.
• ZK oracle endpoints in progress — Turns oracle responses into checkable statements.
• Atomic metering and reserve draw built — Compute charging and reserve draw happen in one write.
• Real model in the jail built — A production language model runs in the confined body.
• Receipts survive crashes built — A crashed body still leaves checkable receipts.
• Four attack certificates refused built — The proved clearing refuses four constructed manipulation attacks.
• Differential test found 4 bugs built — ~580 differential scenarios found four engine bugs.
• Circuit key reused built — One emitted circuit key serves a second game.
• Hand-written AIR deleted built — The Rust rule engine was replaced by the Lean-emitted circuit.
• Market beyond three bids in progress — Scales the runnable market past three bids.
• Verified-desktop claim retracted abandoned — The claim rested on definitional theorems and was withdrawn.
• Answer key off the client in progress — Keeps the game's hidden answers off the player's machine.
• Beyond eight state fields planned — Lifts the 8-field cell state ceiling.
• Permadeath proven of model built — Permadeath is proven of the game model, not the client.
• AMM with hidden reserves in progress — Constant-product AMM with hidden reserves and public invariant.
• Book hidden from prover planned — No prover party sees the order book.
• Move activity in-protocol planned — Markets still run outside the chain's own rules.
• Fixture attestation speed in progress — Fixture attestation is fast; the real path is much slower.
• Grammar checked in-circuit in progress — One grammar is checked in-circuit; the JSON leg runs in Rust.
• Resharing only attenuates built — Rights shrink at every resharing hop.
• Galley content layer built — World content layer with a re-emitted, gated root.
• Live station, seven views in progress — A live station with seven views, five still filling.
• Node boots in 8 seconds built — Moving ~920 declarations out of init cut startup.
• A window is a permission built — A window confers an edge exactly when it carries write rights.

Commons

• The polity in progress — Verdicts are witnesses, not reported counts.
• Off the laptop in progress — Reproducible builds, frozen genesis, a node others can run.
• Three dispute regimes ranked in progress — Dispute mechanisms ordered by binding strength.
• OpenSolve regime typing in progress — Settles every ballot-regime claim by regime.
• Checkable frozen genesis planned — Byte-verifiable genesis and a protocol-freezing ceremony.
• Honest status badges built — A badge went green on a hostile oracle; gates now read artifacts.
• Local gate suite built — Local script running every gate, stricter than hosted CI.
• Governance without custody in progress — Governance that never holds assets on any chain.
• Path of Angels beta in progress — Public world outsiders play and verify unaided.
• Collective-choice corpus in progress — Lean corpus of collective-choice constructions for the commons.
• Public devnet in progress — A durable public node with documented operator kits.
• Reproducible build and freeze in progress — A bare clone builds from pinned inputs; the protocol freezes once.
• Secret tallies planned — Ballots counted unlinked from voter keys.
• Public site and ledger built — Grades every claim as proved, running, mounted or frontier.
• Unforgeable verdicts built — A verdict is a council-checked witness, not an assertion.
• Rebuildable deployed image planned — The deployed image rebuilds bit-for-bit from the repository.
• Pin the Lean toolchain planned — Pins the Lean toolchain as Rust's already is.
• First settled journey built — The first world journey settled end to end.
• Stranger plays and verifies planned — An outsider plays and checks the root with no operator.
• Ratchets run by machine in progress — Quality ratchets run automatically, not by hand.
• Binding displayed tally planned — The displayed tally is not yet the binding one.

Mini

Bread's small successor: a shared programmable world where Lean decides what is allowed.

Proofs

• Objective Bend in progress — Lazy open recursion over first-class partial specifications.
• Proof systems (Selvage) in progress — Composes proof components; states what proofs establish.
• Gates and evidence built — Scripts and snapshots that make claims fail loudly.
• Core4 calculus and machine built — Tiny core calculus run by a demand-driven machine.
• Other executors in progress — Preview interpreter, C machine and research circuits.
• Selvage fabric in progress — Typed joints between heterogeneous proof dialects.
• Types and quantities built — Checker typing Core4 terms and tracking value usage.
• BaseFold and FRI pieces built — Lean-checked BaseFold and FRI reductions.
• C backend (oracle) built — C machine differentially tested against Lean, unproved.
• Checkpoint codec built — Machine state saves and restores exactly between turns.
• Reference semantics built — Deterministic step relation defining mix and fix, laziness included.
• Call-by-need machine built — Heap-and-stack machine running Core4 with at-most-once thunks.
• 120-bit error budget in progress — Theorem-level soundness error accounting toward 120 bits.
• Fast proved machine built — Linear-heap machine proved equal to reference; milliseconds, not seconds.
• Homomorphic Bend in progress — Public Bend on encrypted inputs; BFV theory unused.
• Termination of residents planned — No check yet that well-typed resident segments terminate.
• Instances are accepted in progress — Elaborate instances as substitutions of the checked template.
• Machine completeness built — The machine finishes every closed term the reference evaluates.
• Machine soundness built — A finished bounded run returns the reference value.
• Modular typing built — Templates are checked once; instances are provably accepted.
• Bar for proof admission built — Clauses a proof carrier must meet before gating effects.
• Proof-producing checker built — Returns a typing derivation; checked programs never reach refusal.
• Native prover kernels in progress — Rust NTT, hashing and multilinear kernels chosen by a Lean plan.
• Unique-decoding floor refuted abandoned — An assumed decoding-radius lemma was false and recorded as refuted.
• Theorem snapshot gate built — Byte-pinned theorem statements and axiom sets checked by one script.
• ZK for Objective programs in progress — Statements rest on a premise only five literal programs satisfy.
• Verified ML matmul checker in progress — Matmul checker and BaseFold audit for ML inference.

Kernel

• The authority kernel built — Trusted core deciding whether a proposed world change is allowed.
• Activities, calls and sends in progress — Programs yield typed plans and resume with answers.
• Admit or refuse a change built — Lean admits or refuses each proposed change.
• Legacy BendTT path abandoned — The old Bend evaluator was removed; Git keeps history.
• Source front end built — One Lean front end turns .obend source into Core4.
• Hyperdocuments built — Kernel documents with marks, links, transclusion, history.
• Lean decides, Rust carries built — Lean alone defines meaning; Rust moves bytes and runs kernels.
• Concrete representation in progress — Replace octet lists; node costs exceed throughput.
• Admission by re-execution built — The receiver reruns source under signed limits and public tariff.
• Resources, grants and receipts built — Owned resources, delegable revocable rights, a receipt per change.
• Activity turns built — Each activity step is a signed command with a receipt.
• Ancestry and method combination built — Inheritance order from a published, tested linearization.
• Calls and sends in progress — Objects message each other; no journey row exercises it.
• Causal version history built — Edits form a causal DAG giving forks and merges meaning.
• Time as a cell built — A clock cell lets laws reference time without wall clocks.
• Consent anchor built — Binds member consent into the admitted record.
• Marks and annotations built — Marks and annotations are typed document content.
• Delegate and revoke built — Owners grant narrower rights and revoke them.
• Hash from source in progress — A digest primitive for programs; Core4 has no digest term.
• Durable store built — One directory and key file; reopening recovers receipts exactly.
• Lost reply, same retry built — Exact retries return the original receipt once.
• Independent fixture authority in progress — Judge generated fixtures against a hand-written authority file.
• Agent fleet signing built — Many agents sign turns for one owner.
• Resume equals machine yield in progress — Resume matches the machine, under an open premise.
• Single-use invitations built — Single-use right to one contract role.
• Journey as definition of done built — One script runs journey J0-J8 on fresh stores.
• Next-key rotation in progress — Pre-committed next key; rotation keeps identity.
• Laws inside objects planned — Object laws as compiled source clauses.
• Composable laws in progress — Write predicates composed from clauses into a decidable check.
• Primitive arithmetic in progress — Comparison, division and remainder as constant-cost machine steps.
• Native acceptance journey built — Accepts an invocation, refuses 13 bad cases, replays.
• Durable objects built — Objects with durable identity and a payer-funded lifecycle.
• Admit by proof planned — A verified proof carrier gating effects, replacing re-execution.
• Seats (offer safety) built — One contract side with an unforbiddable exit.
• One public price list built — One tariff charged against a signed envelope.
• Source language semantics in progress — Prove the elaborator preserves .obend source semantics.
• Upgrading objects planned — No upgrade turn exists yet.

Network

• Agreement and traffic in progress — Replica agreement and hiding who talks to whom.
• Agreement mesh in progress — Generic Simplex consensus engine in Lean, compiled native.
• Storage-node link in progress — Publishes releases to and consumes replies from fn.
• Traffic privacy in progress — Post-quantum cohort mix with cover traffic hiding senders.
• Anonymity statement planned — A proved observation game behind the anonymity claim.
• Finality gate built — Only enrolled creators' blocks count toward finality.
• Simplex safety built — Safety proved over the model; four replicas ran.
• Hybrid post-quantum key exchange built — Combines classical and post-quantum key exchange.
• MPC backend in progress — Four holders evaluate Boolean circuits on secret shares.
• Multi-party domains planned — Jointly governed communities on a multi-operator Simplex mesh.
• Second node over fn planned — Two stores exchange an owner-signed selected release.
• Liveness in progress — Mesh liveness is not established.
• Reconfiguration built — Replica sets change under the engine.

Worlds

• Worlds and places in progress — Documents, rooms, shells and authored worlds.
• Agents and residents in progress — Agents summoned into rooms with delegated tools.
• Authored worlds in progress — Markets, ballots, bounties as Objective Bend programs.
• Docuverse and shell built — Shell and browser over documents, boards, rooms.
• Hosted apps (SPK) in progress — Sandstorm-style packages run as grains.
• Ballots and dues built — Sealed single-use ballots and dues as programs.
• Bounty board in progress — Escrowed reward pays on approved work or returns.
• Chat in progress — Chat verbs compiled; joined to no Host run.
• Discord entrance in progress — Friends reach Mini via Discord; simulated only.
• DrEX as seats in progress — Exchange built from seats; preview and kernel landed.
• App serving a browser in progress — No hosted app has served a browser yet.
• Librarian in a room in progress — Agent answers in a room; off publicly.
• MUD sheet laws in progress — Theorems on text-world sheets, items and clocks.
• Private rooms in progress — Client-sealed rooms; node holds wrapped keys; unaudited.
• Resident notes in progress — Resident notes follow document revisions.
• Rooms and invitations in progress — Rooms, invitations, workroom template on dev worlds.
• Shell verbs built — Shell verbs from keygen to export; on public node.
• Grain lifecycle built — Grain install-to-export lifecycle: 44/44 rows.
• Studio in progress — Edit, fork, history and preview workspace source.
• Read-only web face built — Read-only loopback hypertext view of the world.

Commons

• Friends, deploy and money in progress — Public node, onboarding, payment and tenancy.
• Onboarding and tenancy in progress — How friends join, keep keys and pay.
• Public node built — One public node: shell and documents on devnet.
• Consent-safe client SDK built — Members sign only intents they confirmed.
• Pay to enrol in progress — Solana token payment enrols a key; recorded answers only.
• A friend enrolled planned — An outside member enrols and acts; none yet.
• Friends guide built — One page stating what the public node has.
• Journey green on main in progress — Main passes every journey row; three rows failed.
• Public shell candidate built — Public node runs 2026-10-01 candidate; no outside members.
• Re-genesised candidate in progress — Fresh public node from main with Objective and pay-to-enrol.
• Small footprint planned — Node fits a tiny VPS, runtime included.
• One account per friend in progress — Key broker gives each friend an account; never run.

fn

An NNTP news server whose decisions are made by ACL2-verified code.

Primitives

• Authors and signatures built — Author signatures over exact authored bytes.
• Hybrid signatures built — Signatures need classical and post-quantum halves.
• Author key lifecycle in progress — Enrolling, rotating and succeeding an author's keys.
• Signed source bytes built — Signatures cover exact authored bytes, not relay headers.
• SHA-256 store digest abandoned — First digest for store contents; replaced by BLAKE3.

Proofs

• Proof engineering and assurance in progress — ACL2 theorems about functions the server calls.
• Assurance ledger built — Claimed theorems must concern functions the server calls.
• Extracted CHICKEN build in progress — Program extracted from ACL2 serves a store byte-identically.
• Fundamentals F1 to F8 in progress — Eight measurable bars required before first release.
• Host coordination into ACL2 in progress — Hand-written locking becomes generated or proved ACL2.
• Ten-second proofs built — Any book over ten seconds at two jobs is a defect.

Kernel

• Durable store in progress — Keeps accepted articles; recovers exactly after crashes.
• Native image and footprint in progress — Compiled native image, small footprint, no Python.
• Owner runtime in progress — One owner decides every request with costed work.
• Catalog reads in progress — Lookups use an index, not scans.
• Checkpoints and compaction in progress — Stores shrink without freeing a live page.
• Connection multiplexing built — Idle connections cost kilobytes, not threads.
• Byte-level crash model built — Disk cuts, torn writes and fsync gaps modelled.
• Group commit under load in progress — Under one fsync per POST at eight posters.
• Retention built — Posts kept until released; refused without capacity.
• Live reconfiguration built — Configuration as durable records; no half changes visible.
• Memory floor in progress — A node running deeply under 256 MB.
• Native host image built — A node is a compiled SBCL image without Python.
• Octet lists at runtime abandoned — Holding payloads as octet lists at runtime.
• Owner scheduler in progress — Controls answered by deadline under one owner.
• Page store (format 10) in progress — Copy-on-write page store, proved reclamation, BLAKE3.
• Python diet in progress — Delete Python remaining outside the deployed runpath.
• Python host services abandoned — Original Python host calling ACL2 via bridge.
• Record log (format 9) built — Chained segments with proved crash keystone.
• Resource contract built — Stated cost per request; generated limits table.
• Store migrations abandoned — Converting old stores to new formats.
• Adversarial time model in progress — Disk, network and clock modelled as adversaries.
• Heap from store profile built — ACL2 sizes heap from profile and memory.
• Online reclaim in progress — Live space reclamation, opt-in per decision D53.
• Power-loss campaign built — 570 crash and power cuts with no violation.

Network

• Bundle Protocol transport in progress — Articles cross nodes over Bundle Protocol, through outages.
• News service (NNTP) built — NNTP so ordinary newsreaders read and post.
• Accounts and authentication in progress — Invited accounts; AUTHINFO and SASL decided in ACL2.
• 10 MiB bundles built — A 10 MiB message is reassembled and delivered.
• BPv7 bundles built — BPv7 node with durable transfer and restart recovery.
• Group policy built — Groups moderated or read-only via live configuration.
• Licklider Transmission Protocol planned — Space-grade transport; feasibility note only.
• Multi-hop signed missions built — Signed report crosses four nodes; reply returns.
• fn NNTP extensions in progress — fn NNTP extensions such as dictionary compression.
• Posting and cancels built — POST accepts client Path; cancels are withdrawal records.
• Reading commands built — Fast group listing and article and header fetch.
• TCPCLv4 convergence layer built — Bundles over negotiated TCPCL sessions.
• TLS and public exposure built — Ports 119 and 563 with TLS; ACL2 limits.
• ION binding built — fn drives dtn7 and ION relays for the mission.
• Cancel as withdrawal built — visible(T then C) equals visible(C then T).
• Table-driven CRC-32C built — 1 MiB bundle encodes in 0.058 s, not 3.68 s.
• Exposure limits built — 500 connections from one address: 8 admitted.
• Fragment reassembly built — Uncapped linear-work reassembly refined to a reference.
• Verdict in headers built — Readers see the pinned signature verdict.
• Interop with INN built — fn peers with INN 2.7.4 in a lab.
• Moderated groups built — Moderated-group posts wait for a moderator.
• SCRAM-SHA-256 login in progress — SASL exchange books and verifier v2.
• STARTTLS and implicit TLS built — tin and other clients log in over TLS.
• Wildmat matching built — Bounded UTF-8 wildmat parser and matcher.

Worlds

• Agent surface and Mini in progress — What applications, agents and Mini rely on.
• Competing consumers planned — Competing leased workers; outside 6.6.0.
• Durable consumer contract in progress — Consumer owns inbox/outbox; fn supplies cursor, ack.
• Mini E1/E2 exchange in progress — Mini consumer checks a signed report and replies.
• Opaque article kind in progress — Article kind for opaque payloads, proved accepted.
• Private encrypted groups planned — Confidential groups with a stated metadata boundary.
• Remote consumer in progress — Account-scoped remote consumers built with producers.
• Native web reader built — Browser reader and composer, durable submission path.
• ZeroMQ-shaped patterns in progress — Pub/sub, pair, req/rep generated from declarations.

Commons

• Releases and public node in progress — Versioned tarballs and a public node friends join.
• Final release 6.6.6 planned — Last release, after 6.6.x and 6.7.x.
• Peering with a friend built — A tarball-installed node peers with another.
• OpenBSD 7.9 release built — Tarball runs node on 1 CPU, 2 GB OpenBSD.
• Public node built — Public fn node serves news from an edge gateway.
• Release 6.6.0 cut in progress — First release, held for checklist and 17 gates.
• Version sequence built — Release order is a sequence, not a number.
• Generated changelog built — One line per merged lane, reproducible.
• Cut gates 01 to 17 in progress — Cut only when all gates green on one commit.
• TLS reload built — Renewal reloads the certificate without restart.

Dark Egg

Research on private and verifiable market relations.

Proofs

• Assurance in progress — Ledgers, threat models, refinement matching claims to evidence.
• Privacy backends in progress — Run a relation clear, shielded or fully dark.
• Backend bakeoff planned — Encryption schemes compared on identical vectors.
• Claim ledger built — Each claim with strongest wording, evidence, falsifier.
• Clear mode built — Relation run openly as reference oracle.
• Dark computation candidate planned — Fully dark backend, frozen leakage model.
• Formal refinement chain planned — Lean or Rocq specs refining into the kernel.
• Dark Relation IR in progress — Typed IR with first-class leakage for all backends.
• Shielded fixed-size batch built — Declared executor, sealed receipts; 90,082-case differential.
• Leakage threat model built — Per-role leakage, inference limits, disclosure budget.
• Threshold shielded batch planned — Input validity, committee decryption, explicit aborts.
• Verifiable dark computation planned — Binds input root, program, output and settlement.
• Accelerator hypothesis in progress — Tensor accelerators for encrypted arithmetic; literature only.

Kernel

• Guarded late fills in progress — Guarded one-shot value fills one committed slot later.

Network

• Inclusion and availability in progress — Orders cannot be silently omitted.

Worlds

• Market relations in progress — Exact market relations compiled to several backends.
• Padded batch auction built — Fixed-grid batch auction with golden vectors.
• Confidential energy dispatch in progress — Feasible joint plan keeping plant costs private.
• Private net settlement in progress — Net settlement with public solvency proofs.
• Receipt-compiled order policies planned — OCO and bracket orders compiled from receipts.
• Multi-token ring clear planned — Fixed-topology clear across several tokens.
• Independent agreement built — Two implementations agree on 300,436,169 batches.
• Manipulation cost in progress — Manipulation cost and bundling effects on clearing.

Commons

• Public test artifact planned — Synthetic-settlement artifact; deployment undecided.

zkML

Research on proving which model produced an output, without trusted setup.

Primitives

• Poseidon2 round analysis in progress — Does a recent attack apply below the round threshold?
• KoalaBear field migration abandoned — Claimed 3.4x gain measured near 1.05x; not recommended.
• Ring-hash design in progress — A Galois-ring hash; attacks reach 2 rounds, a thinner margin than believed.

Proofs

• Proving inference in progress — Post-quantum proofs that given weights produced an output.
• Soundness accounting in progress — Real security bits; flattering numbers retired.
• Verifiable encrypted computation in progress — Verifiable homomorphic encryption of model computations.
• Bit-exact proving in progress — Prove inference in native number format, no tolerance.
• Compiler seam in progress — Categorical compiler hypergraphs as prover front end.
• Post-quantum Vega path in progress — Priced post-quantum hash-based alternative to a folding design.
• Lean-verified artifacts in progress — Lean checks proof artifacts, with an anti-vacuity sweep.
• Weft in progress — Hash-folding scheme reopened with a repair.
• Zero-emulation vFHE in progress — Limb primes equal proof field; no emulation.
• Drop the blowup in progress — Lower FRI blowup: prover 15x faster; priced only.
• FRI bug fix built — Row-order fix: twelve descriptors prove at blowup 2.
• GKR substrate in progress — GKR-style tensor proofs as an alternative proving core.
• Restore grind parallelism built — Windowed search re-parallelised the grind.
• Low-rank updates built — Proving low-rank weight updates.
• Matmul sumcheck built — Fused matrix-multiplication sumcheck, landed in code.
• Proven-regime queries planned — Proven bounds cost about 86 queries for 100 bits.
• Recursion tower measured built — Per-layer recursion costs; refuted two earlier claims.

Worlds

• Trust layer in progress — Sampling audits, weights registry, Lean-checked artifacts.
• Audit game in progress — Commit to everything, prove sampled work, bound leftover risk.
• Committed terminal in progress — Terminal and file system leaving verifiable receipts.
• EVM decompilation in progress — Staged proving of compiled Ethereum contract behaviour.
• Verifiable training in progress — First pieces of proving honest training steps.
• Weights registry planned — Registry binding weights and architecture to claims.