One lap of the loop, on a real project

Four essays into this series I have described a loop and argued for the machinery around it. All of that was description. This one is a single run: twelve recorded cycles on 4 August 2026, from an empty repository to a working tool, every artifact below taken from a repository you can open.

The thing being built is small on purpose. In March, an engineer finds a security bug in her own product and writes it up. In August, a stranger reports the same bug and asks for the bounty. Her team believes they already knew, and cannot prove it: any document they produce now, they could have written this morning.

They could have hashed the write-up in March and published that hash somewhere nobody can rewrite, a blockchain being the usual answer, which puts the date beyond dispute. But a hash is all-or-nothing: to let the stranger check it they must hand over the whole document, including the paragraph about a second bug they have not fixed yet.

So the team does not hash the write-up as one blob. It hashes every word on its own, combines the hashes in pairs, then those results in pairs again, until one value remains at the top. That value is the root, and each word at the bottom is a leaf. Publishing the root in March commits to every word at once while revealing none of them.

In August the team hands over the words it chooses to reveal and, standing in for each word it does not, that word’s hash. The text with its gaps is a redaction; the substitute hashes and the recipe for combining them are a Merkle proof; and the whole bundle handed to the reporter, redaction plus proof, is a disclosure. Checking one is arithmetic: redo the pairing, and either you arrive at the published root or you do not. Under two assumptions, that no one can find two different inputs with the same SHA-256 hash and that the root really was published in March, arriving at it is only feasible if the revealed words were in the committed document. It says nothing about what the hidden parts contain, and nothing about whether the document describes the reporter’s bug. Those stay human questions.

Hold on to one refinement this run chose to postpone: a whole hidden stretch of words can travel as a single branch hash instead of one hash per word, since the branch above them was already one value. That is the better construction. The day you are about to watch built the simpler one, one hash per leaf. Why it did, and what that cost, is where this story is going.

Every tool has a piece where being wrong is unrecoverable. Here it is the checking itself: a checker that can be fooled lets a team claim knowledge it never had, with nobody downstream able to tell.

So that piece, and only that piece, is written in Rocq. Rocq is a proof assistant: you write the program, you write the property it must have, and then you argue to the machine that the property holds. The machine refuses your argument until it covers every case, including the ones you did not think of. People call such an argument a proof too, which leaves this essay holding two unrelated things with one name, so I will never say the word alone: a Rocq proof is a machine-checked argument that a program has a property; a Merkle proof is the bundle of hashes inside a disclosure. Here the program is the checker, and the property, in one sentence, is that it says yes to a redaction exactly when that redaction came from the document the root was built from. What ships is extracted from what was proven: Rocq translates the argued program to OCaml, and that translation, like the compiler and runtime under it, is trusted rather than proven.

Everything else, and it is most of the code, is ordinary OCaml with ordinary tests. Not because mistakes there are harmless, but because they are cheaper to observe: a crash, a wrong print, a failing test. Two of them, the word splitting and a numeric conversion at the boundary, can be silently wrong, and the repository names them as trusted rather than pretending otherwise. Drawing that line is a decision, and you make one whether or not you notice.

You have seen this ring described in The loop I run; below is that day, arranged as one lap of it. The day ran twelve cycles, and I walk them station by station in the ring’s order rather than the clock’s: the onboarding you will read first actually ran late in the day, and the record keeps every timestamp for a reader who wants the day as it ran. At every stop, the same four things: the job, the tool, what it put on the screen, and what it caught. I took the decisions. The agent, Claude Code driven by the agentic-loop-kit, wrote and ran the code. Each turn of the ring is one cycle, and every cycle of this run was recorded.¹

Onboard the engineer: confidence has a shelf life

The first box closes one gap: between what I already know and what judging the coming work requires me to know. The tool is inbrief, and its contrast with a tool coming later is the one sentence worth keeping: inbrief closes the gap before the work; backbrief re-checks my model after the code has moved.

A session is a set of nodes, each one falsifiable claim: a question, an answer of at most thirty words, and a citation into code that exists. The agent proposes nodes and cannot grade them; marking one held is a click only I can make. What it chooses to teach is not a guess: it reads the model that laconic keeps of what I have already demonstrated, plain files under my home directory, and spends the session on the difference, because the budget here is my attention. The five nodes it chose:

