Documents

Reports

Shared

Diane

New message

Send

Tothe teamCcBcc SubjectThursday review

Hi all,

{{ dictTyped }}

Draft saved just now

{{ micTimer }}

Windows. A microphone at the edge of the screen is the whole interface while you speak. Today the text arrives on the clipboard and is pasted where your cursor was; typing it straight into the field is in development.

agent-cage

Run AI coding agents on your own servers, unattended, from a chat — with exactly the permissions they need and nothing more.

Five agents across two hosts run the work behind this site. A security review precedes the release.

The whole fleet is driven from one chat: list agents, read their state, send a file, upgrade a pod. Each agent also has its own group where you talk to the model directly, and agents attach to the Claude app over MCP, where they appear beside your own conversations.

The design: Linux does the isolating

Every component is a separate Unix account, and the direction of trust between them is deliberate. The relay holds the chat identity and routes messages — nothing else. The manager holds bucket credentials and the authority to perform signed upgrades, and passes commands to exactly one agent. The agent holds one thing: the model credential. The executor, where every model-issued shell command runs, holds nothing at all and has no route back.

Commands flow one way — manager → agent, never the reverse — so a compromised agent cannot reach up into the privileged manager, and a prompt-injected model acting as the executor cannot escalate beyond the account it was given. Nothing here is a novel security mechanism, and nothing is a virtual machine: it is the operating system’s own permission model, applied with care, so the agents can still do real work — build, test, even run their own VMs — on hardware you never have to touch from your laptop.

Two modes

Native harnesses, kept current

agent-cage does not replace a vendor's agent with its own: Anthropic models run in Claude Code, OpenAI in Codex, Z.AI in theirs — and one harness can call another as a tool. Harnesses change several times a month and must be updated the day a new model ships, so an upgrade is one command from the chat: a signed release into a shared read-only Nix store, a pod restart, a report of what changed.

How it is built

One statically-linked Go binary is every daemon, every installer step and the shell shim, with no third-party Go dependencies — nothing has to be vendored, audited or trusted with credentials sight unseen. Nix pins the sandbox image, the toolchain and the signed-upgrade path to one closure.

Where this stands

Molt Petit

A consensus protocol small enough to understand in a minute, with deterministic fast finality — and a deep analysis of what happens to it when keys are rotated, stolen or briefly exposed. Machine-checked from the Rust implementation to Lean 4 theorems. The consensus core of Ledger.

Every headline theorem is gated by a checked-in axiom audit down to Lean's three classical axioms. PDF and artifact.

In one paragraph

A node — in particular a light client that is not always online — holds not a chain but a constant-size certificate plus a short suffix of recent signed blocks. Given only that and a clock, it can re-sync to the latest consensus state without replaying history. A fixed, equally weighted roster; a deterministic round-robin slot schedule; and a single cumulative window-density rule in place of votes, quorum certificates and view change. Signing-key rotation is part of the consensus core.

Keys, in practice

Most protocols treat a signing key as either honest or compromised. Molt Petit distinguishes three events that look alike from the outside and are not: a key rotated on schedule; a key extracted and kept by an attacker; and a key briefly in someone else's hands — a leaked backup, a misconfigured signer, an insider with a window of access. Each has different consequences for what can be forged and for how long, and each has a defined path back to safety — theft of a current key heals after a confirmation-gated rotation. The protocol fits in the paragraph above; this analysis is most of the paper.

What is machine-checked, and about what

The protocol is one Rust program, imported into Lean 4 by the Charon + Aeneas pipeline. Light-client safety and the forged-time bound are stated about the emitted validator, not about a hand-idealised model. The same source instantiates a plonky2 recursive-proof circuit, so the prover proves exactly the predicate that was verified; the circuit backend's per-gadget faithfulness is the one stated residual. A second, independent TypeScript implementation is imported by a second pipeline and proved sound to the same model.

What it costs

A closed participant set, equal weighting in lieu of stake, no liveness recovery, and safety statements scoped by the verifier's clock. These are stated up front and situated against prior art in the paper, not discovered in a footnote.

Molt petit is Catalan for very small.

Ledger

Company records that stay correct, and private, even when someone inside — human or AI — has access to every server.

The consensus core (Molt Petit) is proven; the ledger layer above it is designed and not yet built. Component by component, below.

Why

Companies are about to run AI agents inside their own infrastructure: wide access, machine speed, and motives that are not fully legible and can be altered from outside by a line hidden in a document. Organisations learned, more or less, how to hire people without fearing them. With AI insiders that is still open.

Ledger answers a narrower question: how to keep the records that matter most correct and private when something inside the perimeter — with access to every server — may be wrong or turned. Financial state is the first application, because the cost of an error is clear and unrecoverable. Access-controlled documents in a law firm or a large corporate are the next.

What it is

A Kotlin/JVM library over a shared, seven-operator service. To the institution integrating it, it behaves like a database driver: open an account, move a balance, read consistent state, each call carrying its own authorisation. Underneath there is no single database and no single operator who can be wrong or dishonest on their own. Changes are ordered and validated by seven independent institutions running a consensus protocol whose safety properties are machine-checked theorems, and the whole history is carried by a constant-size zero-knowledge certificate rather than by anyone's copy of the records.

Two things follow that are hard to get any other way. An attacker who fully controls your infrastructure cannot make the ledger accept an invalid change — the validity decision does not run inside your perimeter. And a settled transaction cannot be reverted, whatever subsequently happens to the systems that produced it.

