Eighty Verified Witnesses, Six Proofs

If you want to know what a language model contributed to a result, three accounts are on offer. The model’s own should carry no weight; that is the premise of putting it behind a boundary. The harness’s is only as good as the harness, and it certainly isn’t exhaustive. Your own reading, chosen after the results are in, is, unfortunately, worth less than it feels in many scenarios^aa This is especially true as autonomy in the use of language models is not only increasing, but actively being pushed by essentially all of the frontier labs. For instance, Anthropic switching Claude Code’s default to auto mode, the new “Dots” autonomous agent product of OpenAI, Meta’s Muse, etc. These developments also apply to open source agents like pi, where the default workflows are to allow all actions without much manual intervention..

Proof Broker accepts nothing it cannot check. For R6, I put a live language model behind that boundary and asked it for arithmetic proof certificates on a census of 15 obligations from a real Lean development, the 11 its interface could pose, 8 times each. The analysis and the auditor were frozen before the cohort’s first call, and every request was reserved on a ledger against a signed authorization before it was sent. The questions were simple: how often does one learned proposal become an admissible proof, what does repetition actually buy, and where does the deterministic route already provide that proof?

Every certificate the model was asked for that could exist came back and verified: 80 of 80. Proof coverage, nonetheless, stayed at six of fifteen obligations, equal in the 8th and final draw to the 1st. In contrast to what one might have intuitively expected, the bottleneck was never the model.

Everything reported here can be checked from public records, and one qualification belongs at the top rather than the bottom. I would encourage an interested reader to glance through. In production, I met two situations no rehearsal had covered: a shared policy directory, and a network connection that failed before anything was sent. In both instances, the frozen machinery stopped rather than guess. Each fix changed only what the auditor, and once the runner, would accept, and neither touched the analysis, a recorded outcome, or a run. Two amendments describes what happened in more detail.

The experiment on one page

The boundary has three gates, and the model sits outside all of them. The model proposes a Farkas witness: one integer multiplier per hypothesis, nonnegative on every inequality, chosen so that the weighted sum of the hypotheses and the negated goal cancels every variable and leaves a false statement about constants (such as 1 \le 0). An independent checker verifies the witness. A closer, the step that builds a proof term from the certificate, consumes it. Then the kernel, the small trusted checker at Lean’s core, checks the local proof and the whole declaration that contains it, and the axioms that declaration uses must be unchanged. The architecture essay tells the full boundary story. A concise version to summarize here: nothing the model says is believed until all three gates have passed it.

The workload was fixed before the model saw any of it. The census takes every omega call in VerInf’s Bracket.lean at one pinned commit, the same file R4 used: 15 primary obligations in 4 declarations. The declaration, or family, is the unit of independence, since 4 sites in one proof are not 4 separate pieces of evidence. The frozen SDK refuses the goal form of 4 obligations before any request, which leaves 11 posed. 10 of those are certificate-feasible. The 11th, l170, is a negative control: its rows are satisfiable, so no valid certificate exists, and an acceptance there would mean the checker had failed, not that the model had succeeded.

The model got only one request per slot, nothing else. It was gpt-5.4-2026-03-05, through OpenAI’s Responses API at medium reasoning effort, with no tools, one stateless request, at most 4,096 output tokens and no automatic retries.^bb The name is the provider’s label. The frozen policy records it as “a documented dated provider snapshot; not a model-content hash or an attestation that the returned text came from it.” Nothing in this experiment depends on the attribution, since the boundary treats any proposer’s output the same way. Any claim about which model did this rests on that label and nothing more. The prompt’s rules close with: “The witness is checked independently; do not claim acceptance yourself. Supply a proposal even if uncertain.” Each posed obligation received eight preassigned draws with byte-identical input: 88 slots. The draws are repeated attempts on the same eleven questions, not 88 independent trials.

Everything that could be decided in advance was. The analysis program was locked on 23 September, before the cohort’s first call.^cc Earlier stages of R6 made live calls while building the harness, and two of them showed the provider one of these fifteen obligations. Counting what counts reports what that means for it. The auditor that decides whether a collection is admissible at all was locked before the first block was signed. The deterministic comparison arm was frozen and run before any learned draw. Collection ran in two blocks, each under its own signed authorization: draw 1 on all eleven posed obligations, then draws 2 through 8.

What happened