What does this tool let a team prove? · Which part of this system carries a proof? · Why did one statement have to become two? · Why is the leaf count hashed in as well? · What does the tool refuse to decide for you?

Nothing about hashing, nothing about Merkle proofs, nothing about proof assistants: I had used all three in the prompt that started the project, so the session spent nothing re-teaching them. All five nodes are about this design and only this design.

I marked all five as held and closed the session. What those clicks bought has a shelf life: confidence in five sentences as the code stood at that moment. Twenty minutes later, a cycle rewrote the lines behind the fifth claim. Come back to the session, and it looks like this:

The claim reads as it did when I learned it, and I follow is still pressed. What changed is the orange line between them: the code behind the citation moved, and nothing matching it exists any more. Notice how little the tool asserts. It does not say I am wrong, because it cannot know that. It says nobody can vouch for the claim until someone looks at the new code. From inside my head, the two situations feel identical; in one of them my approval is a signature on a document I can no longer check.

What this station catches: the gap between what the engineer knows and what the work about to happen requires them to know.

Resolve the ambiguity: who decides, on the record

The vague demand becomes questions, and the answers become the decisions the specification will freeze; each is a decision that would otherwise be taken quietly by whoever writes the code. The tool is forebrief, which puts them to me as cards: one question, its options, and under each option its consequences, every consequence declaring its grounding, a citation into real lines or the tag conjecture. The agent cannot present a guess as established fact. One option is the default, and the log is append-only.

This is the card that mattered, transcribed from the round record:

What exactly does the Rocq module prove?

1. Verification accepts exactly the genuine redactions · DEFAULT · CONJECTURE Both directions matter: accepting too much lets a claim be forged, rejecting too much leaves an honest team unable to defend a true one.

2. A genuine redaction always verifies (soundness of the prover only)

3. Both directions, plus that a redaction never reveals a hidden word

Decided: option 1, default accepted.

Three candidate theorems, three different promises to whoever uses the tool. The consequence under option 1 is tagged conjecture because nothing cited it: I had reasoned it out and no code backed it yet. That tag is the tool refusing to let reasoning pass as fact. I took the default, and option 1 became the statement you will watch break two stations from here.

File one more detail away: option 2’s parenthetical, soundness of the prover only. Two stations from now that label turns out to be exactly backwards, and where it sits, on the day’s first card, transcribed by the agent and approved by me, will matter.

Not every card ends that way. Much later in the run, for reasons the last two stations will give, each finding acquired a secret of its own, a random value the team keeps and never publishes, and a card asked what happens when that secret is lost. The agent’s default was to print it once and make keeping it the team’s problem; I chose otherwise, and the tool now writes it into a file beside the finding. The log marks that an override: the record distinguishes decisions I made from defaults I let stand.

What this station catches: product intent decided silently by whoever writes the code.

Write the spec and the knowledge base: one memory, two audiences

Decisions become documents for two audiences: the knowledge base, which the agent reloads at the start of every cycle, and the specification, which a stranger must be able to build against. The knowledge base is documentation selected and sized to be reloaded every cycle, which is why it is six files and an index, one idea per file:

product.md            what this is for, and what it refuses to claim
architecture.md       where the boundary falls, and the trusted base
glossary.md           finding, leaf, root, disclosure, compatibility
format.md             the wire format, complete enough to reimplement from
plan.md               the cycles in risk order, and what each settles
decisions-round-1.md  round 1 verbatim, the cards that drew the boundary

The glossary defines eight words and defines them nowhere else. One entry is the most important sentence in this essay, and the proof it speaks of is the Merkle proof inside a disclosure:

compatibility · What a proof establishes: this redaction is a redaction of the text committed to by this root. Not that the text describes anyone’s finding, not that anything hidden is true.

Keep that one. The whole run turns on it.

The specification is format.md, and it exists because a guarantee only our own code can check is a guarantee nobody else can evaluate: the reporter holding a disclosure has neither OCaml nor this repository. So the file states how every hash is built. Here is that section as it stood that afternoon, H being SHA-256:

leaf(i, w)   = H( 0x00 ‖ uint32be(i) ‖ utf8(w) )
node(a, b)   = H( 0x01 ‖ a ‖ b )
count(n, r)  = H( 0x02 ‖ uint32be(n) ‖ r )