What is visible and what is not

Each institution has a shard — its own ledger, fully visible to it and to nobody else. Outside the shard, its state is a single cryptographic root. The operators verify a batch without learning its contents, its structure or how many transactions it contains. Every submission carries two independent attestations: a signature, saying which institution stands behind it, and a zero-knowledge proof, saying the change obeyed the rules. They answer different questions and fail differently, which is the point.

What holds when the shared infrastructure is attacked

Safety holds as long as compromised slots plus stolen keys stay within two of the seven in any window of seven slots. Exceeding it means compromising three independent institutions at once — different companies, different clouds, ideally different enclave vendors and jurisdictions. Stolen keys die on rotation. A forced conflict names its authors: producing two conflicting states leaves non-repudiable evidence identifying which operators equivocated, which is what makes the consortium's contractual exposure enforceable rather than decorative.

Rules inside a shard

Accounts carry their own rules, enforced automatically and checked twice by different parties on different bases. Multisig backed by hardware keys — a phone's secure element is a perfectly good signer. Time locks with a cancellation window held by a separately-keyed party: the control that matters most against an attacker operating at machine speed. Receipts from external services as inputs; certificates for counterparties and auditors as outputs. And external settlement credentials held in a TEE that verifies the ledger's proof before it will authorise anything.

Where this stands

What it does not do

If an action is inside the envelope declared in advance — properly authorised, past its grace period, rule-respecting — the ledger will accept it, whoever initiated it. Nothing here divines intent. The operator set is fixed and closed; there is no liveness recovery, so a broad simultaneous outage halts the ledger rather than degrading it, with safety untouched; and safety depends on reasonably synchronised clocks. These are the price of deterministic finality at a fixed depth and a client that needs to hold almost nothing.

Not a replacement for a core banking database: the integrity layer for the operations where being wrong is unrecoverable. The long tail stays where it already is.

Proof-driven development

AI agents change the economics of formal verification. Yak's research programme is about what that makes practical: moving the critical parts of a system from tests that sample its behaviour to properties proved about the artifact that ships.

The economics

Formal verification has always been the right tool for software whose failure is unrecoverable, and almost never the tool actually used. The reason was never doubt about the result. It was the cost of producing it: proofs written by hand, by specialists, at a pace of lines per day — and reopened by every change to the code. Agents change exactly that term. Proof search, restatement, and the tedious re-proving after a refactor are work a model can grind through and iterate on at negligible cost, while the thing that decides whether the proof is right — the checker — stays small, unchanged, and impossible to persuade. The expensive part became cheap; the trustworthy part stayed trustworthy.

The shift

For most software the pipeline is requirements → implementation → tests, and the tests catch what they were written to catch. Where that is not good enough, proof-driven development turns it into requirements → formal properties → implementation and proof search → an executable artifact the theorem is about. The properties are written before the code, as the things the system must never do. Code and proof are then developed together, largely by agents, against a checker that takes nobody's word for anything.

What it does not claim

Not that tests disappear. Tests and proofs are tools for different layers, used together: proofs for the handful of properties whose violation cannot be undone; tests for behaviour, integration and everything a specification would only restate; measurement for performance, about which no proof has anything to say. Not that a proof about a model is worth much — the theorem has to be about the artifact that ships, or it is decoration. And not that judgement leaves the loop: the properties themselves still have to be the right ones, and the method makes that human decision more important, not less.

First example: Molt Petit

Molt Petit is the first substantial system built this way at Yak. A consensus protocol was written once, in Rust; that source was imported into Lean 4 and its light-client safety proved — a development of about fifteen thousand lines, every headline theorem gated by a checked-in axiom audit — with proof search and iteration carried largely by agents. The same source instantiates the recursive-proof circuit, so the prover proves exactly the predicate that was verified. The method is documented in the paper's appendix, so that a reader can judge it rather than take it on trust. The paper and artifact.

What comes next

The Ledger layer — accounts, shards, committed state — is intended to be built the same way, on top of the proven core. Alongside it, notes on the method as it matures: what agents are good at in a proof and where they are not, and what the tooling has to look like for a team that is not made of Lean specialists. More work is intended, and will be listed here as it becomes real.

Consulting

Architecture, protocols and systems that are meant to keep working — built or fixed with extreme rigour, so that they run nearly all the time with minimal maintenance.

Available in limited capacity. Most of Yak's time goes to its own work, so it takes on very little — but a genuinely hard or unusual system is always worth a message, and the answer comes quickly either way.

What

Software architecture and reliable systems. Networking and consensus protocols, and protocols in general. Fail-safe systems and the algorithms beneath them. Blockchain systems, from consensus and ledger design to the client. Applied cryptography, including zero-knowledge proofs. The common thread: designs where correctness is argued, not hoped for, and where the failure modes are enumerated before the code is written.

How

Long-term engagements

Both multi-year, both as external partners embedded with the client's engineering team.

o1Labs2021 – present

Technical leadership and architecture for the Mina protocol and the products around it — today, overseeing execution across the whole engineering team. Earlier: re-architecting the protocol's networking layer, and introducing a data-driven, fully automated experimental approach to the core blockchain implementation, so that every new release is stress-tested before it ships.

Serokell2016 – 2021

Software development leadership for Serokell's blockchain clients: the core team behind Cardano SL — ledger, consensus, networking — through to mainnet; technical lead and chief architect for StakerDAO's products, including a trustless, DoS-resilient token bridge across Algorand, Ethereum and Tezos.