• Verified witnesses: all 80 certificate-feasible slots.
• Proofs: 48 of 88 slots ended in a whole-declaration-validated proof with the axioms unchanged. They are six obligations proved at every draw: l069, l070, l071 and l078 in lift_cell, through the ℕ closer, and l096 and l099 in threshold_unique, through the ℤ closer.
• Coverage: six of fifteen obligations at draw 1, and six of fifteen at draw 8. Each draw added exactly six proofs, on the same six obligations.
• Refused: l166, l175, l178 and l204 received verified witnesses at all eight draws, and the closer refused all 32.
• The negative control held: the verifier rejected l170 at all eight draws. No false certificate was accepted, and no observation contradicted another.

Against the deterministic arm, the gain is two obligations in one family. The frozen deterministic route, cvc4 1.8 with the SDK’s own Farkas synthesis, proved the same four lift_cell obligations. On l096 and l099 it never invoked its backend, and no certificate was minted. The model closed both, at every draw. On the other posed obligations the arms agree: both prove the lift_cell four, and on l166, l175, l178 and l204 both produce certificates that verify and then fail at reconstruction.

Counting what counts

Obligations are what a proof is about; families are what is independent; draws are repetitions. “48 of 88” reads like a 55% success rate, but it’s really 6 obligations in 2 families, each proved 8 times. So the obligations go beside the slots every time a number appears, and Figure 2 follows both units from start to finish.

Nothing in either ladder was lost to a missing or invalid proposal on a feasible obligation. The losses are the four goals the SDK would not pose, the negative control doing its job, and the 4 goals the closer refused.

Repetition bought diversity, not coverage. Compared up to positive scaling, l070 returned 4 distinct verified witnesses over its 8 draws, and only 3 of those slots matched the certificate the classification had found. l071 returned two, neither matching. Every other verified site returned the same witness at every draw, equal to the classification’s. The extra witnesses all landed on obligations that were already proved, so they bought no new proof.

One obligation may have been seen before. l070 is the control site of R6-000, the project’s first golden episode. Its obligation, rows and deterministic witness were visible to the provider in 2 earlier live calls. The analysis keeps it as a stratum rather than removing it. Without l070, 40 of 80 slots validate; without its whole family, 16 of 56. The gain over the deterministic arm does not depend on it: that gain is l096 and l099, and no site but l070 had been extracted or transmitted before the census.

Where it stopped

The four refused obligations had verified certificates every time. What failed was the step from certificate to proof. The pinned closer picks its mode from the extraction. These four contain natural-number variables, so it selects the ℕ closer, whose goal matcher accepts only comparisons at Nat. The goals themselves are integer comparisons over casts, such as ↑v0 ≤ z. The closer refused before the kernel was asked anything, and the refusal was diagnosed as nat_closer_int_goal from bound evidence alone. These are the four sites the design had predeclared closer-unreachable from its rehearsals. The live model’s certificates did not move them.

A route that re-proves the goal cannot answer the question. The broker’s default route closes through gated_omega. Once a certificate is accepted, it runs omega again on the original goal. As a separate reference, it closed l069 through l078 and exactly the four refused sites, and missed l096 and l099. That shows the four refused obligations are provable, which nobody doubted: omega proves them in the original file. It does not show that a retained witness can be consumed, because on that route the certificate is only a gate. So it is tabled beside the frozen arm as a control and never pooled with it. No route closed all ten feasible obligations.

R6 leaves one sharp question. The 32 verified certificates at l166, l175, l178 and l204 are retained. Can a closer suited to their ℤ goals build proofs from them? R6-015, proposed and not yet run, would test that offline, preregistered separately, with no provider, no credential and no spending. It would not revise R6’s result, which stands as recorded under its frozen route.

What an outside reader can check

A claim like this is only as good as whatever bounds each way it could be wrong. The table is the argument. Each row names a failure, the mechanism that bounds it, and where to look.

The analysis is an empirically replicable experiment rather than a judgment. Anyone with the repository at the r6 tag can rerun it on the recorded input and compare the bytes:

cd experiments/r6
python3 analysis_r6.py \
  --input reviews/2026-09-29/R6-014-BLOCK2-ANALYSIS-INPUT.json \
  --policy policies/farkas-cohort-v9.json \
  --output /tmp/r6.json
cmp /tmp/r6.json \
  reviews/2026-09-29/R6-014-BLOCK2-ANALYSIS.json