Read the first line: a leaf hashes the word together with its position, so the same word in two places gives two different leaves and nobody can quietly move one. A node hashes its two children in order. The third line looks like decoration and is not: the published root hashes the top of the tree together with the number of leaves, so two findings of different lengths cannot share a root. You will see where that line came from at the next station. The byte in front of each recipe stops one kind of hash from ever being read as another kind, which closes the attack where part of a tree is presented as a whole one.

verifier/verify.py is sixty lines of Python written later from that file alone, sharing no code with the tool, and it agrees with the tool on a real disclosure. One honesty note, which the file itself carries: I wrote both the format and the verifier, so their agreement shows the format is precise, not that it is independently reproducible. A stranger still owes us the real test.

What this station catches: nothing on its own. It is the written memory that every later catch is a comparison against.

Produce a change: the machine rejects what we meant

This is the box people picture when they hear the word agentic, and mechanically it is narrower than the picture: one written decision becomes one bounded change, under conditions fixed in advance, so that “the agent kept going until something passed” cannot happen. A cycle starts with a goal written down. The budget of attempts exists before the first attempt runs. The agent iterates against the harness inside it, and the cycle ends on a written judgement. The agentic-loop-kit enforces that shape: the budgets, the ratchet that forbids breaking a check that already passed, the rule for stopping. Here is one cycle as recorded, and its take, the recorder’s copy of it, is in the public record:

01KZ611JQ9VB5WBTWR9FXCAB22  shipped
goal: cycle 3e: bind the length into the root and close soundness with no
      axiom, budget four attempts
judgement: both theorems closed under the global context, no axioms, seventeen
      proofs; the obligation that resisted was removed by binding the leaf
      count into the root rather than by proving harder
  kb     d3bd2d9e6e087472…  /home/yann/work/dev/notary/kb
  goal   4ebebacc87320e50…  goal
  diff   9dbd2f79b7866f71…  diff

Goal before, judgement after, inputs pinned. And that goal line closes a promise from the previous station: this is the cycle the count recipe came from, the one that made two lengths unable to share a root.

Now the cycle that mattered most, as one worked instance of that shape. Its goal was to transcribe into Rocq the promise picked on the round-1 card: the checker says yes exactly when the redaction is genuine. Here is the transcription, and most letters are characters you have met: ws is the document’s words, d the redaction being handed over (the code’s disclosure record carries just its claimed length and revealed words; the Merkle proof p travels beside it as its own argument), r the published root. Two glosses for the rest: root_of ws = Some r says the root of ws exists and equals r, -> reads as “implies”, and <-> as “exactly when”. The code says verify where this essay says checker; same program, and the screens later say verifier too.

Definition verify_spec
  (verify : disclosure -> proof_data -> digest -> bool) : Prop :=
  forall ws d p r,
    root_of ws = Some r ->
    (verify d p r = true <-> projects d ws).

It type-checks, and read aloud it says what the card said. It is also fatally wrong, and you can find the flaw yourself, with no Rocq at all. Hunt for p on each side of the “exactly when”. The left side uses it: the checker reads the Merkle proof. The right side, projects d ws, never mentions it. So the verdict must be the same whatever p is handed in. Follow that one step further. For a genuine redaction the right side is true, so the checker must say yes to every p, a real Merkle proof or garbage. For a fake one it must say no to every p. The Merkle-proof channel is dead, and the checker is being asked to decide genuineness from thirty-two published bytes alone. No checker that actually distinguishes valid proof data from garbage can satisfy this property.

Neither I nor the agent saw that. I had approved the target on a card, the agent had transcribed it faithfully, and the flaw lived in what we meant. The machine found it the moment it was asked to argue for the property, and its finding is itself a four-line Rocq proof, p and p' being two arbitrary Merkle proofs:

Theorem spec_forces_ignoring_the_proof :
  forall verify, verify_spec verify ->
    forall ws d p p' r,
      root_of ws = Some r -> verify d p r = verify d p' r.

The repair split the promise in two, and here is what ships, both proven with no axioms. Read them with the same letters as before:

Definition verify_sound
  (verify : disclosure -> proof_data -> digest -> bool) : Prop :=
  forall ws d p r,
    root_of ws = Some r ->
    verify d p r = true ->
    projects d ws.

