A libre governance layer for AI-assisted work: every agent walk is bounded by a contract, checked by deterministic gates, and recorded in a durable, tamper-evident ledger.
librecode is a Common Lisp (SBCL) toolkit for running AI-agent work as governed campaigns, not open-ended chat sessions. A walker — the LLM-driven process actually doing the work — never operates on a bare instruction; it executes against a boundary refined out of a human's intent until it's precise enough for a machine to check.
Three pieces work together:
| Piece | Where | What it is |
|---|---|---|
| Reference model | src/model/ |
The pure state machine of governed work — DAG, node phases, deposits, event log — with four crown-jewel invariants as executable predicates. |
| Metaharness | src/meta/ |
Campaign orchestration: DAG scheduling, crash-safe journal, native Nickel gates, multi-child supervision with condition/restart recovery. |
| Runner | src/runner/ |
The reference supervisable walker — an event-sourced LLM agent harness proving out the supervision contract (freeze/handshake, cooperative shutdown, resume). |
Today it's driven from a Lisp REPL (just repl), not yet a polished CLI — see
Status.
- A human states intent, often underspecified; an agent presses on the gaps until it's a sufficient IBC (Initial Boundary Condition) — a plain document naming the goal, what's already known, what's delegated to the walker's own judgment, and what must halt and ask rather than be guessed at. The human keeps final say over every detail and scope — the agent sharpens, it doesn't decide.
- An architect maps that campaign-level IBC into a plan — a DAG of nodes, each needing its own IBC drawn from that living plan, which acts as a kind of meta-IBC for the nodes under it.
- The metaharness schedules the DAG and dispatches each node to an isolated worktree.
- A walker executes its node and lands a deposit — its unit of finished work.
- A gate — any deterministic check, whether a Nickel contract or a script the harness runs as a hook — verifies the deposit before it's accepted. A contract is one specific, load-bearing kind of gate, not a synonym for the concept. The walker never supplies the terms of its own checking.
- Every step — findings, decisions, and their why — is written to a durable, append-only ledger, so any reviewer can reconstruct what happened without trusting a summary.
- The human is surfaced only where a delegation table actually requires it (see The human seam) — everything else resolves without a human in the loop.
Hand anyone a non-trivial assignment — homework, a lab experiment, a consulting engagement — and the expectation is universal: do the work, and keep a legible record of it. Show your steps. Keep the lab notebook. File the report. No serious discipline, from grade school to professional practice, accepts "trust me, it's done" as a deliverable. Should we expect less from our AI helpers?
We can't introspect a model directly, so librecode enforces the same discipline externally that we'd expect from any capable colleague:
- A contract states the work requirements — machine-checkable, filled as the work progresses, never graded by the one who did the work.
- Deterministic gates check every deposit of work against its contract. An agent supplies work; it never supplies the terms of its own checking.
- A durable ledger keeps the pertinent record, zettelkasten-style — findings, decisions, and their why — append-only and replayable, so progress is tamper-evident and any reviewer can reconstruct what happened from the record alone.
This isn't a complaint about current models, it's structural: an LLM is a stochastic walk, not a mind, and open-loop generation drifts by default — handed a vague task, it doesn't ask what you meant, it fills the gap with a plausible-sounding assumption instead of surfacing it, and it can't be trusted to grade its own work either. No amount of scale removes this; only external structure closes the loop. So librecode pushes precision to both ends: a contract states requirements before work starts, and a gate — never the agent that did the work — checks the result after.
That's not just risk management. Working with an LLM changes what's tractable, not just what's fast: research and code both move quickly enough that problems previously out of reach on a realistic timeline become worth attempting. But that speedup only holds if direction stays coherent — the bottleneck isn't the model's capability, it's ours. A precisely scoped boundary is what turns "should this stop and ask a human" from a guess into a derivable decision, which is what lets the system move at LLM speed on everything it can, while still reliably stopping for the one thing no model has: the human's actual vision for what's being built. See docs/design.md for the full formal treatment.
The human operator is the only one who can judge whether the work is actually useful and moving toward their goal. There is one exception: when a claim and the goal it is measured against are both stated precisely enough, whether the claim satisfies the goal can be settled by a check that runs and gives the same answer every time. Short of that precision, the call stays with the human.
A wrong answer that reads badly gets caught right away. A wrong answer that reads well is the one that gets past you, because the prose is good enough that you stop checking it. That's the actual failure mode: fluency standing in for verification, not the machine simply being incorrect.
What follows is a prose account of a result that is already proved, not argued here for the first time. The proof is mechanized in Lean 4 and lives in Factoring Trust: A Machine-Checked Characterization of Where Verification Must End, not in this file; this section only explains why the result applies.
Here is why that call can never move off the human, and it isn't a matter of preference. Above two granted assumptions, that the cryptography holds and that the verifier running is the one specified, verifying a claim over an append-only record that keeps growing can fail for exactly three reasons. The count isn't chosen. It comes from one direction of a machine-checked if-and-only-if: grant all three conditions and the other direction builds a working check out of them, on the spot, out of nothing but those three. A fourth reason would have to be something that construction secretly needed. It doesn't need one, so there isn't one.
Each of the three names who you have to trust and what fixing it costs. A claim the record doesn't settle needs a witness of history, someone who saw what happened and says so. A claim the record holds but nobody can check needs a voucher, someone whose judgment stands in for the check that can't run. A claim that stops being true as the record grows needs a holder of liveness watching it stay current, or an accepted expiry on how long the claim is good for.
Only two kinds of evidence close any claim at all: a check that ran and that anyone can run again, and an admitted party's testimony, someone recognized to speak for what happened, which nobody can run on their behalf. An artifact's own declaration about itself is neither one. It never closes a claim by itself, no matter how it's phrased.
There's a ceiling to how good this can get, and it's exact. A system sits at the best state it can reach exactly when the only thing still trusted is the assumptions it started with, named up front. That's also an if-and-only-if: reaching that state and having nothing else trusted are the same fact, not two facts that happen to travel together. "Cannot be improved on" is therefore a proved statement about a system that reaches it, not a boast about one that hopes to.
Now point this at a harness. "Did the agent do useful work toward my goal" is a claim about the record, and it's the first kind: nothing committed to the record settles it, because usefulness is measured against a goal that lives in the human's head, not in the record. No amount of tooling, tests, or agent cleverness closes a claim of that kind, because the argument above says nothing does, short of a party willing to testify. The only move left is to name that party. The party it names is the human. A harness that reports its own success is trying to close that claim with the artifact's own declaration, and that's exactly the move that never closes anything. That's the shape of the problem, not a design choice librecode made, and it holds for every harness whether or not the harness knows it.
That's also why the agent can never be the witness. It can run a check, and it can enumerate; neither of those is testimony about the world, and it sounds exactly as convincing when it tries to supply that testimony as when it's doing its actual job.
None of this makes a misgrade impossible, and any harness claiming otherwise is committing one. Whether a claim was graded correctly is itself a judgment, and judgments aren't settled by machinery, same as "useful" wasn't. What the structure buys is narrower and it is provable: the places a misgrade can hide are enumerable. The set of things still resting on trust is computed from the record, not estimated, so nobody searches prose for a bad grade. They are handed the list.
That turns an unbounded job into a bounded one, and the rest of this system exists to shrink what is left. Sweeps run over that list rather than over the project, checking whether each claim's cited authority says what the claim says it says. What they turn up goes back through the same seam everything else does, which means the human sees the disagreements and not the sweep. Gates hold the shape of the record so the list stays computable as it grows. None of that makes the reading free. It keeps the part that reaches a person small enough for them to actually follow it, and that is the end the whole arrangement serves. A record nobody can keep up with has stopped being useful, however well it is kept.
What proves the system is working isn't a conversation that felt productive. It's a record with more claims that survived grading than it had an hour ago, counted against how much of the human's attention it cost to get them there.
Three roles carry that split, and they're kept apart on purpose. A frontend talks to the human and has no access to the record at all; its one job is making sure the human is genuinely caught up, on the human's own request and never on the frontend's assumption that they needed it, in an actual back-and-forth rather than a report handed down. That job overrides anything a worker thinks matters more. A keeper has one goal, a record with nothing false in it, and checks every claim a piece of work touches before it ever calls on the composer. A composer conducts the working roster (maintainer, architect, workers, reviewers, surveyors, test engineers) and never addresses the human at all. The frontend and the keeper deliberately withhold the evidence behind their own reasoning from each other; a frontend that has seen the keeper's measurements, or a keeper that has heard the frontend's read of the conversation, has stopped being a check on the other. That's a failure condition, not a shortcut. The human reaches the record only by going there directly, never through either agent's account of what's in it. Nothing about that split is temporary.
Escalation runs through a council of specialized seats (architect, composer, lead-maintainer, auditor), each owning a slice of the decision space. A delegation table routes every decision-type to its owning seat and the assent it requires (a single seat, a subset, the full council, or the human), so only the decisions that genuinely need a human ever reach one. Three seam classes dominate that traffic:
- Novelty-bounding: greenfield work, closed by writing a sufficient IBC.
- Divergence-alert: real-time deviation from a mapped plan, surfaced immediately rather than held until review.
- Coherence-judgment: the human's quality call at close, which overrides any agent's self-assessment.
See docs/design.md for the full delegation table.
Prompt variation can't fix what a model systematically cannot see: errors stay correlated through the model itself. Only genuinely different models break that floor — which is why librecode is heterogeneous-first, composing disparate models (and deterministic checks, and the human) rather than deepening a bond with any single vendor. No incumbent can build this: composing competitors is structurally against their interests. Freedom here isn't ideology bolted on — it is the enabling condition of the math. See MANIFESTO.md and docs/foundations.md for the full argument.
Pre-1.0 and molten — still being reshaped freely, no API stability promised yet. The proof-of-concept is reached: a real supervised subprocess walker with working tools, a native gate producing a gated artifact, mid-run kill/resume, and a runnable end-to-end demo against a local model. The current push is a usable MVP — librecode governing real day-to-day campaigns, including its own development.
Inside the Nix shell (shell.nix provides SBCL and dependencies):
just build # compile all systems
just test # FiveAM + check-it suite
just repl # interactive REPL with everything loaded
just repl-drive # REPL loaded to charter and drive a real campaign
just demo # end-to-end campaign demo against local Ollama
just repl-drive is the native (non-TUI) way to charter and drive one real
campaign end to end from the REPL — build a DAG, dispatch it against a real
provider, and watch deposits, gates, and the journal as they land. It's a
library, not a script: see demo/repl-drive.lisp's header for the full
interactive session recipe.
- MANIFESTO.md — why libre, why now
- docs/foundations.md — first principles: the decorrelation theorem, the null hypothesis, what "stable" means
- docs/design.md — the campaign lifecycle, council protocol, human seam
- docs/model.md — the reference state machine and its invariants
- docs/roadmap.md — workstreams and sequencing
Not yet declared (pre-release).