The money reconciles to the micro-dollar. The final authorization covered all 88 slots at 9,011,200 µUSD, about $9.01. The ledger holds 89 reservation rows totalling 9,113,600 µUSD gross; one pre-send release returned 102,400, so the net committed is exactly the authorization, and nothing is open. The provider reported 108,480 input and 44,886 output tokens, which at the frozen rates prices at 944,490 µUSD, about $0.94.

The disclosure scans cover what was published. Their scope is the experiment’s directory, not the whole repository. The published records deliberately keep host metadata such as local paths, and never a credential value.

Some stops were the machinery working. The first launch of block 2 was interrupted by an interrupt signal before it reserved anything. The runner found the sealed attempt on relaunch and paused, and the attempt was moved aside byte for byte, 175 files with identical digests. Three stops never fired: the integrity stop for a negative-control acceptance, any unknown or partial send, and any slot exhausting its attempts.

Two amendments

Production met two things no rehearsal had. The first surfaced on 24 September. The first frozen audit of block 1 rejected the collection at a layout check, before examining a single run. The check required the policy directory to hold only the campaign’s own files. Every reviewed fixture had a directory to itself, but production signs into a shared one, beside every earlier policy and lock. Amendment 1 derived the campaign’s expected files explicitly and ignored unrelated ones; every other predicate stayed the frozen auditor’s. It was reviewed and locked as live-evaluation-v2, and block 1 was accepted with 550 cases. The rejection is retained beside it.

The second surfaced at 23:34 UTC on 28 September, at l204’s sixth draw, with 64 slots collected. The sender made one connection attempt, and it failed after 15.7 seconds with nothing sent.^dd The host’s network probe dropped at about the same moment. That is circumstantial, and I claim no cause. The ledger already had a reviewed rule for this: a release with termination established and zero sends leaves the slot unconsumed and retriable, up to three attempts. But neither the live auditor nor the runner had ever met one, so the runner paused, as its rule required. Amendment 2 taught the auditor to admit a live pre-send release only on the sender’s complete pre-grant state, not on the ledger’s word. It let the runner retry within the ledger’s limit, after a preflight over every existing run. Its first review found two real defects before anything resumed: contradictory send evidence could still authorize a retry, and a restart could skip existing attempts. Both were repaired and reviewed again. With the lock at live-evaluation-v3, run 3 retried the slot and collected the remaining 23 in eighteen minutes.

What changed, and what did not. Both amendments changed only what the auditor, and for the second the runner, would accept. Neither changed the frozen analysis, a recorded outcome, or a run. Both were built and tested on synthetic evidence first, without reading the collected outcomes to decide what to accept. R6 is therefore not an unchanged preregistered evaluation; what it can claim is that every change is dated, reasoned, reviewed and kept next to what it replaced.

The lesson is cheap to apply. Neither gap was a defect in the evidence. Both were gaps between what was rehearsed and what production does. Some might say this is the reason we tend to distinguish between development and production!

Current Limitations

The evidence is narrow, and the result is interesting because it is bounded.

• One file. Fifteen obligations from one file at one commit, in four families. They support no claim about a repository population, and that is a scale-out that I look forward to building.
• One model, one interface. One snapshot, through one prompt contract, with one stateless request per slot and no tools. The snapshot’s identity is the provider’s label rather than an attestation.
• One exposed site. l070 had been visible to the provider before; the sensitivities above bound its effect.
• Money. The cost is an estimate from provider-reported usage, not a bill.
• Scans. They cover the experiment’s published records, not the whole repository.
• Amendments. The evaluation was amended twice after collection, as described.

Proposal is not the hard part

The case for putting search behind a boundary never rested on the searcher being trustworthy. R6 shows something narrower: on real goals, a model that is trusted with nothing can still be measured, and on these goals it returned a valid certificate every time it was asked for one that could exist. What decided coverage was the machinery on either side of it: which goals could be posed, and which certificates a closer could turn into proofs. That is where the next work is.

The other half of the problem is the one VerInf works on. The policy for this experiment records, correctly, that nothing attests which model produced these witnesses. For Proof Broker nothing needs to, because every witness was checked on its own terms. A claim about the model itself would need exactly that attestation. Both projects are the same discipline pointed at different claims: check the claim without trusting its author, and say plainly what you changed along the way.