Definition prover_complete
  (build : disclosure -> list word -> proof_data)
  (verify : disclosure -> proof_data -> digest -> bool) : Prop :=
  forall ws d r,
    root_of ws = Some r ->
    projects d ws ->
    verify d (build d ws) r = true.

Soundness belongs to the checker alone: if it says yes, the redaction is genuine, which is the stranger’s protection from the bounty story. Completeness is the team’s: an honest redaction always passes. And look at the second statement’s signature. It quantifies over a new program, build, the thing that assembles the Merkle proof. The single biconditional had hidden that half of it was about a program the design had never named. That program, the prover, entered the design because a Rocq statement refused to stay quiet about it.

A test generated from the statement we believed could not have found this: there was nothing to run it against yet, and it would have encoded the same misunderstanding. The defect was in what we asked for.

The budget is not decoration either. One cycle of this day declared four attempts before the first ran, spent all four on a lemma that would not close, and ended with the goal unmet, outcome failed, kept in the record. The next cycle extended a three-attempt budget by one, with its reason logged: those attempts had died on Rocq’s proof-script language, not on the mathematics, which is a different kind of stuck.

What this station catches: defects in statements, in what we meant, which a test written from the same misunderstanding cannot see. An independent example, or a metamorphic test, sometimes can; a proof of coherence always does.

Run the harness checks: a failure names a place and an owner

Every change faces the same battery, and a failure is worth two things: it names a place, and it names an owner, because the code is not always the guilty party. Three failures that day went three ways. A test failed and the specification was at fault: the test had encoded my misunderstanding, so the obligation was restated and the code left alone (the diff of that cycle is in the record). The knowledge-base linter failed and the knowledge base was at fault: four properties named an enforcement channel that had moved, printed with their line numbers. A commit landed carrying two lint errors and the harness itself was at fault: no pre-commit hook, so the fix was the missing check.

The strongest check in the battery asks Rocq’s kernel, the small component every Rocq proof must ultimately pass through:

$ make assumptions
Closed under the global context
Closed under the global context

Two theorems, and for each the kernel answers: no axioms, nothing admitted. Be precise about what that is, because the run will shortly punish imprecision. The kernel answers for the logical assumptions of two stated theorems, and for nothing else. It cannot see SHA-256, the assumption that its outputs never collide, the translator that turned the proven core into OCaml, the six lines converting between Rocq’s numbers and OCaml’s, or the splitting of a text into words. Those live in a hand-kept list beside the kernel’s answer, the trusted base, and a hand-kept list can drift. Before the day ends, this run will prove that the hard way.

A fourth failure had no check behind it: a rule I had written into a project file myself and then broken three times in one day, once inside the very command that wrote it. It held nothing until it acquired an exit code. That is the small arrow looping from the checks back into the checks, labelled extend the checks: a rule that exists only in prose is a wish.

What this station catches: drift, when the code, the knowledge base and the rules stop agreeing. Cheap to catch, and caught constantly.

The engineer’s mental model: two true theorems, one broken promise

The dashed box at the centre, reached by the arrow labelled sync: the code has moved, and the human has to be brought back alongside it. This is where the run turned.

One confession before the screen. The previous essay prescribes this checkpoint after every cycle. This run did not follow its own prescription: the session below is the first one, eleven cycles in, and the screenshot admits it in its own words, this is our first brief together. The belief defect you are about to watch surface had exactly that long to grow.

The tool is backbrief. It builds a comprehension map over the repository, a graph whose nodes are questions, each cited to real lines, and walks it with me one claim at a time. Opening a region it has not covered, it starts with calibration: ask what I believe before showing me anything. Only I can advance a node. The map it built had twelve questions, indented here under what each depends on. Half of them use the project’s own jargon, which is what a real map looks like; two concern the chain, the separate program that publishes a root on a ledger, and this lap never visited it:

What does the proof actually cover?
├── Why two theorems rather than one biconditional?
│   ├── Which program did the biconditional hide?
│   └── Why does the root hash the leaf count?
│       ├── How was the last obligation discharged?
│       ├── What happened to the distinctness lemmas?
│       └── What does a reporter need to check a claim?
├── Who maintains the trusted base list?
├── What actually crosses into OCaml?
│   └── What is the exposure the boundary leaves?
└── Why is the chain a separate program?
    └── What makes trusting that program acceptable?

Everything hangs off the boundary question, the one I had decided on day one and never checked since. Two moves ran that evening before the session was interrupted by what it found. The second:

My calibration answer was right about order and length and crossed one direction: I attributed soundness to the prover, where it belongs to the verifier. That is precisely the distinction the two-theorem split existed to expose. And it was not a decay product. Go back to the first card: option 2’s parenthetical had labelled that direction soundness of the prover from the day’s first hour, transcribed by the agent, approved by me, corrected by neither, until a checkpoint made me say it aloud. So the agent probed: which one stops a forged disclosure? I answered with something else entirely, the non-reversibility of the hash: not an answer to the question, and a property no theorem, no test and no document in the project had ever claimed.

So the agent measured what a recipient could actually recover, and the construction the opening asked you to hold now comes due. This run had postponed the collapsing Merkle proof; to keep the Rocq proofs simple, a disclosure carried one hash per leaf, hidden words included, with a written note that the better construction “is a cycle of its own”. Every hidden word sat behind its own hash at a public position, and words come from a very small space:

hidden positions : 18
recovered by brute force from a 40-word dictionary: 16

· · · · · · · the Secure flag on the staging login · so it · · · · ·
a user reaches the site over plain ·

The attack is worth spelling out, because forty words sounds like nothing. A leaf hash is H(tag, position, word), and every ingredient except the word is public. So the attacker takes each hidden position, hashes a candidate word at it, and compares with the hash in the disclosure; a match identifies the word, under the same no-collision assumption the proof already leans on. Forty candidates were enough because the hidden words of a web-security finding come from a tiny vocabulary, articles and prepositions plus the dozen nouns of the trade. A larger dictionary widens the attack; I do not claim it recovers the last two, only that the space is small enough that it might. Sixteen of eighteen, in milliseconds. The redaction was formatting, not protection.

Both theorems were true the whole time, and they still are. This is the glossary entry doing its work: compatibility establishes that a redaction is a redaction of the committed text, not that anything hidden is true, or safe, or hidden at all. The project wrote that down on its first day, and I had marked the claim as held.

Two decisions made it possible, both on the record. The first you have just read: a Merkle-proof shape chosen because it made the Rocq proofs easier, dated by its own postponement note. The second: the trusted base, reviewed three times that day, listed five assumptions and not the one the product needed: that a hidden word cannot be recovered from its hash, which takes the preimage resistance of SHA-256 together with a secret salt that has enough entropy and stays secret.

The property the product depended on was nobody’s obligation.

Now go back to the card in the second station. Option 3 read both directions, plus that a redaction never reveals a hidden word. The property that failed sat on the first card of the first round, offered, declined and recorded. Declining it was legitimate, and I would decline it again: proving confidentiality is a different project with a different budget. What went wrong is that no other station inherited the obligation when the Rocq proof gave it back. The card decided what the proof would cover. Nothing decided what would cover the rest.

What this station catches: defects in what the humans believe, the class no checker can see, and the one that killed this product while every check was green.

What comes back: the repair lap

That evening, the dashed box at the centre of the ring stopped being a figure of speech. The model it names is the set of files introduced at the first station, and they gained one entry, the only one I will publish; the rest stays private:

id: merkle-redaction-disclosure
state: exposed                     (unknown -> exposed, 2026-08-04)
evidence:
  - 2026-08-04 [justification] Diagnosed unprompted that exposing every leaf
    hash made a redaction brute-forceable, and proposed redacting whole
    subtrees so a hidden region collapses to one node hash.

An hour earlier that concept had no entry at all; one observation moves a state by one step, which is why a correct unprompted diagnosis lands the concept at exposed rather than higher. The next round put the proposal in it onto a card, beside two others: give every leaf a salt, a random value derived per finding and mixed into each word’s hash, so that hashing “the” here and “the” there gives unrelated results; or build the collapsing subtree construction the opening described; or both, salt now, subtrees in a later cycle. I took the third.

The specification changed first. The three-line recipe from two stations ago gained a fourth line and a warning:

salt(i)      = H( 0x03 ‖ secret ‖ uint32be(i) )
leaf(i, w)   = H( 0x00 ‖ uint32be(i) ‖ salt(i) ‖ utf8(w) )

secret is thirty-two random bytes, one per finding, kept by whoever committed it and never published. The salts of revealed words travel inside the disclosure, so a reporter can still check everything; the salts of hidden words are what a recipient cannot compute. The same attack now recovers zero of eighteen. Zero is conditional, and the price should be said plainly: hiding lasts exactly as long as the secret stays secret and random. What the scheme still shows is the number of words, the position and length of every gap, and the subject line (leaf 0, the finding’s one-line title, revealed in every disclosure); a lost secret makes the root a commitment the team can never open again; and a chain anchor establishes inclusion in that chain’s history, not authorship. The tool prints what a recipient will see and scores none of it.

Then the change, the harness, and the commit, which is the boundary paying for itself in one screen:

$ git show --stat a392a3e
Salt every leaf, because the redaction was hiding nothing

 .backbrief/events/01KZ6CM7C6Z699MVZA0W58BCAF.jsonl |   8 +
 .backbrief/model/map.json                          |  40 +
 .forebrief/decisions.jsonl                         |   3 +
 .forebrief/rounds/01KZ6ZW268W8VQX36NEJAJCCH8.json  | 232 +
 kb/architecture.md                                 |  30 +
 kb/format.md                                       |  21 +-
 src/boundary.ml                                    |  31 +-
 src/notary.ml                                      | 213 +-
 verifier/verify.py                                 |  13 +-
 11 files changed, 509 insertions(+), 97 deletions(-)

theories/ is not among the eleven files. The proven core changed by zero lines, because it quantifies over an abstract type of word and a salted word is still a word. That is abstraction paying off, not confidentiality being proven: the Rocq proofs still say nothing about hiding, and now the architecture document says so in bold.

An earlier cycle had already shown what the next demand arrow means: it shipped no feature, tried to hand a disclosure to someone with neither the tool nor the repository, and found no written format, nothing to hand over, and a crash on the first command anyone types. format.md and the Python verifier exist because of that walk. Products meet strangers and come back with work.

The next demand is on a card already. The day after the run, a forebrief round opened the subtree lap: the disclosure becomes a Merkle multiproof, so a hidden run of any length collapses to one hash instead of one per word.

That lap has since landed, and it is in the repository you have been reading from: a proven multiproof core whose soundness and completeness the kernel closes with no axioms, and a verifier that folds the pruned tree in the same sixty lines. Reproving verify cost real work, because it sits inside the proven core. This is the loop’s last move on the page: a demand named on a card, taken round the ring, and checkable when you arrive.

What it cost, and what it does not establish

A demonstration is worth what its reader can check, so here is what would let you catch me staging it.

The recorder kept all twelve cycles and all twelve are public, each with the goal written before the work, the diff, and the judgement written after, in record/. One is failed and kept. None was re-run, so nothing here is a second take of something that went badly.

I also wrote down what this essay would show before the first cycle ran. That list is now in the repository with its provenance stated: the original commit lives in a private repository, so its date is my claim, not an independently checkable fact. And it answers only the weak objection, that the run was assembled afterwards to fit a story. The strong one stands: I chose the project and the slice. One engineer, one small tool, no control group, nothing here about a team.

The lesson is not that machine-checked proofs are strong, though they are, nor that people catch what machines miss, though they do, and more often when they are kept beside the work rather than on its critical path. It is the gap this series started from. No formal checker can derive what you meant from the specification you wrote; evidence of alignment is human and empirical, and it expires. The Rocq proof attacked the gap from one side and found a promise nothing could satisfy. The checkpoint attacked it from the other and found a property nobody had written down. Different classes, different stations. Remove the proof attempt and you keep a specification nobody knows is incoherent. Remove the checkpoint and you keep two true theorems about a product that does not work.

That is the series closing on itself. The first essay named the meaning-to-specification gap; the third insisted that no checker settles whether a criterion matches the need; the fourth made the engineer’s understanding an objective the process pursues rather than a property it can prove. This run is one instance of all three at once: a machine that ruled its own side of the gap and a human who was needed for the other, on the same afternoon, over the same tool.

The repository is there. make checks the proofs, make assumptions asks the kernel what they rest on, and verifier/verify.py checks a disclosure in sixty lines of Python that share no code with the tool. The first two need Rocq and OCaml, and the README names the toolchain; the third runs on stock Python 3.

Appendix