PRIME：迈向 LLM 智能体中可验证的证据支撑推理

# PRIME: Towards Verifiable Evidence-Grounded Reasoning in LLM Agents
Source: [https://arxiv.org/html/2610.22426](https://arxiv.org/html/2610.22426)
Xiaoming HuoAffiliation:H\. Milton Stewart School of Industrial and Systems EngineeringAffiliation:Georgia Institute of TechnologyEmail:[hkhosravi7@gatech\.edu](mailto:)huo@gatech\.edu

###### Abstract

LLM agents are used to check records against an organization’s requirements, for example whether a vulnerability report is ready for investigation\. Requirements often allow several ways to be met, such as a severity rating with a curator\-reviewed advisory or a published advisory link\. Agents fail by accepting a report after a required check has failed, or by settling for a weaker conclusion without trying another way that could still succeed\. We introduce PRIME \(Precommitted Rules for Inference from Minimal Evidence\)\. Before checking, it fixes evidence routes specifying how each conclusion may be justified\. A separate program records each check result and refuses any conclusion the results do not justify\. It also points the agent to checks that could justify a stronger conclusion, or runs them itself\. PRIME reports only conclusions authorized by its rules and ledger\. With correct requirements, exact checks at known locations, and sufficient budget at stopping, completion reaches the strongest supported conclusion\. On 480 public\-record tasks, an agent shown the requirements reported unjustified conclusions on 26\.7% of tasks, while PRIME reported none\. Its directions and added checks raised the average score for justified conclusions from 30\.1, with refusal alone, to the maximum of 59\.2 out of 100\.

## 1Introduction

Large language model \(LLM\) agents increasingly assist security triage\([Saju and Azim, 2026](https://arxiv.org/html/2610.22426#bib.bib26);[Liu and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib15)\), and similar agents can check records against an organization’s requirements, for example whether a software vulnerability report has enough information for analysts to investigate\. The outcome is rarely a simple yes or no\. A review can reach conclusions of increasing strength, from “the report has a description” to “the report is ready for investigation”, and requirements often accept more than one combination of checks\. Suppose a company accepts a report for investigation if it has a description and either \(a\) a severity rating together with an advisory reviewed by a curator, or \(b\) a link to a published security advisory\. An agent finds that the curator review is missing\. It can then fail in two ways\. It may accept the report anyway, an*unsupported conclusion*that its checks do not justify\. Or it may settle for a weaker conclusion without checking the link, a*missed conclusion*, although option \(b\) could still succeed\. Showing an agent its requirements and previous check results does not enforce what it may report\.

Existing methods address one failure or the other\. Self\-verification rechecks answers\([Dhuliawala et al\., 2024](https://arxiv.org/html/2610.22426#bib.bib7)\), citation methods link claims to sources\([Gao et al\., 2023](https://arxiv.org/html/2610.22426#bib.bib9)\), and conformal methods calibrate factuality risk\([Mohri and Hashimoto, 2024](https://arxiv.org/html/2610.22426#bib.bib17)\)\. None of them requires a reported conclusion to rest on checks that were actually run\. Rule\-enforcement approaches block agent actions that break fixed rules\([Wang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib35);[Doshi et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib8)\), and evidence\-gated systems refuse a claim until evidence for it has been recorded\([Xia and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib37);[Huang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib11)\)\. They do not jointly use fixed alternative routes to authorize graded conclusions and guide checking\. Evidence\-gathering methods select checks\([Zhang et al\., 2026b](https://arxiv.org/html/2610.22426#bib.bib42);[Liu and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib15)\), but do not combine both functions through fixed routes\.

We introduce PRIME \(Precommitted Rules for Inference from Minimal Evidence\), which handles both failures with one set of requirements\. Before review, PRIME fixes the combinations of checks its program treats as sufficient for each conclusion\. We call each such combination an*evidence route*\. A component separate from the agent, the*runtime*, then records every check result and refuses to report any conclusion that lacks a fully checked route\. It also tells the agent which unchecked items could still complete a route to the strongest conclusion within the remaining tool calls, and if the agent stops early, the runtime can run those checks itself\. In the example, PRIME refuses to accept the report after the failed curator check and directs the agent to check the advisory link\.

Our contributions follow the structure of the paper\.

- •Formulation\.We state the review as choosing checks under a limit on tool calls, with the strict rule that every reported conclusion must be justified by checks actually run \(Section[2](https://arxiv.org/html/2610.22426#S2)\)\.
- •Method\.PRIME uses the same evidence routes to decide what may be reported and which checks to run next \(Section[3](https://arxiv.org/html/2610.22426#S3)\)\.
- •Guarantees\.No agent behavior can make PRIME show the user an unjustified conclusion, and its remaining errors come only from wrong requirements or wrong check results\. With correct rules, exact checks at known locations, and sufficient budget at stopping, completion reaches the strongest supported conclusion \(Section[4](https://arxiv.org/html/2610.22426#S4)\)\.
- •Positioning\.We compare PRIME with verification, enforcement, and evidence\-gathering systems and state its costs \(Section[5](https://arxiv.org/html/2610.22426#S5)\)\.
- •Benchmark and evaluation\.SUFFICE has 938 tasks built from public security, clinical\-trial, drug\-recall, and financial records, scored by code rather than by an LLM \(Section[6](https://arxiv.org/html/2610.22426#S6)\)\. On 480 held\-out tasks and four models, PRIME reported no unsupported conclusions\. For Qwen2\.5\-32B with refusal alone, the average score for supported conclusions was 30\.1 out of 100\. PRIME’s directions raised it to 45\.5, and running the remaining checks raised it to 59\.2, the maximum possible on these tasks\. Programs generated by an LLM from a clinical\-trial regulation also ran unchanged on real registry records \(Section[7](https://arxiv.org/html/2610.22426#S7)\)\.

## 2Problem Formulation

#### Review task\.

A review casex=\(Sx,Vx\)x=\(S\_\{x\},V\_\{x\}\)has a*specification*SxS\_\{x\}naming conclusions and available checks, and an initially unchecked*evidence view*VxV\_\{x\}containing the report’s values\.

- •*Conclusions*C=\{c1≺⋯≺cK\}C=\\\{c\_\{1\}\\prec\\dots\\prec c\_\{K\}\\\}, ordered by strength, with utilities0=U⁡\(⊥\)<U⁡\(c1\)<⋯<U⁡\(cK\)0=U\(\\bot\)<U\(c\_\{1\}\)<\\dots<U\(c\_\{K\}\), where⊥\\botis abstention\.
- •*Evidence atoms*E=\{e1,…,em\}E=\\\{e\_\{1\},\\dots,e\_\{m\}\\\}, yes\-or\-no conditions such as “a severity rating exists”, with hidden valuesωx∈\{0,1\}m\\omega\_\{x\}\\in\\\{0,1\\\}^\{m\}\.
- •*Checks*: field and text reads and*attestations*, in which a model or person records a judgment as evidence, settle one or more atoms, and each atom’s*resolver*is the registered procedure that checks it\. Uncached checks and emissions cost one call from a budgetBB; cached repeats andstopare free \(Appendix[A](https://arxiv.org/html/2610.22426#A1)\)\.

#### Requirements\.

A*review program*PPgives each conclusioncca set of evidence routesP⁡\(c\)P\(c\)\. A routeppis a conjunction of literalseeor¬e\\neg e, and completing any one route justifiescc\. In the example, acceptance has the routesp1=\{description,severity,curator review\}p\_\{1\}=\\\{\\text\{description\},\\text\{severity\},\\text\{curator review\}\\\}andp2=\{description,advisory reference,URL\}p\_\{2\}=\\\{\\text\{description\},\\text\{advisory reference\},\\text\{URL\}\\\}\. The*intended standard*fx⋆​\(c,ω\)∈\{0,1\}f^\{\\star\}\_\{x\}\(c,\\omega\)\\in\\\{0,1\\\}says whether a complete assignmentω\\omegajustifiescc\. The program is*correct*when, for everyω\\omegaandcc,fx⋆​\(c,ω\)=1f^\{\\star\}\_\{x\}\(c,\\omega\)=1exactly when some route ofccor of a stronger conclusion holds underω\\omega\.

#### Evidence and authorization\.

The*ledger*z∈\{𝖴,𝖳,𝖥\}mz\\in\\\{\\mathsf\{U\},\\mathsf\{T\},\\mathsf\{F\}\\\}^\{m\}records each atom as unknown, established true, or established false\. A routeppholds atzz, writtenz⊧pz\\models p, if every literal ofppis established\. A conclusion is*authorized*if a route to it or to a stronger conclusion holds:

AuthP\(z\)=\{c∣∃d⪰c,p∈P\(d\):z⊧p\}\.\\mathrm\{Auth\}\_\{P\}\(z\)=\\\{c\\mid\\exists d\\succeq c,\\ p\\in P\(d\):\\ z\\models p\\\}\.\(1\)Authorization compares recorded evidence with the program, not with the world: it does not test whether the program or the observations are correct\.

#### Decision problem\.

The agent issues one request per step: run a check \(which updates the ledger\), report a conclusion withemit​\(c\)\\textsc\{emit\}\(c\), orstop\. LetP0P\_\{0\}be the program fixed before the first check,π\\pithe agent’s policy,c^\\hat\{c\}the reported conclusion, andzτz\_\{\\tau\}the final ledger\. The goal is

maxπ\\displaystyle\\max\_\{\\pi\}𝔼π​\[U⁡\(c^\)​fx⋆​\(c^,ωx\)\]\\displaystyle\\mathbb\{E\}\_\{\\pi\}\\big\[U\(\\hat\{c\}\)\\,f^\{\\star\}\_\{x\}\(\\hat\{c\},\\omega\_\{x\}\)\\big\]\(2\)s\.t\.\\displaystyle\\mathrm\{s\.t\.\}c^∈AuthP0​\(zτ\)∪\{⊥\}​for every episode,\\displaystyle\\hat\{c\}\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\_\{\\tau\}\)\\cup\\\{\\bot\\\}\\ \\text\{for every episode\},total cost≤B\.\\displaystyle\\textstyle\\displaystyle\\text\{total cost\}\\leq B\.The constraint makes a report*verifiable*: anyone holdingP0P\_\{0\}and the ledger can check it without trusting the agent\. It must hold in every episode, not on average\. The objective rewards the strongest conclusion that is also true\. An unsupported conclusion violates the constraint, and a missed conclusion loses utility\. Appendix[A](https://arxiv.org/html/2610.22426#A1)adds logical constraintsΦx\\Phi\_\{x\}between atoms, conflicting observations, and partially ordered conclusions, and Appendix[C](https://arxiv.org/html/2610.22426#A3)gives the exact charging rule\.

## 3PRIME

PRIME solves Problem \([2](https://arxiv.org/html/2610.22426#S2.E2)\) in two parts: it enforces the constraint exactly and pursues the objective heuristically\. Both use the committed routes \(Figure[1](https://arxiv.org/html/2610.22426#S3.F1)\)\.

\(A\) PRIME Overview\!SecurityReport\(to be reviewed\)LLM Agentproposes the nextcheck or conclusionTools for ChecksRead fieldRead textLook uprecordPRIME Runtime∙\\bulletFixed review program \(requirements\)∙\\bulletEvidence ledger \(records check results\)∙\\bulletGuidance \(useful remaining checks\)∙\\bulletAuthorization \(allowed conclusions\)proposedactionfeedback andguidancerunschecksresultsAuthorized Answersupported by collected evidenceNotationccCandidateconclusionppEvidence route\(required checkoutcomes\)Check passedCheck failedNot yet checkedRoute blockedRoute still possibleNext checkrecommended\(B\) Worked Example:Reviewing a Security ReportTarget conclusioncc:The report meets therequirements for further review\.Routep1p\_\{1\}\(blocked\)Vulnerability descriptionexists in the reportSeverity rating existsAdvisory reviewedby a curatorRoutep1p\_\{1\}blocked\(required check failed\)Routep2p\_\{2\}\(still possible\)Vulnerability descriptionexists in the reportReference is a publishedadvisoryReference has a URLRoutep2p\_\{2\}can still be used\(not yet checked\)Current state∙\\bulletp1p\_\{1\}blocked \(curator\-review checkfailed\)∙\\bulletp2p\_\{2\}possible butincompletePRIME guidanceCheck thesupportingreference next\(from routep2p\_\{2\}\)Authorized conclusionNot yet allowedto concludecc\(not yet checked\)Figure 1:PRIME in a hypothetical security\-report review\. \(A\) The independent runtime records check outcomes, uses precommitted evidence routes to guide the agent, and authorizes conclusions\. \(B\) Acceptance requires a description plus either a severity rating and curator\-reviewed advisory \(p1p\_\{1\}\) or a published advisory reference with a URL \(p2p\_\{2\}\)\. A failed curator\-review check blocksp1p\_\{1\}, while the reference checks ofp2p\_\{2\}remain open\. PRIME recommends checking the reference but cannot yet authorize acceptance\.#### 1\. Commit\.

A commitment procedureGGproducesP0=G⁡\(Sx,r\)P\_\{0\}=G\(S\_\{x\},r\)from the specification and randomnessrralone, never from field values\. The program may be supplied by a person or generated by a model\. The runtime validates its structure, records its hash, and only then enables checks, so a failed check cannot lead to rewriting the requirements \(Appendix[A](https://arxiv.org/html/2610.22426#A1)\)\.

#### 2\. Gate\.

The runtime refusesemit​\(c\)\\textsc\{emit\}\(c\)unlessc∈AuthP0​\(z\)c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)at the current ledger\. If checking ends without an accepted request, it reports the strongest authorized conclusion, or abstains if none is authorized\. A renderer with fixed templates produces the answer, listing the conclusion with its supporting checks rather than free model prose\.

#### 3\. Guide\.

Blocking unsupported reports can make the agent stop too early, so PRIME also uses the routes to direct further checking\. The*residual*of routeppatzzis the set of its literals not yet established,

R⁡\(p,z\)=\{ℓ∈p∣z⊧̸ℓ\}\.R\(p,z\)=\\\{\\ell\\in p\\mid z\\not\\models\\ell\\\}\.\(3\)A route is*live*if none of its literals is established false or certified unavailable\. Letκ^​\(p,z\)\\hat\{\\kappa\}\(p,z\)be the number of distinct checks needed to settleR⁡\(p,z\)R\(p,z\)\. With remaining budgetbb, PRIME targets the strongest conclusion that has a live route within budget, and that conclusion’s cheapest live route:

ℛ⁡\(z,b\)\\displaystyle\\mathcal\{R\}\(z,b\)=\{c∣∃p∈P0\(c\)live,κ^\(p,z\)≤b\},\\displaystyle=\\\{c\\mid\\exists p\\in P\_\{0\}\(c\)\\text\{ live\},\\ \\hat\{\\kappa\}\(p,z\)\\leq b\\\},\(4\)c⋆\\displaystyle c^\{\\star\}∈arg⁡maxc∈ℛ⁡\(z,b\)⁡U⁡\(c\),\\displaystyle\\in\\arg\\max\_\{c\\in\\mathcal\{R\}\(z,b\)\}U\(c\),p⋆\\displaystyle p^\{\\star\}∈arg⁡minp∈P0​\(c⋆\)​live​κ^​\(p,z\)\.\\displaystyle\\in\\arg\\min\_\{p\\in P\_\{0\}\(c^\{\\star\}\)\\text\{ live\}\}\\hat\{\\kappa\}\(p,z\)\.Ifℛ⁡\(z,b\)\\mathcal\{R\}\(z,b\)is empty,c⋆=⊥c^\{\\star\}=\\bot\. The agent seesc⋆c^\{\\star\},R⁡\(p⋆,z\)R\(p^\{\\star\},z\), andAuthP0​\(z\)\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\), and still chooses its own next check\. Whilec⋆c^\{\\star\}is stronger than every authorized conclusion, the runtime holds requests to report a weaker one and answers up to threestoprequests with reminders\.

#### Completion\.

With completion enabled, when the agent finally stops, the runtime runs the open checks ofp⋆p^\{\\star\}itself and recomputes the target after each result, until the target is authorized, no stronger conclusion is reachable, or the budget is spent\. It uses only registered resolvers\. It cannot invent evidence or make judgments that require a model or a person\. Algorithm[1](https://arxiv.org/html/2610.22426#alg1)in Appendix[B](https://arxiv.org/html/2610.22426#A2)gives the full procedure\.

## 4Guarantees and Why They Matter

We assume a trusted runtime that faithfully records resolver outputs and identified attestations, and a renderer that is*sound*: its text expresses only conclusions marked as authorized\. Appendix[A](https://arxiv.org/html/2610.22426#A1)states these premises \(T1–T4\), and Appendix[B](https://arxiv.org/html/2610.22426#A2)gives all proofs\.

###### Theorem 4\.1\(Authorization holds for every agent\)\.

\(i\) For fixed randomness, two cases with the same specification receive the same committed program, whatever their evidence\. \(ii\) For every policy, sequence of actions and resolver results, budget, and stopping point, every conclusion PRIME outputs at final ledgerzzlies inAuthP0​\(z\)\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\. \(iii\) If the renderer is sound, every conclusion the user sees also lies inAuthP0​\(z\)\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\.

*Why it matters\.*The constraint of \([2](https://arxiv.org/html/2610.22426#S2.E2)\) holds whatever the model, prompt, or agent behavior, so it does not depend on the agent following instructions\. An auditor can check any answer against the committed program and the ledger without rerunning the agent\. Part \(i\) rules out tailoring the requirements to the evidence\.

Authorization is not truth\. Call a ledger*truthful*when every atom it settles agrees withωx\\omega\_\{x\}\. LetEprogE\_\{\\mathrm\{prog\}\}be the event that the program authorizes, at some truthful ledger, a conclusion withfx⋆=0f^\{\\star\}\_\{x\}=0, andEresE\_\{\\mathrm\{res\}\}the event that the runtime admits an incorrect atom value, from a resolver or an attester\. LetEmaskE\_\{\\mathrm\{mask\}\}andErenderE\_\{\\mathrm\{render\}\}be the failures of parts \(ii\) and \(iii\), andEuserE\_\{\\mathrm\{user\}\}the event that the user sees a conclusion withfx⋆=0f^\{\\star\}\_\{x\}=0\.

###### Theorem 4\.2\(Where end\-to\-end error comes from\)\.

Under T3 and T4, for any distribution of episodes,

Pr⁡\(Euser\)≤\\displaystyle\\Pr\(E\_\{\\mathrm\{user\}\}\)\\leqPr⁡\(Eprog\)\+Pr⁡\(Eres\)\\displaystyle\\Pr\(E\_\{\\mathrm\{prog\}\}\)\+\\Pr\(E\_\{\\mathrm\{res\}\}\)\(5\)\+Pr⁡\(Emask\)\+Pr⁡\(Erender\),\\displaystyle\+\\Pr\(E\_\{\\mathrm\{mask\}\}\)\+\\Pr\(E\_\{\\mathrm\{render\}\}\),and by Theorem[4\.1](https://arxiv.org/html/2610.22426#S4.Thmtheorem1)the last two terms are zero\.

*Why it matters\.*Any remaining error comes from two components that can be tested separately: the rules, which can be checked against the intended standard, and the observations, which can be verified\. Effort can therefore go where error actually arises\. When every atom is settled by an exact deterministic resolver,Pr⁡\(Eres\)=0\\Pr\(E\_\{\\mathrm\{res\}\}\)=0\. Wrong admitted judgments still enterEresE\_\{\\mathrm\{res\}\}\.

The first two results concern safety\. The third concerns utility: it says when the gate costs nothing\. Letc†c^\{\\dagger\}be the strongest conclusion withfx⋆​\(c†,ωx\)=1f^\{\\star\}\_\{x\}\(c^\{\\dagger\},\\omega\_\{x\}\)=1, or⊥\\botif there is none\. LetE†E^\{\\dagger\}be the atoms on the routes ofc†c^\{\\dagger\}and of every stronger conclusion, or of all conclusions ifc†=⊥c^\{\\dagger\}=\\bot\. LetN⁡\(z\)N\(z\)be the number of distinct checks needed to settle the atoms ofE†E^\{\\dagger\}that are unknown atzz, andz0z\_\{0\}the initial ledger\.

###### Theorem 4\.3\(Completion reaches the strongest supported conclusion\)\.

Suppose the conclusions form a chain,P0P\_\{0\}is correct,Φx\\Phi\_\{x\}is empty, no atom ofE†E^\{\\dagger\}has withheld evidence, every check returns the true values of the atoms it settles and reads a known field, and completion is enabled\. If the agent’s checking ends without an accepted report at a ledgerzzwith remaining budgetb≥N⁡\(z\)b\\geq N\(z\), PRIME reportsc†c^\{\\dagger\}\. In particular, ifB≥N⁡\(z0\)B\\geq N\(z\_\{0\}\), PRIME reportsc†c^\{\\dagger\}for an agent that stops at once, and for any agent whose charged requests all check unknown atoms ofE†E^\{\\dagger\}\.

*Proof idea\.*Because checks are exact, the ledger never contradictsωx\\omega\_\{x\}\. So nothing abovec†c^\{\\dagger\}is ever authorized, and some routep†p^\{\\dagger\}ofc†c^\{\\dagger\}, true underωx\\omega\_\{x\}, is never blocked\. Whileb≥N⁡\(z\)b\\geq N\(z\),p†p^\{\\dagger\}fits the budget, so the targetc⋆c^\{\\star\}isc†c^\{\\dagger\}or stronger\. Its route then lies inE†E^\{\\dagger\}, and each completion check lowersbbandN⁡\(z\)N\(z\)by one, which preservesb≥N⁡\(z\)b\\geq N\(z\)\. Completion therefore ends either withc†c^\{\\dagger\}authorized or with every atom ofE†E^\{\\dagger\}settled, which also authorizesc†c^\{\\dagger\}\(Appendix[B](https://arxiv.org/html/2610.22426#A2)\)\.

*The bound is tight, andbminb\_\{\\min\}is not enough\.*Letbminb\_\{\\min\}be the cost of the cheapest route to the strongest conclusion\. Takec1≺c2≺c3c\_\{1\}\\prec c\_\{2\}\\prec c\_\{3\}with routes\{e1\}\\\{e\_\{1\}\\\}or\{e3\}\\\{e\_\{3\}\\\}forc1c\_\{1\},\{e1,e2\}\\\{e\_\{1\},e\_\{2\}\\\}or\{e3,e4\}\\\{e\_\{3\},e\_\{4\}\\\}forc2c\_\{2\}, and\{e1,e5,e2\}\\\{e\_\{1\},e\_\{5\},e\_\{2\}\\\}forc3c\_\{3\}, checked in that order, where onlye2e\_\{2\}is false\. The target rule first pursuesc3c\_\{3\}, spends three checks learning thate2e\_\{2\}fails, and only then turns to\{e3,e4\}\\\{e\_\{3\},e\_\{4\}\\\}\. With 3 calls, which equalsbminb\_\{\\min\}and exceeds the 2\-call cost ofc2c\_\{2\}’s true route, PRIME ends atc1c\_\{1\}\. With 4 calls, one fewer thanN⁡\(z0\)N\(z\_\{0\}\), it still ends atc1c\_\{1\}, and withN⁡\(z0\)=5N\(z\_\{0\}\)=5calls it reachesc2c\_\{2\}\.

*Why it matters\.*Under these premises, whenever the agent’s checking ends without an accepted report and withb≥N⁡\(z\)b\\geq N\(z\), PRIME reachesc†c^\{\\dagger\}and never reports above it \(Theorem[4\.2](https://arxiv.org/html/2610.22426#S4.Thmtheorem2)withPr⁡\(Eprog\)=Pr⁡\(Eres\)=0\\Pr\(E\_\{\\mathrm\{prog\}\}\)=\\Pr\(E\_\{\\mathrm\{res\}\}\)=0\), so it earns the largest utility that Problem \([2](https://arxiv.org/html/2610.22426#S2.E2)\) allows\. The bound gives a budget rule that can be computed before checking, sinceN⁡\(z0\)N\(z\_\{0\}\)is at most the number of distinct checks on all routes\. The guarantee requires sufficient remaining budget and known evidence locations; it does not cover early stopping without completion or checks requiring field discovery\.

## 5Positioning, Advantages, and Costs

ApproachControlsNext checkAnswer verification, citation\([Dhuliawala et al\., 2024](https://arxiv.org/html/2610.22426#bib.bib7);[Gao et al\., 2023](https://arxiv.org/html/2610.22426#bib.bib9)\)nothing; claims rechecked afterwardnot chosenConformal factuality\([Mohri and Hashimoto, 2024](https://arxiv.org/html/2610.22426#bib.bib17)\)claims, at calibrated risknot chosenAction rules\([Wang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib35);[Doshi et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib8)\)agent actionsnot chosenEvidence\-gated control\([Xia and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib37);[Huang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib11);[Ren, 2026](https://arxiv.org/html/2610.22426#bib.bib23)\)claims or transitionsrepair or stopEvidence acquisition\([Zhang et al\., 2026b](https://arxiv.org/html/2610.22426#bib.bib42);[Liu and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib15)\)stopping rule or verifier acceptanceuncertainty or information gainPRIMEgraded conclusions, every policyopen route of the strongest reachable conclusionTable 1:What each family enforces and how it chooses further evidence\. Among these families, only PRIME uses alternative routes both to authorize a conclusion and to choose the next check\.#### What is new\.

PRIME does not claim to originate evidence gating, precommitment, or cost\-aware probing\. Evidence\-gated systems already admit claims only on attested evidence under contracts fixed in advance\([Xia and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib37);[Huang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib11);[Ren, 2026](https://arxiv.org/html/2610.22426#bib.bib23)\), and HESP combines cost\-aware probing with evidence\-backed stopping\([Liu and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib15)\)\. To our knowledge, PRIME is the first to use one committed set of alternative routes for two jobs: deciding which*graded*conclusion the recorded checks authorize, and finding which*still\-live*route could authorize a stronger one within budget \(Table[1](https://arxiv.org/html/2610.22426#S5.T1)\)\. The ingredients are classical\. Minimal routes are prime implicants\([Quine, 1952](https://arxiv.org/html/2610.22426#bib.bib19)\), as in diagnosis and truth maintenance\([Reiter, 1987](https://arxiv.org/html/2610.22426#bib.bib22);[de Kleer, 1986](https://arxiv.org/html/2610.22426#bib.bib3)\), and budgeted checking is sequential testing\([Ünlüyurt, 2004](https://arxiv.org/html/2610.22426#bib.bib32)\)\. Appendix[H](https://arxiv.org/html/2610.22426#A8)discusses related work at length\.

#### Advantages\.

PRIME uses the same fixed evidence routes to guide checking and authorize conclusions\. Every reported conclusion can be audited against its program and evidence ledger\.

#### Costs\.

PRIME requires a review program, supplied or generated\. Its guarantees concern authorization, not the correctness of the rules or observations \(Theorem[4\.2](https://arxiv.org/html/2610.22426#S4.Thmtheorem2)\)\. Verifying model judgments adds model calls\. With known fields and deterministic checks, scripted checking is a viable alternative; agent\-directed checking is relevant when evidence must first be located\.

## 6SUFFICE

#### Motivation\.

τ\\tau\-bench scores final database outcomes\([Yao et al\., 2025](https://arxiv.org/html/2610.22426#bib.bib38)\), Partial Evidence Bench addresses inaccessible evidence\([Tallam, 2026](https://arxiv.org/html/2610.22426#bib.bib31)\), and the Evidence Sufficiency Benchmark tests answering or abstaining with supplied evidence\([Zhang and Wu, 2026](https://arxiv.org/html/2610.22426#bib.bib40)\)\. None jointly evaluates budgeted evidence collection and graded conclusions authorized by completed alternative routes\. SUFFICE measures both failures of Section[1](https://arxiv.org/html/2610.22426#S1), unsupported and missed conclusions\.

#### Construction\.

SUFFICE contains 938 tasks built from public records in the Open Source Vulnerabilities \(OSV\) database, ClinicalTrials\.gov registrations, openFDA recalls, and financial filings in the U\.S\. Securities and Exchange Commission’s Electronic Data Gathering, Analysis, and Retrieval \(EDGAR\) system\. A common structure supports comparisons across record schemas\. Each of 120 task families fixes a request, three strength\-ordered conclusions, routes, and field predicates\. The generator evaluates predicates on records to compute the intended standardfx⋆f^\{\\star\}\_\{x\}and checks that resolvers reproduce those values\. To block routes, the generator sets required values that records do not meet, occasionally synthetic values outside a field’s valid range, and withholds some evidence \(Appendix[C](https://arxiv.org/html/2610.22426#A3)\)\. An LLM coding assistant drafted candidate fields and conclusion descriptions, but checks are executable\.

#### Splits\.

The 938 tasks comprise 480 balanced, 218 natural\-prevalence, 192 development, and 48 validation tasks, and development and validation use 60 families disjoint from the held\-out ones\. The balanced split has 120 tasks per domain, 396 with at least one supported conclusion, and equal numbers of nested tasks, whose successive conclusions use extending routes, and branching tasks, where one conclusion has two alternative sufficient routes\. The natural\-prevalence split keeps each record’s own evidence without constructed failures and is not analyzed here\. Two held\-out variants are counted separately, a locator\-uncertain copy of the balanced split with three candidate fields per atom and a 240\-task split that replaces selected field checks with text judgments\. Every task leavesΦx\\Phi\_\{x\}empty\.

#### Scoring\.

*False authorization*is the share of evaluated episodes reporting a conclusion unsupported by source records\.*Premature conclusions*, counted the same way, lack a recorded complete route to themselves or a stronger conclusion, even if factually true\. False authorization is judged against the source records, and premature reporting against the recorded checks\.*Supported utility*scores the strongest source\-supported conclusion reported as 33\.3, 66\.7, or 100, and zero otherwise\.*Emission*is the share of answerable tasks, those supporting some conclusion, that receive one\. A direct\-answer baseline using Qwen2\.5\-32B\-Instruct without tools scores 30\.3 utility and 42\.1% false authorization on the balanced split, showing why utility alone does not establish checked support\. Executable requirements, not an LLM judge, determine all scores\.

#### Statistics\.

The information and guidance comparisons of Sections[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)and[7\.2](https://arxiv.org/html/2610.22426#S7.SS2)on the balanced split were registered before confirmatory evaluation\. We use task families for inference, paired sign\-flip tests, 95% bootstrap confidence intervals \(CIs\), and Holm correction within registered groups\. Other analyses, including premature\-conclusion rates added afterward, are secondary\. Tables report pooled rates\. The corpus, scorer, generator, runtime, agents, and logs are public at the links in Section[8](https://arxiv.org/html/2610.22426#S8)\. Appendix[C](https://arxiv.org/html/2610.22426#A3)details construction and splits, and Appendix[D](https://arxiv.org/html/2610.22426#A4)details statistical procedures\.

## 7Experiments

We ask which parts of PRIME prevent unsupported reports and which help agents reach stronger conclusions when evidence is costly or uncertain\. Unless noted, experiments use Qwen2\.5\-32B\-Instruct\([Qwen Team, 2024](https://arxiv.org/html/2610.22426#bib.bib20)\)on the 480\-task balanced split with a budget of 20 tool requests, which include reporting requests\. Total model calls and tokens are not matched\. Appendix[C](https://arxiv.org/html/2610.22426#A3)gives the complete charging rule\.

### 7\.1Information versus enforcement

AgentFalseauth\. %↓\\downarrowPrem\.%↓\\downarrowAgainstledger↓\\downarrowUtil\.↑\\uparrowEmit%↑\\uparrowReAct13\.056\.9617\.959\.0\+verify19\.947\.6310\.049\.6\+spec\+verify22\.333\.85526\.989\.9\+program\+verify22\.325\.25632\.798\.5Fully informed agent26\.728\.36738\.099\.0PRIME, no guidance0\.00\.0030\.199\.0PRIME0\.00\.0045\.5100\.0Table 2:Information versus enforcement \(480 tasks\)\. \+verify adds an instruction to verify, \+spec the specification view \(each atom and its field\), \+program the routes, and the fully informed agent its ledger\. Up to four incomplete episodes were excluded per row\. Against ledger counts claims with a recorded failed check on every route\. Prem\. is premature reporting, and Emit is reporting among answerable tasks\.Does showing an agent the requirements and its checked evidence prevent unsupported reporting, or is external enforcement necessary? We progressively reveal verification instructions, checks, routes, and the ledger, then add PRIME’s authorization gate and guidance\.

More information did not stop unsupported reporting, but the authorization gate did\.Table[2](https://arxiv.org/html/2610.22426#S7.T2)shows false authorization rising from 13\.0% for ReAct\([Yao et al\., 2023](https://arxiv.org/html/2610.22426#bib.bib39)\)to 26\.7% for the fully informed agent, which sees the routes and its own ledger but is not enforced and reported 67 conclusions against that ledger\. Adding the gate reduced false authorization to 0\.0%, with or without guidance\. On SUFFICE, Theorems[4\.1](https://arxiv.org/html/2610.22426#S4.Thmtheorem1)and[4\.2](https://arxiv.org/html/2610.22426#S4.Thmtheorem2)guarantee this zero, because the program is the reference standard and the resolvers reproduce its atom values\.

Fully informedFAremovedUtil\. with gate↑\\uparrowModelFA %↓\\downarrowUtil\.↑\\uparrow\[95% CI\]no guid\.PRIMEQwen2\.5\-32B26\.738\.028\.0 \[22\.7, 33\.5\]30\.145\.5gpt\-oss\-20b17\.730\.518\.0 \[13\.5, 22\.7\]26\.958\.5Mistral\-24B19\.435\.219\.5 \[14\.9, 24\.2\]29\.336\.6Qwen2\.5\-7B0\.41\.00\.5 \[0\.0, 2\.1\]24\.726\.1Table 3:Other models \(480 tasks, 20 calls\)\. Mistral\-24B is Mistral\-Small\-24B\. FA is false authorization, and FA removed is the family\-mean reduction from the gate\. With the gate, every model had 0% false authorization\.The result held across models\.Table[3](https://arxiv.org/html/2610.22426#S7.T3)shows that the gate removed 18\.0 and 19\.5 points of false authorization for gpt\-oss\-20b\([OpenAI, 2025](https://arxiv.org/html/2610.22426#bib.bib18)\)and Mistral\-Small\-24B\([Mistral AI, 2025](https://arxiv.org/html/2610.22426#bib.bib16)\)\. Guidance raised utility for every model, by 1\.4 to 31\.6 points\. Qwen2\.5\-7B shows where the gate has little to remove: without it, the agent stated a conclusion on only 3\.8% of answerable tasks\. Under sampled decoding, false authorization was 25\.4–26\.9% without the gate and 0% with it \(Appendix[E\.1](https://arxiv.org/html/2610.22426#A5.SS1)\)\.

### 7\.2Guidance and evidence location

Does the authorization gate cause agents to stop before gathering enough evidence for stronger conclusions? We test whether guidance and completion recover those conclusions, and whether agent\-directed search beats fixed\-order checking \(blind enumeration\) when each condition has three possible evidence locations\.

Figure 2:Supported utility by budget with known \(left\) or uncertain \(right\) evidence locations\. Dashed curves denote scripted checking policies \(Appendix[C](https://arxiv.org/html/2610.22426#A3)\)\. Right\-panel completion replays logged episodes without model calls\.bminb\_\{\\min\}is the cost of the cheapest committed route to the strongest conclusion before checking\.With the gate alone, agents stopped before obtaining stronger supported conclusions\.Figure[2](https://arxiv.org/html/2610.22426#S7.F2)\(left\) shows utility of 30\.1 without guidance and 45\.5 with guidance at 20 tool requests\. Completion reached 59\.2, the maximum for this split, by2​bmin2b\_\{\\min\}\. Preventing unsupported reports therefore does not ensure that useful remaining checks are performed\.

When evidence fields were uncertain, choosing where to check helped under tight budgets\.Figure[2](https://arxiv.org/html/2610.22426#S7.F2)\(right\) shows that atbminb\_\{\\min\}PRIME scored 51\.5 against 40\.3 for blind enumeration, while a policy given the correct fields \(true locators\) scored 59\.2\. At2​bmin2b\_\{\\min\}, blind enumeration reached 58\.5 but PRIME fell to 48\.8 after early stopping, while replayed completion restored 59\.2\. The benefit of agent\-directed search therefore depends on the budget and on the model \(Appendix[E\.3](https://arxiv.org/html/2610.22426#A5.SS3)\)\.

### 7\.3Judging textual evidence

Can the authorization gate prevent unsupported reporting when an LLM, rather than a deterministic resolver, judges the evidence? We replace selected checks with text judgments on 240 tasks, scored against structured registry fields withheld from the agent, and test requiring a second, agreeing judgment before accepting an observation\.

AgentFA%↓\\downarrowUtil\.↑\\uparrowAdm\.att\.Res\.err\. %↓\\downarrowEp\.err\. %↓\\downarrowFully informed agent4\.258\.52109\.58\.3PRIME, no guidance1\.747\.415113\.28\.3PRIME4\.657\.529810\.111\.7PRIME, verified0\.855\.12222\.72\.5Table 4:Text judgments \(240 tasks\)\. FA is false authorization, Adm\. att\. counts accepted judgments, Res\. err\. is the share of them that are wrong, and Ep\. err\. is the share of episodes with such an error\.The gate cannot correct a wrong judgment once the runtime accepts it as evidence\.Table[4](https://arxiv.org/html/2610.22426#S7.T4)shows false authorization of 4\.6% for PRIME, falling to 0\.8% with verification, while supported utility decreased from 57\.5 to 55\.1 and verification required 1\.2 additional model calls per episode, outside the tool\-request budget\. Guidance improved utility but increased false authorization because it prompted more judgments\. Runtime authorization thus depends on the accuracy of the recorded evidence\.

### 7\.4Closest control systems

SystemFalseauth\. %↓\\downarrowPrem\.%↓\\downarrowUtil\.↑\\uparrowEmit%↑\\uparrowReads↓\\downarrowFully informed agent26\.728\.338\.099\.03\.1AgentSpec\([2026](https://arxiv.org/html/2610.22426#bib.bib35)\)stop0\.00\.038\.787\.43\.0self\-examine0\.00\.040\.192\.93\.1ResearchLoop\([2026](https://arxiv.org/html/2610.22426#bib.bib37)\)0\.00\.047\.797\.03\.2Proof\-or\-Stop\([2026](https://arxiv.org/html/2610.22426#bib.bib11)\)0\.00\.052\.099\.24\.2GLEAN\([2026b](https://arxiv.org/html/2610.22426#bib.bib42)\)14\.414\.635\.083\.33\.1HESP\([2026](https://arxiv.org/html/2610.22426#bib.bib15)\)0\.011\.759\.2 \(49\.0\)100\.03\.9PRIME0\.00\.045\.5100\.02\.8PRIME with completion0\.00\.059\.2 \(59\.2\)100\.03\.6Table 5:Adapted systems, sharing tools and requirements, on 480 tasks\. Parentheses in Util\. show scores supported by each agent’s recorded checks \(HESP and PRIME with completion\)\. Reads counts fields per task\.Does PRIME improve on existing verification and control systems given the same evidence requirements? We compare PRIME with adaptations of AgentSpec\([Wang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib35)\), ResearchLoop\([Xia and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib37)\), Proof\-or\-Stop\([Huang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib11)\), GLEAN\([Zhang et al\., 2026b](https://arxiv.org/html/2610.22426#bib.bib42)\), and HESP\([Liu and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib15)\), reimplemented on PRIME’s tool loop because most have no usable public code, with GLEAN applied as a verifier to the fully informed agent’s logged runs\. They are not exact reruns of the original systems, and they share the model, tools, requirements, resolvers, and budget but not the number of model calls\.

Some controls prevented unsupported conclusions but sacrificed supported utility\.Table[5](https://arxiv.org/html/2610.22426#S7.T5)shows zero false authorization for PRIME and every adapted system except GLEAN \(14\.4%\)\. AgentSpec, ResearchLoop, and Proof\-or\-Stop reached utility of 38\.7–52\.0, against 45\.5 for PRIME and 59\.2 for PRIME with completion\. HESP also scored 59\.2, but its conclusion was premature on 11\.7% of tasks\. When only conclusions established by recorded checks receive credit, HESP scored 49\.0 versus 59\.2 for PRIME with completion\.

Appendix[E\.5](https://arxiv.org/html/2610.22426#A5.SS5)details the adapted controllers and other budgets\.

### 7\.5Requirements generated from a regulation

PolicynnUnsupported %\[95% CI\]↓\\downarrowUtil\.↑\\uparrowCov\.%↑\\uparrow*Assistant\-built program*\(526 instances\)Ceiling\-targeting1,9991\.8 \[1\.3, 2\.5\]18\.426\.3Ceiling\-targeting6001\.7 \[0\.9, 3\.0\]19\.026\.8Fully informed agent6000\.2 \[0\.0, 0\.9\]13\.126\.8PRIME6000\.2 \[0\.0, 0\.9\]9\.926\.8PRIME, completion6001\.7 \[0\.9, 3\.0\]19\.026\.8*Protocolized program*\(1,999 instances\)Ceiling\-targeting1,9993\.5 \[2\.8, 4\.4\]47\.592\.4Ceiling\-targeting6003\.2 \[2\.0, 4\.9\]47\.792\.5Fully informed agent6000\.0 \[0\.0, 0\.6\]31\.292\.5PRIME6000\.3 \[0\.1, 1\.2\]32\.392\.5PRIME, completion6003\.2 \[2\.0, 4\.9\]47\.792\.5Table 6:Held\-out regulatory evaluation\. Cov\. is the share of registrations with a stated conclusion\. Tracker levels are 3 for late, 2 for due, and 1 otherwise\. Scripted checks use 1,999 registrations, agents 600, and missing instances count as abstentions\. Full\-evidence agreement is 22\.8% \(assistant\-built\) and 81\.6% \(protocolized\)\.Can PRIME run requirements that were not written for the benchmark? We generated programs from the U\.S\. clinical\-trial results\-reporting regulation in the Code of Federal Regulations \(CFR\), 42 CFR Part 11, and applied them to ClinicalTrials\.gov registrations\. A program can conclude that a trial must report results \(c1c\_\{1\}\), that they are due \(c2c\_\{2\}\), or that they were submitted late \(c3c\_\{3\}\)\. For the*protocolized*program, Qwen2\.5\-32B\-Instruct wrote candidates from the regulation text, and one was selected on 600 validation registrations and frozen\. An LLM coding assistant wrote the*assistant\-built*program\. The reference is an independent reporting\-status tracker\([DeVito et al\., 2018](https://arxiv.org/html/2610.22426#bib.bib5);[DeVito et al\., 2020](https://arxiv.org/html/2610.22426#bib.bib6)\)that reads the same registry, and a conclusion is unsupported when it is stronger than the tracker’s verdict\. We test both programs on 1,999 held\-out registrations from other sponsors, with agents on 600 of them \(Appendix[F](https://arxiv.org/html/2610.22426#A6)\)\.

Generated programs ran unchanged, and their errors came mainly from their rules\.Table[6](https://arxiv.org/html/2610.22426#S7.T6)shows that PRIME with completion, using the protocolized program, stated a conclusion for 92\.5% of registrations with 3\.2% unsupported, matching the scripted ceiling\-targeting policy \(Appendix[C](https://arxiv.org/html/2610.22426#A3)\)\. Without completion, the agent stopped at weaker conclusions \(utility 32\.3 against 47\.7\), as on the benchmark\. Consistent with Theorem[4\.2](https://arxiv.org/html/2610.22426#S4.Thmtheorem2), most unsupported conclusions trace to the program\. It omits the regulation’s deadline extensions for filed certifications, and 55 of the 70 unsupported conclusions on the 1,999 registrations involve such a certification\. The assistant\-built program agreed with the tracker on 98\.5% of the registrations it classified, but it classified only 26\.3%\.

## 8Conclusion

PRIME treats evidence\-based review as budgeted evidence acquisition under a hard authorization constraint\. One committed set of evidence routes both gates what the agent may report and directs it to the checks that could justify a stronger conclusion\. The gate holds for every agent policy, and the remaining error comes only from the rules and the recorded observations\. With correct rules and exact checks at known locations, completion reaches the strongest supported conclusion once the budget covers the checks on the relevant routes\. Empirically, PRIME eliminated false authorization with supplied programs and deterministic checks, guidance and completion recovered the conclusions that the gate alone missed, and model\-judged checks showed why the accuracy of admitted observations matters\.

#### Reproducibility\.

## Limitations

PRIME’s guarantees assume faithful evidence recording and a trusted runtime and renderer\. They cover authorization, not the correctness of the requirements or observations \(Section[5](https://arxiv.org/html/2610.22426#S5)\)\. SUFFICE evaluates authorization using executable requirements over four public\-record domains, rather than independently validated organizational policies\. Confirmatory results use one primary model, Qwen2\.5\-32B\-Instruct, with one greedy run per task, and only this model ran the text\-judgment and regulation experiments\. Qwen2\.5\-7B, a registered secondary model, repeated the enforcement and guidance comparisons, as did gpt\-oss\-20b and Mistral\-Small\-24B in secondary analyses without multiplicity correction\. SUFFICE tasks use emptyΦx\\Phi\_\{x\}, leaving constraint closure and conflict handling to runtime unit tests\. The regulation study compares generated programs with an independent registry tracker rather than legal adjudication\. Agent\-directed search for where model\-judged evidence is located remains untested\. Theorem[4\.3](https://arxiv.org/html/2610.22426#S4.Thmtheorem3)assumes correct programs, exact checks, and known fields, and free cached checks preclude a general termination guarantee\.

## Ethical Considerations

PRIME targets a risk of using LLM agents for record review, reporting conclusions that their checks do not justify\. It refuses such conclusions, and every conclusion it reports can be audited against its program and evidence ledger\. Its guarantees concern authorization, so an incorrect rule or observation can still produce an incorrect conclusion \(Theorem[4\.2](https://arxiv.org/html/2610.22426#S4.Thmtheorem2)\)\. Deployments in clinical, security, financial, or regulatory settings should therefore validate their programs and keep a person responsible for consequential decisions\. The regulation study measures agreement with a public tracker and makes no legal determination about any trial or sponsor\. All records are public, and Appendix[C](https://arxiv.org/html/2610.22426#A3)describes the personal details that some of them contain\.

## References

- Alshiekh et al\. \(2018\)Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu\. 2018\.[Safe reinforcement learning via shielding](https://doi.org/10.1609/aaai.v32i1.11797)\.In*Proceedings of the AAAI Conference on Artificial Intelligence*, volume 32, pages 2669–2678\.
- Chern et al\. \(2025\)I\-Chun Chern, Steffi Chern, Shiqi Chen, Weizhe Yuan, Kehua Feng, Chunting Zhou, Junxian He, Graham Neubig, and Pengfei Liu\. 2025\.[FacTool: Factuality detection in generative AI – a tool augmented framework for multi\-task and multi\-domain scenarios](https://openreview.net/forum?id=hJkQL9VtWT)\.In*Second Conference on Language Modeling \(COLM\)*\.arXiv:2307\.13528\.
- de Kleer \(1986\)Johan de Kleer\. 1986\.[An assumption\-based TMS](https://doi.org/10.1016/0004-3702(86)90080-9)\.*Artificial Intelligence*, 28\(2\):127–162\.
- Deshpande et al\. \(2016\)Amol Deshpande, Lisa Hellerstein, and Devorah Kletenik\. 2016\.[Approximation algorithms for stochastic submodular set cover with applications to Boolean function evaluation and min\-knapsack](https://doi.org/10.1145/2876506)\.*ACM Transactions on Algorithms*, 12\(3\):42:1–42:28\.
- DeVito et al\. \(2018\)Nicholas J\. DeVito, Seb Bacon, and Ben Goldacre\. 2018\.[FDAAA TrialsTracker: A live informatics tool to monitor compliance with FDA requirements to report clinical trial results](https://doi.org/10.1101/266452)\.bioRxiv preprint\.
- DeVito et al\. \(2020\)Nicholas J\. DeVito, Seb Bacon, and Ben Goldacre\. 2020\.[Compliance with legal requirement to report clinical trial results on ClinicalTrials\.gov: A cohort study](https://doi.org/10.1016/S0140-6736(19)33220-9)\.*The Lancet*, 395\(10221\):361–369\.
- Dhuliawala et al\. \(2024\)Shehzaad Dhuliawala, Mojtaba Komeili, Jing Xu, Roberta Raileanu, Xian Li, Asli Celikyilmaz, and Jason Weston\. 2024\.[Chain\-of\-verification reduces hallucination in large language models](https://doi.org/10.18653/v1/2024.findings-acl.212)\.In*Findings of the Association for Computational Linguistics: ACL 2024*, pages 3563–3578\. Association for Computational Linguistics\.
- Doshi et al\. \(2026\)Aarya Doshi, Yining Hong, Congying Xu, Eunsuk Kang, Alexandros Kapravelos, and Christian Kästner\. 2026\.[Towards verifiably safe tool use for LLM agents](https://doi.org/10.1145/3786582.3786839)\.In*Proceedings of the IEEE/ACM 48th International Conference on Software Engineering: New Ideas and Emerging Results \(ICSE\-NIER\)*, pages 201–205\. ACM\.arXiv:2601\.08012\.
- Gao et al\. \(2023\)Tianyu Gao, Howard Yen, Jiatong Yu, and Danqi Chen\. 2023\.[Enabling large language models to generate text with citations](https://doi.org/10.18653/v1/2023.emnlp-main.398)\.In*Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing*, pages 6465–6488\. Association for Computational Linguistics\.
- Geifman and El\-Yaniv \(2017\)Yonatan Geifman and Ran El\-Yaniv\. 2017\.[Selective classification for deep neural networks](https://proceedings.neurips.cc/paper_files/paper/2017/hash/4a8423d5e91fda00bb7e46540e2b0cf1-Abstract.html)\.In*Advances in Neural Information Processing Systems*, volume 30\.
- Huang et al\. \(2026\)Jek Huang, Jeffery Hsia, Jiayi Sun, Freddie Shi, Wei Huang, and Ian H\. White\. 2026\.[Proof\-or\-Stop: Don’t trust the agent, trust the evidence – loop engineering for verifiable evidence\-gated lifecycle control](https://arxiv.org/abs/2607.14890)\.*Preprint*, arXiv:2607\.14890\.
- Ignatiev et al\. \(2019\)Alexey Ignatiev, Nina Narodytska, and Joao Marques\-Silva\. 2019\.[Abduction\-based explanations for machine learning models](https://doi.org/10.1609/aaai.v33i01.33011511)\.In*Proceedings of the AAAI Conference on Artificial Intelligence*, volume 33, pages 1511–1519\.
- Kwon et al\. \(2023\)Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E\. Gonzalez, Hao Zhang, and Ion Stoica\. 2023\.[Efficient memory management for large language model serving with PagedAttention](https://doi.org/10.1145/3600006.3613165)\.In*Proceedings of the 29th Symposium on Operating Systems Principles*, pages 611–626\.
- Li et al\. \(2025\)Xiangci Li, Sihao Chen, Rajvi Kapadia, Jessica Ouyang, and Fan Zhang\. 2025\.[Minimal evidence group identification for claim verification](https://doi.org/10.18653/v1/2025.trustnlp-main.8)\.In*Proceedings of the 5th Workshop on Trustworthy NLP \(TrustNLP 2025\)*, pages 103–111\. Association for Computational Linguistics\.
- Liu and Wang \(2026\)Zhuowen Liu and Zhixuan Wang\. 2026\.[HESP: Separating what to probe from when to stop in local LLM alert\-triage agents](https://arxiv.org/abs/2609.33446)\.*Preprint*, arXiv:2609\.33446\.
- Mistral AI \(2025\)Mistral AI\. 2025\.[Mistral small 3](https://mistral.ai/news/mistral-small-3)\.Model release, 30 January 2025\.
- Mohri and Hashimoto \(2024\)Christopher Mohri and Tatsunori Hashimoto\. 2024\.[Language models with conformal factuality guarantees](https://proceedings.mlr.press/v235/mohri24a.html)\.In*Proceedings of the 41st International Conference on Machine Learning*, volume 235 of*Proceedings of Machine Learning Research*, pages 36029–36047\. PMLR\.
- OpenAI \(2025\)OpenAI\. 2025\.gpt\-oss\-120b and gpt\-oss\-20b model card\.arXiv:2508\.10925\.
- Quine \(1952\)Willard V\. Quine\. 1952\.[The problem of simplifying truth functions](https://doi.org/10.1080/00029890.1952.11988183)\.*The American Mathematical Monthly*, 59\(8\):521–531\.
- Qwen Team \(2024\)Qwen Team\. 2024\.Qwen2\.5 technical report\.arXiv:2412\.15115\.
- Reddy et al\. \(2026\)Vikas Reddy, Sumanth Reddy Challaram, and Abhishek Basu\. 2026\.[Reason less, verify more: Deterministic gates recover a silent policy\-violation failure mode in tool\-using LLM agents](https://arxiv.org/abs/2607.07405)\.*Preprint*, arXiv:2607\.07405\.
- Reiter \(1987\)Raymond Reiter\. 1987\.[A theory of diagnosis from first principles](https://doi.org/10.1016/0004-3702(87)90062-2)\.*Artificial Intelligence*, 32\(1\):57–95\.
- Ren \(2026\)Junyu Ren\. 2026\.[Evidence\-grounded verified agentic reasoning: A path toward eliminating LLM hallucination in empirical inference via tool\-attested kernel proofs](https://arxiv.org/abs/2607.12650)\.*Preprint*, arXiv:2607\.12650\.
- Roh and Han \(2026\)Daeyoung Roh and Donghee Han\. 2026\.[HALT: Verification\-aware stopping for retrieval\-augmented search agents](https://arxiv.org/abs/2608.02009)\.In*Findings of the Association for Computational Linguistics: EMNLP 2026*\.To appear\. arXiv:2608\.02009\.
- Saar\-Tsechansky et al\. \(2009\)Maytal Saar\-Tsechansky, Prem Melville, and Foster Provost\. 2009\.[Active feature\-value acquisition](https://doi.org/10.1287/mnsc.1080.0952)\.*Management Science*, 55\(4\):664–684\.
- Saju and Azim \(2026\)Md Hasan Saju and Akramul Azim\. 2026\.[Toward autonomous SOC operations: End\-to\-end LLM framework for threat detection, query generation, and resolution in security operations](https://proceedings.mlr.press/v318/saju26a.html)\.In*Proceedings of the 39th Canadian Conference on Artificial Intelligence*, volume 318 of*Proceedings of Machine Learning Research*, pages 422–433\. PMLR\.
- Schmied et al\. \(2026\)Thomas Schmied, Jörg Bornschein, Jordi Grau\-Moya, Markus Wulfmeier, and Razvan Pascanu\. 2026\.[LLMs are greedy agents: Effects of RL fine\-tuning on decision\-making abilities](https://openreview.net/forum?id=weUP6H5Ko9)\.In*International Conference on Learning Representations \(ICLR\)*\.arXiv:2504\.16078\.
- Shi et al\. \(2025\)Tianneng Shi, Jingxuan He, Zhun Wang, Hongwei Li, Linyu Wu, Wenbo Guo, and Dawn Song\. 2025\.[Progent: Securing AI agents with privilege control](https://arxiv.org/abs/2504.11703)\.*Preprint*, arXiv:2504\.11703\.
- Shih et al\. \(2018\)Andy Shih, Arthur Choi, and Adnan Darwiche\. 2018\.[A symbolic approach to explaining Bayesian network classifiers](https://doi.org/10.24963/ijcai.2018/708)\.In*Proceedings of the 27th International Joint Conference on Artificial Intelligence \(IJCAI\)*, pages 5103–5111\.
- Shinn et al\. \(2023\)Noah Shinn, Federico Cassano, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao\. 2023\.[Reflexion: Language agents with verbal reinforcement learning](https://proceedings.neurips.cc/paper_files/paper/2023/hash/1b44b878bb782e6954cd888628510e90-Abstract.html)\.In*Advances in Neural Information Processing Systems*, volume 36, pages 8634–8652\.
- Tallam \(2026\)Krti Tallam\. 2026\.[Partial Evidence Bench: Benchmarking authorization\-limited evidence in agentic systems](https://arxiv.org/abs/2605.05379)\.*Preprint*, arXiv:2605\.05379\.
- Ünlüyurt \(2004\)Tonguç Ünlüyurt\. 2004\.[Sequential testing of complex systems: A review](https://doi.org/10.1016/j.dam.2002.08.001)\.*Discrete Applied Mathematics*, 142\(1–3\):189–205\.
- U\.S\. Department of Health and Human Services \(2016\)U\.S\. Department of Health and Human Services\. 2016\.[Clinical trials registration and results information submission](https://www.federalregister.gov/d/2016-22129)\.Final rule \(42 CFR Part 11\)\. Federal Register 81\(183\):64982–65157\.
- U\.S\. Department of Health and Human Services \(2024\)U\.S\. Department of Health and Human Services\. 2024\.[Clinical trials registration and results information submission](https://www.federalregister.gov/d/2024-28475)\.Final rule, technical amendment\. Federal Register 89:97558–97559\.
- Wang et al\. \(2026\)Haoyu Wang, Christopher M\. Poskitt, and Jun Sun\. 2026\.[AgentSpec: Customizable runtime enforcement for safe and reliable LLM agents](https://doi.org/10.1145/3744916.3764546)\.In*Proceedings of the 48th IEEE/ACM International Conference on Software Engineering \(ICSE\)*, pages 2938–2950\. ACM\.
- Wei et al\. \(2024\)Jerry Wei, Chengrun Yang, Xinying Song, Yifeng Lu, Nathan Hu, Jie Huang, Dustin Tran, Daiyi Peng, Ruibo Liu, Da Huang, Cosmo Du, and Quoc V\. Le\. 2024\.[Long\-form factuality in large language models](https://doi.org/10.52202/079017-2567)\.In*Advances in Neural Information Processing Systems*, volume 37, pages 80756–80827\.
- Xia and Wang \(2026\)Yihan Xia and Taotao Wang\. 2026\.[ResearchLoop: An evidence\-gated control plane for AI\-assisted research](https://arxiv.org/abs/2605.28282)\.*Preprint*, arXiv:2605\.28282\.
- Yao et al\. \(2025\)Shunyu Yao, Noah Shinn, Pedram Razavi, and Karthik Narasimhan\. 2025\.[τ\\tau\-bench: A benchmark for tool\-agent\-user interaction in real\-world domains](https://openreview.net/forum?id=roNSXZpUDN)\.In*International Conference on Learning Representations \(ICLR\)*\.arXiv:2406\.12045\.
- Yao et al\. \(2023\)Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao\. 2023\.[ReAct: Synergizing reasoning and acting in language models](https://openreview.net/forum?id=WE_vluYUL-X)\.In*International Conference on Learning Representations \(ICLR\)*\.arXiv:2210\.03629\.
- Zhang and Wu \(2026\)Hantian Zhang and Wentai Wu\. 2026\.[Do LLMs know when evidence is insufficient? An Evidence Sufficiency Benchmark for answer\-abstention calibration in retrieval\-augmented generation](https://doi.org/10.32604/cmc.2026.086343)\.*Computers, Materials & Continua*, 89\(1\):69\.
- Zhang et al\. \(2026a\)Xiaorui Zhang, Zhuoran Cheng, Kailin Liu, Zhaoxi Sun, Shiyu Fan, Tongyu Yuan, Bin Yuan, Weizhong Qiang, and Deqing Zou\. 2026a\.[AGATE: Provenance\-based runtime defense against compositional attacks on LLM agents](https://arxiv.org/abs/2609.30830)\.*Preprint*, arXiv:2609\.30830\.
- Zhang et al\. \(2026b\)Yichi Zhang, Nabeel Seedat, Yinpeng Dong, Peng Cui, Jun Zhu, and Mihaela van der Schaar\. 2026b\.[GLEAN: Guideline\-grounded evidence accumulation for high\-stakes agent verification](https://proceedings.mlr.press/v306/zhang26fc.html)\.In*Proceedings of the 43rd International Conference on Machine Learning*, volume 306 of*Proceedings of Machine Learning Research*, pages 158266–158287\. PMLR\.arXiv:2603\.02798\.

#### Organization of the appendix\.

Appendices[A](https://arxiv.org/html/2610.22426#A1)and[B](https://arxiv.org/html/2610.22426#A2)support the formulation, method, and guarantees of Sections[2](https://arxiv.org/html/2610.22426#S2)to[4](https://arxiv.org/html/2610.22426#S4)\. Appendix[A](https://arxiv.org/html/2610.22426#A1)gives the full interaction model that Section[2](https://arxiv.org/html/2610.22426#S2)simplifies, the premises T1–T4 behind the guarantees, program validation, and conformance tests of the runtime and renderer\. Appendix[B](https://arxiv.org/html/2610.22426#A2)states PRIME as Algorithm[1](https://arxiv.org/html/2610.22426#alg1), proves Theorems[4\.1](https://arxiv.org/html/2610.22426#S4.Thmtheorem1)to[4\.3](https://arxiv.org/html/2610.22426#S4.Thmtheorem3), and describes a machine check of Theorem[4\.3](https://arxiv.org/html/2610.22426#S4.Thmtheorem3)against the runtime’s code\. Appendices[C](https://arxiv.org/html/2610.22426#A3)to[E](https://arxiv.org/html/2610.22426#A5)support the benchmark and experiments of Sections[6](https://arxiv.org/html/2610.22426#S6)and[7](https://arxiv.org/html/2610.22426#S7)\. Appendix[C](https://arxiv.org/html/2610.22426#A3)describes the records and splits, the running example, the agents and models, the charging rule, and the scripted policies\. Appendix[D](https://arxiv.org/html/2610.22426#A4)gives the statistical protocol\. Appendix[E](https://arxiv.org/html/2610.22426#A5)reports additional results in the order of Section[7](https://arxiv.org/html/2610.22426#S7): the information ladder \([E\.1](https://arxiv.org/html/2610.22426#A5.SS1)\), guidance \([E\.2](https://arxiv.org/html/2610.22426#A5.SS2)\), field choice \([E\.3](https://arxiv.org/html/2610.22426#A5.SS3)\), text judgments \([E\.4](https://arxiv.org/html/2610.22426#A5.SS4)\), and the closest systems \([E\.5](https://arxiv.org/html/2610.22426#A5.SS5)\)\. Appendix[F](https://arxiv.org/html/2610.22426#A6)runs PRIME on programs generated from a clinical\-trial regulation\. Appendix[G](https://arxiv.org/html/2610.22426#A7)reports an earlier exploratory pilot whose results are not pooled with the others\. Appendix[H](https://arxiv.org/html/2610.22426#A8)extends the comparison of Section[5](https://arxiv.org/html/2610.22426#S5)\.

## Appendix AFormal Details and Implementation Checks

#### Intended minimal routes\.

Let𝒫x⋆​\(c\)\\mathcal\{P\}\_\{x\}^\{\\star\}\(c\)denote the minimal sufficient routes for conclusioncc\. Formally,

𝒫x⋆\(c\)=MinΦx\{p∣\\displaystyle\\mathcal\{P\}\_\{x\}^\{\\star\}\(c\)=\\operatorname\{Min\}\_\{\\Phi\_\{x\}\}\\\{p\\mid\{\}Φx∧p​is satisfiable,\\displaystyle\\Phi\_\{x\}\\land p\\text\{ is satisfiable\},\(6\)p⊧Φxfx⋆\(c,⋅\)\}\.\\displaystyle p\\models\_\{\\Phi\_\{x\}\}f\_\{x\}^\{\\star\}\(c,\\cdot\)\\\}\.Here,p⊧Φxfx⋆\(c,⋅\)p\\models\_\{\\Phi\_\{x\}\}f\_\{x\}^\{\\star\}\(c,\\cdot\)means that every assignment satisfyingppandΦx\\Phi\_\{x\}justifiescc\. The operatorMinΦx\\operatorname\{Min\}\_\{\\Phi\_\{x\}\}keeps only the routes from which no condition can be removed without losing sufficiency underΦx\\Phi\_\{x\}\. We assume the intended standard respects the strength order, soc⪯xdc\\preceq\_\{x\}dandfx⋆​\(d,ω\)=1f\_\{x\}^\{\\star\}\(d,\\omega\)=1implyfx⋆​\(c,ω\)=1f\_\{x\}^\{\\star\}\(c,\\omega\)=1for every permittedω\\omega\.

#### Full interaction model\.

Section[2](https://arxiv.org/html/2610.22426#S2)states the problem in its simplest form\. The full model used by the runtime and the proofs is as follows\. A case isx=\(Sx,Vx\)x=\(S\_\{x\},V\_\{x\}\), where the*evidence view*VxV\_\{x\}holds the record’s field values and the agent initially knows onlySxS\_\{x\}\. Each atomeehas a*resolver*σx​\(e\)\\sigma\_\{x\}\(e\), the registered procedure that checks it\. A formulaΦx\\Phi\_\{x\}over the atoms expresses logical constraints, for example that a reference cannot have a URL unless the reference exists, andωx\\omega\_\{x\}satisfiesΦx\\Phi\_\{x\}\. The ledger has a fourth state𝖢\\mathsf\{C\}for atoms whose admitted observations disagree\. LetClΦx​\(z\)\\mathrm\{Cl\}\_\{\\Phi\_\{x\}\}\(z\)contain the literals established inzztogether with thoseΦx\\Phi\_\{x\}implies, excluding conflicting atoms \(definition D1 in Appendix[B](https://arxiv.org/html/2610.22426#A2)\)\. Equation \([1](https://arxiv.org/html/2610.22426#S2.E1)\) then readsClΦx​\(z\)⊧p\\mathrm\{Cl\}\_\{\\Phi\_\{x\}\}\(z\)\\models pin place ofz⊧pz\\models p, and nothing is authorized when the established literals violateΦx\\Phi\_\{x\}\. WithΦx\\Phi\_\{x\}empty and no conflicts, as in every benchmark task, the two definitions coincide\. The checking actionsChkx\\mathrm\{Chk\}\_\{x\}comprise field reads, text reads, and attestations, in which a model or person records a judgment as evidence\. After historyhth\_\{t\}, requestaacostsκx​\(a,ht\)≥0\\kappa\_\{x\}\(a,h\_\{t\}\)\\geq 0\. A cached repeat, with matching tool arguments and evidence\-read state, is free and returns its recorded result\. A checkata\_\{t\}with observationoto\_\{t\}updates the ledger byzt\+1=Δx​\(zt,at,ot\)z\_\{t\+1\}=\\Delta\_\{x\}\(z\_\{t\},a\_\{t\},o\_\{t\}\), and observations may be wrong\.emit​\(c\)\\textsc\{emit\}\(c\)is charged whether or not the runtime accepts it, andstopis free\. With remaining budgetbtb\_\{t\}, starting fromb0=Bxb\_\{0\}=B\_\{x\}, the affordable requests are

𝒜t=\\displaystyle\\mathcal\{A\}\_\{t\}=\{\}\{a∈Chkx∪\{emit\(c\)∣c∈C\}∣\\displaystyle\\\{a\\in\\mathrm\{Chk\}\_\{x\}\\cup\\\{\\textsc\{emit\}\(c\)\\mid c\\in C\\\}\\midκx\(a,ht\)≤bt\}∪\{stop\}\.\\displaystyle\\kappa\_\{x\}\(a,h\_\{t\}\)\\leq b\_\{t\}\\\}\\cup\\\{\\textsc\{stop\}\\\}\.Other requests are refused without changing the ledger but may be charged\. The utilityU⁡\(c,x\)U\(c,x\)depends only onccandSxS\_\{x\}, so the runtime can compute it before checking\. The planning estimateκ^x​\(p,z\)\\hat\{\\kappa\}\_\{x\}\(p,z\)of Equation \([4](https://arxiv.org/html/2610.22426#S3.E4)\) counts a check that settles several literals once, and it may omit the effort of locating a field whose location is uncertain\. Every actual check is still charged\. The*hold indicator*μ\\muequals11whenU⁡\(c⋆,x\)U\(c^\{\\star\},x\)exceedsU⁡\(c,x\)U\(c,x\)for everyc∈AuthP0​\(z\)∪\{⊥\}c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\\cup\\\{\\bot\\\}, and00otherwise\. PRIME holds weaker reports and issues reminders only whileμ=1\\mu=1\. The*completion setting*γ∈\{0,1\}\\gamma\\in\\\{0,1\\\}turns completion on, and when an atom’s field is uncertain, completion tries the supplied candidate fields\. If checking ends without an accepted request, PRIME reports the setMaxAuthP0​\(z\)\\mathrm\{MaxAuth\}\_\{P\_\{0\}\}\(z\)of maximal authorized conclusions, a single conclusion in the chain setting\. The structured resulty⁡\(c,z\)y\(c,z\)recordsccand its supporting ledger evidence, and a deterministic rendererRender\\mathrm\{Render\}turns it into text using fixed templates\.

#### Commitment\.

Before checking begins, the runtime validates the program \(Program validation, below\), rejects an invalid one, records the hash of an accepted one, and only then enables resolvers\. Validation tests the program’s structure, not whether its rules are correct\. In the experiments, each task file supplies the program, the runtime validates it when the task is loaded, and the program cannot change during the episode\. The hash\-gated commitment and the template renderer are exercised by the conformance tests of Table[7](https://arxiv.org/html/2610.22426#A1.T7), and the experiment runner scores the structured output directly\.

#### Decision problem\.

A*policy*πθ\\pi\_\{\\theta\}, parameterized by model parametersθ\\theta, chooses actions using the specificationSxS\_\{x\}, fixed programP0P\_\{0\}, and historyhth\_\{t\}of previous actions and observations\. At termination stepτ\\tau, the runtime either reports conclusioncτc\_\{\\tau\}or abstains, writtencτ=⊥c\_\{\\tau\}=\\bot\. Withfx⋆​\(⊥,ωx\)=0f\_\{x\}^\{\\star\}\(\\bot,\\omega\_\{x\}\)=0, the agent seeks a policy maximizing expected utility, with unsupported conclusions receiving no reward\.

maxπθ\\displaystyle\\max\_\{\\pi\_\{\\theta\}\}𝔼πθ,σx​\[U⁡\(cτ,x\)​fx⋆​\(cτ,ωx\)\]\\displaystyle\\mathbb\{E\}\_\{\\pi\_\{\\theta\},\\sigma\_\{x\}\}\\\!\\left\[U\(c\_\{\\tau\},x\)f\_\{x\}^\{\\star\}\(c\_\{\\tau\},\\omega\_\{x\}\)\\right\]\(7\)s\.t\.\\displaystyle\\mathrm\{s\.t\.\}at∈𝒜t,b0=Bx,z0=𝖴m,\\displaystyle a\_\{t\}\\in\\mathcal\{A\}\_\{t\},\\ b\_\{0\}=B\_\{x\},\\ z\_\{0\}=\\mathsf\{U\}^\{m\},bt\+1=bt−κx​\(at,ht\),\\displaystyle b\_\{t\+1\}=b\_\{t\}\-\\kappa\_\{x\}\(a\_\{t\},h\_\{t\}\),ht\+1=ht⋅\(at,ot\),\\displaystyle h\_\{t\+1\}=h\_\{t\}\\cdot\(a\_\{t\},o\_\{t\}\),zt\+1=Δx​\(zt,at,ot\)​if​at∈Chkx,\\displaystyle z\_\{t\+1\}=\\Delta\_\{x\}\(z\_\{t\},a\_\{t\},o\_\{t\}\)\\ \\text\{if \}a\_\{t\}\\in\\mathrm\{Chk\}\_\{x\},zt\+1=zt​otherwise,\\displaystyle z\_\{t\+1\}=z\_\{t\}\\ \\text\{otherwise\},cτ∈AuthP0​\(zτ\)∪\{⊥\}\.\\displaystyle c\_\{\\tau\}\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\_\{\\tau\}\)\\cup\\\{\\bot\\\}\.The expectation covers policy choices and resolver observations\. The constraints limit actions to affordable requests and require recorded evidence to authorize the reported conclusion\. Without authorization, the agent may report unsupported conclusions\.

#### Partial orders\.

The decision problem above writes a single stated conclusioncτc\_\{\\tau\}, which is exact when⪯x\\preceq\_\{x\}is a chain\. For partially ordered conclusions, an extension of the main formulation,MaxAuthP0​\(z\)\\mathrm\{MaxAuth\}\_\{P\_\{0\}\}\(z\)is an antichain\. The runtime’s final outputy​\(MaxAuthP0​\(z\),z\)y\(\\mathrm\{MaxAuth\}\_\{P\_\{0\}\}\(z\),z\)lists every maximal authorized conclusion with its established route, the renderer states each as a separate finding, the last constraint of \([7](https://arxiv.org/html/2610.22426#A1.E7)\) is read asc∈AuthP0​\(zτ\)c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\_\{\\tau\}\)for each statedcc, and utility is the maximum over the stated set\. Theorems[4\.1](https://arxiv.org/html/2610.22426#S4.Thmtheorem1)and[4\.2](https://arxiv.org/html/2610.22426#S4.Thmtheorem2)hold in this form, since neither proof compares distinct maximal elements, and Theorem[4\.3](https://arxiv.org/html/2610.22426#S4.Thmtheorem3)assumes a chain\.

#### Residual status and conflicts\.

The runtime gives each literal of a route exactly one status, which in order of precedence is satisfied, repairable \(a conflict or a retractable opposing attestation blocks it\), open \(a check can establish it\), or impossible \(a terminal unavailability certificate\)\. Precedence resolves overlaps, and if no status applies, the runtime raises an error instead of guessing\. If the settled atoms contradictΦx\\Phi\_\{x\}, it authorizes nothing, suspends route statuses, and exposes the contradicting attestations for review, never the constraint formula, so Equations \([3](https://arxiv.org/html/2610.22426#S3.E3)\) and \([4](https://arxiv.org/html/2610.22426#S3.E4)\) apply to consistent ledgers only\. A formula unsatisfiable on its own is rejected before commitment\. Neither failure state, no applicable status or settled atoms that contradictΦx\\Phi\_\{x\}, arises in the structured splits, whereΦx\\Phi\_\{x\}is empty and each atom has one deterministic resolver\.

#### Output and trusted components\.

The structured output lists the authorized conclusions, the atoms on their routes, the unresolved stronger conclusions with their residual requirements, the scope, and qualifications\. The mapdenote\\mathrm\{denote\}, which returns the conclusions a rendered text asserts \(D4 in Appendix[B](https://arxiv.org/html/2610.22426#A2)\), reads only the zone of authorized findings\. Unresolved stronger conclusions appear in a separate zone that lists their missing checks and asserts nothing\. Each rendered finding uses one of 13 templates whose slots accept identifiers, numbers, dates, or a quoted span of at most 200 characters drawn only from letters, digits, spaces, parentheses, and the characters,\.;:/\_’\-, so a slot can never forge a finding or a conclusion\. The guarantees assume \(T1\) a finite list of conclusions with a mechanically checkable order, \(T2\) a constraint formula supplied from outside and frozen for the episode, \(T3\) output produced only by the sound renderer, and \(T4\) a ledger changed only by faithfully recording, under the conflict rule of \(D1\) in Appendix[B](https://arxiv.org/html/2610.22426#A2), the values the runtime admits from resolvers or identified attesters, or by retracting such a record\. Exactly resolved atoms receive the full guarantee\. For atoms attested by a person or a model, it covers only a faithful record of the attestation, and their errors enterEresE\_\{\\mathrm\{res\}\}\. Table[7](https://arxiv.org/html/2610.22426#A1.T7)reports the implementation checks of these premises\.

#### Program validation\.

Before commitment the runtime rejects programs whose conclusions, atoms, or routes are malformed, whose atoms name no registered resolver or embedded record, whose routes are unsatisfiable together withΦx\\Phi\_\{x\}or strictly contain another route of the same conclusion, or whose routes are not order\-coherent, that is, some route of a stronger conclusion contains no route of a weaker comparable one\. A check whose field path or predicate cannot be evaluated establishes nothing at run time, and in our builds a separate linter caught such bindings before commitment\.

ConditionMaskviolationsConflictfail\-openPrematureconclusionRendererstrengtheningRetractionfailurePRIME runtime00000Templates: 52 of 52 round trips exact; strengthening mutations: 9 of 9 rejected; slot injections: 8 of 8 blocked\.Commitment inputShare of the 70 pairs with different committed programsSpecification view only \(production\)0\.000Plus each atom’s authored description0\.429Plus the true values and the answer key0\.786Table 7:Runtime and renderer tests include 52 round trips, 9 mutations, 8 injections, and 27 renderer cases\. Violation counts come from a scripted episode with 3 conclusions, 4 atoms, 1 conflict, and 1 retraction\. Commitment tests compare 70 hidden\-evidence pairs across 5 seeds and 14 perturbation types\. Deliberately leaky inputs confirm detection\.

## Appendix BProofs of the Results in Section[4](https://arxiv.org/html/2610.22426#S4)

Algorithm[1](https://arxiv.org/html/2610.22426#alg1)restates the procedure of Section[3](https://arxiv.org/html/2610.22426#S3)as pseudocode; the proofs cite its lines\.

Algorithm 1One PRIME review\. Inputs:SxS\_\{x\},BxB\_\{x\}, and completion settingγ\\gamma\.1:

P0←G⁡\(Sx,r\)P\_\{0\}\\leftarrow G\(S\_\{x\},r\); validate

P0P\_\{0\}, reject if invalid; record

hash⁡\(P0\)\\mathrm\{hash\}\(P\_\{0\}\)and enable checks

2:

z←𝖴mz\\leftarrow\\mathsf\{U\}^\{m\};

b←Bxb\\leftarrow B\_\{x\};

h←∅h\\leftarrow\\emptyset;

n←0n\\leftarrow 0⊳\\trianglerightnncounts reminders

3:while

b\>0b\>0do

4:compute

AuthP0​\(z\)\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\);

\(c⋆,p⋆\)\(c^\{\\star\},p^\{\\star\}\)by Equation \([4](https://arxiv.org/html/2610.22426#S3.E4)\);

μ←1\\mu\\leftarrow 1if

U⁡\(c⋆,x\)\>maxc∈AuthP0​\(z\)∪\{⊥\}⁡U⁡\(c,x\)U\(c^\{\\star\},x\)\>\\max\_\{c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\\cup\\\{\\bot\\\}\}U\(c,x\), else

00
5:

a←πθ​\(Sx,P0,z,h,b,AuthP0​\(z\),c⋆,R⁡\(p⋆,z\)\)a\\leftarrow\\pi\_\{\\theta\}\(S\_\{x\},P\_\{0\},z,h,b,\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\),c^\{\\star\},R\(p^\{\\star\},z\)\)
6:if

κx​\(a,h\)\>b\\kappa\_\{x\}\(a,h\)\>bthenrefuse

aa; end checking

7:

b←b−κx​\(a,h\)b\\leftarrow b\-\\kappa\_\{x\}\(a,h\)
8:if

a=emit​\(c\)a=\\textsc\{emit\}\(c\)thenrecompute

\(c⋆,p⋆\)\(c^\{\\star\},p^\{\\star\}\)and

μ\\muas in line[4](https://arxiv.org/html/2610.22426#alg1.l4)with the charged

bb
9:if

a∈Chkxa\\in\\mathrm\{Chk\}\_\{x\}is a registered check with allowed parametersthenrun its resolver, or return its recorded result if

aarepeats a cache\-eligible request; update

zz,

hh
10:else if

a=emit​\(c\)a=\\textsc\{emit\}\(c\),

c∈AuthP0​\(z\)c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\), and

μ=0\\mu=0thenreturn

Render⁡\(y⁡\(c,z\)\)\\mathrm\{Render\}\(y\(c,z\)\)
11:else if

a=emit​\(c\)a=\\textsc\{emit\}\(c\),

c∈AuthP0​\(z\)c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\), and

μ=1\\mu=1thenhold the request; update

hh
12:else if

a=stopa=\\textsc\{stop\},

μ=1\\mu=1, and

n<3n<3thenremind the agent;

n←n\+1n\\leftarrow n\+1; update

hh
13:else if

a=stopa=\\textsc\{stop\}thenif

μ=1\\mu=1and

γ=1\\gamma=1, run the open checks of

p⋆p^\{\\star\}while

μ=1\\mu=1and

b\>0b\>0, recomputing

\(c⋆,p⋆\)\(c^\{\\star\},p^\{\\star\}\)and

μ\\muafter each and charging each as in line[7](https://arxiv.org/html/2610.22426#alg1.l7); end checking

14:elserefuse

aa; update

hhwithout changing

zz
15:return

Render⁡\(y⁡\(MaxAuthP0​\(z\),z\)\)\\mathrm\{Render\}\(y\(\\mathrm\{MaxAuth\}\_\{P\_\{0\}\}\(z\),z\)\), a single conclusion in a chain, or abstain if empty

Line[6](https://arxiv.org/html/2610.22426#alg1.l6)never applies in our benchmark, because every charge is zero or one call and checking ends when the budget reaches zero\. Every emission is charged \(line[7](https://arxiv.org/html/2610.22426#alg1.l7)\), so line[8](https://arxiv.org/html/2610.22426#alg1.l8)recomputes the target and the hold test with the budget left after that charge, and an emission is held only while a stronger conclusion remains reachable within that budget\. The final statement in line[15](https://arxiv.org/html/2610.22426#alg1.l15)is free, so an authorized conclusion is still reported when the budget runs out, including one whose emission was held\. Cached repeats are free, so a policy can repeat them without reducingbb, and the loop need not terminate for every policy\. The guarantees therefore hold for every episode that produces an output\.

Each line of a proof chains steps with arrows\. A bracket names the premise, result, or line of Algorithm[1](https://arxiv.org/html/2610.22426#alg1)that a step uses; steps that only apply a definition or routine algebra carry no bracket\.

#### Definitions used in the proofs\.

\(D1\) The update ruleΔx\\Delta\_\{x\}sets an atom to𝖳\\mathsf\{T\}\(𝖥\\mathsf\{F\}\) when every admitted, unretracted value for it is 1 \(0\), to𝖢\\mathsf\{C\}when such values disagree, and leaves it𝖴\\mathsf\{U\}when there is none\. For a ledgerzz, the settled literals areL⁡\(z\)=\{ei:zi=𝖳\}∪\{¬ei:zi=𝖥\}L\(z\)=\\\{e\_\{i\}:z\_\{i\}=\\mathsf\{T\}\\\}\\cup\\\{\\neg e\_\{i\}:z\_\{i\}=\\mathsf\{F\}\\\}and the conflicting atoms areK⁡\(z\)=\{i:zi=𝖢\}K\(z\)=\\\{i:z\_\{i\}=\\mathsf\{C\}\\\}\. IfΦx∧⋀L⁡\(z\)\\Phi\_\{x\}\\wedge\\bigwedge L\(z\)is unsatisfiable, thenClΦx\(z\)=⊥\\mathrm\{Cl\}\_\{\\Phi\_\{x\}\}\(z\)=\\bot; otherwiseClΦx\(z\)=\{ℓ:the atom ofℓ∉K\(z\),Φx∧⋀L\(z\)⊧ℓ\}\\mathrm\{Cl\}\_\{\\Phi\_\{x\}\}\(z\)=\\\{\\ell:\\text\{the atom of \}\\ell\\notin K\(z\),\\ \\Phi\_\{x\}\\wedge\\bigwedge L\(z\)\\models\\ell\\\}\. A routeppholds atzz, writtenClΦx​\(z\)⊧p\\mathrm\{Cl\}\_\{\\Phi\_\{x\}\}\(z\)\\models p, whenClΦx\(z\)≠⊥\\mathrm\{Cl\}\_\{\\Phi\_\{x\}\}\(z\)\\neq\\botandp⊆ClΦx​\(z\)p\\subseteq\\mathrm\{Cl\}\_\{\\Phi\_\{x\}\}\(z\)\. We abbreviateClΦx\\mathrm\{Cl\}\_\{\\Phi\_\{x\}\}toCl\\mathrm\{Cl\}\. \(D2\)MaxAuthP​\(z\)=\{c∈AuthP​\(z\):no​d∈AuthP​\(z\)​has​c≺d\}⊆AuthP​\(z\)\\mathrm\{MaxAuth\}\_\{P\}\(z\)=\\\{c\\in\\mathrm\{Auth\}\_\{P\}\(z\):\\text\{no \}d\\in\\mathrm\{Auth\}\_\{P\}\(z\)\\text\{ has \}c\\prec d\\\}\\subseteq\\mathrm\{Auth\}\_\{P\}\(z\), wherec≺dc\\prec dmeansc⪯dc\\preceq dandc≠dc\\neq d\. \(D3\) In each pass of the loop of Algorithm[1](https://arxiv.org/html/2610.22426#alg1), the runtime computesAuthP0​\(zt\)\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\_\{t\}\)\(line[4](https://arxiv.org/html/2610.22426#alg1.l4)\) and decides on the proposed action without changing the ledger in between\. A check setszt\+1=Δx​\(zt,at,ot\)z\_\{t\+1\}=\\Delta\_\{x\}\(z\_\{t\},a\_\{t\},o\_\{t\}\)\(line[9](https://arxiv.org/html/2610.22426#alg1.l9)\), and completion \(line[13](https://arxiv.org/html/2610.22426#alg1.l13)\) appliesΔx\\Delta\_\{x\}once per check it runs, sozτz\_\{\\tau\}is the ledger after completion\. A refused request \(line[14](https://arxiv.org/html/2610.22426#alg1.l14)\), a held emission \(line[11](https://arxiv.org/html/2610.22426#alg1.l11)\), and a reminder \(line[12](https://arxiv.org/html/2610.22426#alg1.l12)\) only extend the history, sozt\+1=ztz\_\{t\+1\}=z\_\{t\}, and output nothing\. Every request exceptstopand a cached repeat of a check or of an unrecognized request reducesbb, so emissions are always charged, and the episode ends when an emission is accepted, when checking ends, or when the budget is spent\. An emissionemit​\(c\)\\textsc\{emit\}\(c\)is accepted \(line[10](https://arxiv.org/html/2610.22426#alg1.l10)\) only ifc∈AuthP0​\(zt\)c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\_\{t\}\)andμ=0\\mu=0, and acceptance ends the episode\. Otherwise the episode ends at a timeτ\\tauand the runtime statesMaxAuthP0​\(zτ\)\\mathrm\{MaxAuth\}\_\{P\_\{0\}\}\(z\_\{\\tau\}\)or abstains \(line[15](https://arxiv.org/html/2610.22426#alg1.l15)\)\. \(D4\) When an episode ends at ledgerzz, the runtime returns a structured outputyy;M⁡\(y\)M\(y\)denotes the conclusionsyymarks as authorized: the stated conclusion and the authorized conclusionsyylists, which the runtime takes fromAuthP0​\(z\)\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\. “PRIME outputsccatzz” meansc∈M⁡\(y\)c\\in M\(y\)\. The user seess=Render⁡\(y\)s=\\mathrm\{Render\}\(y\)and the conclusionsdenote⁡\(s\)\\mathrm\{denote\}\(s\)\. \(D5\)Emask=\{M\(y\)⊈AuthP0\(z\)\}E\_\{\\mathrm\{mask\}\}=\\\{M\(y\)\\not\\subseteq\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\\\},Erender=\{denote\(s\)⊈M\(y\)\}E\_\{\\mathrm\{render\}\}=\\\{\\mathrm\{denote\}\(s\)\\not\\subseteq M\(y\)\\\}, andEuser=\{∃c∈denote⁡\(s\):fx⋆​\(c,ωx\)=0\}E\_\{\\mathrm\{user\}\}=\\\{\\exists c\\in\\mathrm\{denote\}\(s\):f^\{\\star\}\_\{x\}\(c,\\omega\_\{x\}\)=0\\\};EprogE\_\{\\mathrm\{prog\}\}andEresE\_\{\\mathrm\{res\}\}are as in Section[4](https://arxiv.org/html/2610.22426#S4)\.

Part \(i\) of Theorem[4\.1](https://arxiv.org/html/2610.22426#S4.Thmtheorem1)in full reads as follows\. Letx=\(S,V\)x=\(S,V\)andx′=\(S,V′\)x^\{\\prime\}=\(S,V^\{\\prime\}\)have the same specification and arbitrary evidence views\. IfGGis invoked only onSSand fixed randomnessrr, and no resolver can run before the hash of the committed program is recorded, both cases receive the programG⁡\(S,r\)G\(S,r\)with the same hash\. IfGGdraws its seed for both cases from one distribution that does not depend on the evidence view, the committed programs have the same distribution\.

###### Proof of Theorem[4\.1](https://arxiv.org/html/2610.22426#S4.Thmtheorem1), part \(i\)\.

ModelGGas an algorithm that runs in roundsj=1,2,…j=1,2,\\dots\. In roundjj, ifδj​\(S,r,a1,…,aj−1\)=halt\\delta\_\{j\}\(S,r,a\_\{1\},\\dots,a\_\{j\-1\}\)=\\mathrm\{halt\}, it returnsgj​\(S,r,a1,…,aj−1\)g\_\{j\}\(S,r,a\_\{1\},\\dots,a\_\{j\-1\}\), and otherwise it sends a resolver request and receivesaja\_\{j\}\. It halts after finitely many rounds\. The hash is computed from the program it returns, so every request precedes the recording of the hash, and the gate answers it with⊥\\botwhatever the evidence view\. Hence, by induction onjj,

aj=⊥∀j\\displaystyle a\_\{j\}=\\bot\\ \\ \\forall j⇒J=min\{j:δj\(S,r,⊥j−1\)=halt\}\\displaystyle\\Rightarrow J=\\min\\\{j:\\delta\_\{j\}\(S,r,\\bot^\{j\-1\}\)=\\mathrm\{halt\}\\\}⇒P0=gJ\(S,r,⊥J−1\)=:G^\(S,r\)\\displaystyle\\Rightarrow P\_\{0\}=g\_\{J\}\(S,r,\\bot^\{J\-1\}\)=:\\hat\{G\}\(S,r\)⇒P0​\(x\)=G^​\(S,r\)=P0​\(x′\)​\[Sx=Sx′\]\\displaystyle\\Rightarrow P\_\{0\}\(x\)=\\hat\{G\}\(S,r\)=P\_\{0\}\(x^\{\\prime\}\)\\ \\text\{\[$S\_\{x\}=S\_\{x^\{\\prime\}\}$\]\}⇒hash⁡\(P0​\(x\)\)=hash⁡\(P0​\(x′\)\)\.\\displaystyle\\Rightarrow\\mathrm\{hash\}\(P\_\{0\}\(x\)\)=\\mathrm\{hash\}\(P\_\{0\}\(x^\{\\prime\}\)\)\.Neither evidence view appears in these lines, so both are arbitrary\. IfGGis randomized and the cases draw seedsρ,ρ′\\rho,\\rho^\{\\prime\}from the same distributionν\\nu, which does not depend on the evidence view, then for every set𝒜\\mathcal\{A\}of programs

Pr⁡\(P0​\(x\)∈𝒜\)=Pr⁡\(G^​\(S,ρ\)∈𝒜\)\\displaystyle\\Pr\(P\_\{0\}\(x\)\\in\\mathcal\{A\}\)=\\Pr\(\\hat\{G\}\(S,\\rho\)\\in\\mathcal\{A\}\)=ν⁡\(\{r:G^​\(S,r\)∈𝒜\}\)​\[ρ∼ν\]\\displaystyle=\\nu\(\\\{r:\\hat\{G\}\(S,r\)\\in\\mathcal\{A\}\\\}\)\\ \\text\{\[$\\rho\\sim\\nu$\]\}=Pr⁡\(G^​\(S,ρ′\)∈𝒜\)​\[ρ′∼ν\]\\displaystyle=\\Pr\(\\hat\{G\}\(S,\\rho^\{\\prime\}\)\\in\\mathcal\{A\}\)\\ \\text\{\[$\\rho^\{\\prime\}\\sim\\nu$\]\}=Pr⁡\(P0​\(x′\)∈𝒜\)\.\\displaystyle=\\Pr\(P\_\{0\}\(x^\{\\prime\}\)\\in\\mathcal\{A\}\)\.∎

###### Proof of Theorem[4\.1](https://arxiv.org/html/2610.22426#S4.Thmtheorem1), part \(ii\)\.

By \(D3\) the runtime outputs conclusions only when the episode ends, either with an acceptedemit​\(c\)\\textsc\{emit\}\(c\)at timett\(z=ztz=z\_\{t\}\) or at a timeτ\\tauwithout one \(z=zτz=z\_\{\\tau\}\)\. LetL⊆AuthP0​\(z\)L\\subseteq\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)be the authorized conclusions the output lists \(D4\)\.

Case 1:emit\(c\)accepted\\displaystyle\\text\{Case 1: \}\\textsc\{emit\}\(c\)\\text\{ accepted\}⇒c∈AuthP0​\(zt\)​\[lines[4](https://arxiv.org/html/2610.22426#alg1.l4),[10](https://arxiv.org/html/2610.22426#alg1.l10)\]\\displaystyle\\Rightarrow c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\_\{t\}\)\\ \\text\{\[lines~\\ref\{alg:auth\},~\\ref\{alg:accept\}\]\}⇒M⁡\(y\)=\{c\}∪L⊆AuthP0​\(zt\);\\displaystyle\\Rightarrow M\(y\)=\\\{c\\\}\\cup L\\subseteq\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\_\{t\}\);Case 2:M\(y\)=MaxAuthP0\(zτ\)∪L\\displaystyle\\text\{Case 2: \}M\(y\)=\\mathrm\{MaxAuth\}\_\{P\_\{0\}\}\(z\_\{\\tau\}\)\\cup L⊆AuthP0​\(zτ\)​\[line[15](https://arxiv.org/html/2610.22426#alg1.l15); D2\]\\displaystyle\\qquad\\subseteq\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\_\{\\tau\}\)\\ \\text\{\[line~\\ref\{alg:final\}; D2\]\}⇒M⁡\(y\)⊆AuthP0​\(z\)​always\\displaystyle\\Rightarrow M\(y\)\\subseteq\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\\text\{ always\}⇒Emask=∅\.\\displaystyle\\Rightarrow E\_\{\\mathrm\{mask\}\}=\\varnothing\.If nothing is authorized atzτz\_\{\\tau\}, the runtime abstains andM⁡\(y\)=L=∅M\(y\)=L=\\varnothing\. Neither case used a property of the policy, the actions, the resolver outcomes, the budget, or the stopping time\. ∎

###### Proof of Theorem[4\.1](https://arxiv.org/html/2610.22426#S4.Thmtheorem1), part \(iii\)\.

For any episode with final ledgerzz, outputyy, and texts=Render⁡\(y\)s=\\mathrm\{Render\}\(y\),

denote⁡\(s\)⊆M⁡\(y\)⊆AuthP0​\(z\)\\displaystyle\\mathrm\{denote\}\(s\)\\subseteq M\(y\)\\subseteq\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\[soundness; part \(ii\)\]⇒denote⁡\(s\)⊆AuthP0​\(z\);\\displaystyle\\Rightarrow\\mathrm\{denote\}\(s\)\\subseteq\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\);denote⁡\(Render⁡\(y\)\)⊆M⁡\(y\)​∀y​\[soundness\]\\displaystyle\\mathrm\{denote\}\(\\mathrm\{Render\}\(y\)\)\\subseteq M\(y\)\\ \\forall y\\ \\text\{\[soundness\]\}⇒Erender=∅\.\\displaystyle\\Rightarrow E\_\{\\mathrm\{render\}\}=\\varnothing\.Every evaluative sentence the user sees comes fromss, so every conclusion the user sees lies inAuthP0​\(z\)\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\. ∎

###### Proof of Theorem[4\.2](https://arxiv.org/html/2610.22426#S4.Thmtheorem2)\.

Let𝒢=Erender∪Emask∪Eres\\mathcal\{G\}=E\_\{\\mathrm\{render\}\}\\cup E\_\{\\mathrm\{mask\}\}\\cup E\_\{\\mathrm\{res\}\}and take an episode inEuser∖𝒢E\_\{\\mathrm\{user\}\}\\setminus\\mathcal\{G\}, with final ledgerzz, outputyy, and textss:

∃c∈denote⁡\(s\):fx⋆​\(c,ωx\)=0\\displaystyle\\exists c\\in\\mathrm\{denote\}\(s\):f^\{\\star\}\_\{x\}\(c,\\omega\_\{x\}\)=0⇒c∈M⁡\(y\)​\[∉Erender\]\\displaystyle\\Rightarrow c\\in M\(y\)\\ \\text\{\[$\\notin E\_\{\\mathrm\{render\}\}$\]\}⇒c∈AuthP0​\(z\)​\[∉Emask\]\\displaystyle\\Rightarrow c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\\ \\text\{\[$\\notin E\_\{\\mathrm\{mask\}\}$\]\}⇒z​truthful,c∈AuthP0​\(z\),fx⋆​\(c,ωx\)=0\\displaystyle\\Rightarrow z\\text\{ truthful\},\\ c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\),\\ f^\{\\star\}\_\{x\}\(c,\\omega\_\{x\}\)=0\[∉Eres\\notin E\_\{\\mathrm\{res\}\}; T4\]⇒the episode lies in​Eprog\.\\displaystyle\\Rightarrow\\text\{the episode lies in \}E\_\{\\mathrm\{prog\}\}\.HenceEuser⊆Eprog∪Eres∪Emask∪ErenderE\_\{\\mathrm\{user\}\}\\subseteq E\_\{\\mathrm\{prog\}\}\\cup E\_\{\\mathrm\{res\}\}\\cup E\_\{\\mathrm\{mask\}\}\\cup E\_\{\\mathrm\{render\}\}, the union bound gives \([5](https://arxiv.org/html/2610.22426#S4.E5)\), and parts \(ii\) and \(iii\) of Theorem[4\.1](https://arxiv.org/html/2610.22426#S4.Thmtheorem1)make the last two terms zero\. On the complement ofEresE\_\{\\mathrm\{res\}\}, every admitted value agrees withωx\\omega\_\{x\}, so no atom becomes conflicting, and because T4, the faithful\-ledger assumption of Appendix[A](https://arxiv.org/html/2610.22426#A1), makes the ledger record exactly the admitted values, every settled atom of the final ledger agrees withωx\\omega\_\{x\}\. ∎

#### Premises of Theorem[4\.3](https://arxiv.org/html/2610.22426#S4.Thmtheorem3)\.

The conclusions form a chain andΦx\\Phi\_\{x\}is empty\. The program is correct in the sense of Section[2](https://arxiv.org/html/2610.22426#S2)\. Checks fall into*call classes*: one call of a class settles every atom of the class, and it returns their values underωx\\omega\_\{x\}\(exact resolvers, known fields\)\. Hence every ledger in the episode is truthful and has no conflicts\. Completion \(line[13](https://arxiv.org/html/2610.22426#alg1.l13)of Algorithm[1](https://arxiv.org/html/2610.22426#alg1)\) repeats the following step whileμ=1\\mu=1andb\>0b\>0: check an atom ofR⁡\(p⋆,z\)R\(p^\{\\star\},z\), charge one call, and recompute\(c⋆,p⋆\)\(c^\{\\star\},p^\{\\star\}\)andμ\\mu\.N⁡\(z\)N\(z\)is the number of call classes that contain an atom ofE†E^\{\\dagger\}that is unknown atzz\.

###### Proof of Theorem[4\.3](https://arxiv.org/html/2610.22426#S4.Thmtheorem3)\.

Writeωx⊧p\\omega\_\{x\}\\models pwhen every literal ofppis true underωx\\omega\_\{x\}\. Truthfulness givesz⊧p⇒ωx⊧pz\\models p\\Rightarrow\\omega\_\{x\}\\models p, and it also gives that a route withωx⊧p\\omega\_\{x\}\\models pis live at every ledger\.

*Step 1 \(nothing abovec†c^\{\\dagger\}is ever authorized\)\.*For a truthfulzz,

c∈AuthP0​\(z\)\\displaystyle c\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)⇒∃d⪰c,p∈P0​\(d\):z⊧p\\displaystyle\\Rightarrow\\exists d\\succeq c,\\ p\\in P\_\{0\}\(d\):\\ z\\models p⇒ωx⊧p​\[truthful\]\\displaystyle\\Rightarrow\\omega\_\{x\}\\models p\\ \\text\{\[truthful\]\}⇒fx⋆​\(d,ωx\)=1​\[correctP0\]\\displaystyle\\Rightarrow f^\{\\star\}\_\{x\}\(d,\\omega\_\{x\}\)=1\\ \\text\{\[correct $P\_\{0\}$\]\}⇒c⪯d⪯c†​\[definition ofc†\]\.\\displaystyle\\Rightarrow c\\preceq d\\preceq c^\{\\dagger\}\\ \\text\{\[definition of $c^\{\\dagger\}$\]\}\.Ifc†=⊥c^\{\\dagger\}=\\bot, thenAuthP0​\(z\)=∅\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)=\\varnothingat every ledger, PRIME abstains, and the claim holds\. From here on,c†≠⊥c^\{\\dagger\}\\neq\\bot\.

*Step 2 \(a true route ofc†c^\{\\dagger\}\)\.*By correctness,fx⋆​\(c†,ωx\)=1f^\{\\star\}\_\{x\}\(c^\{\\dagger\},\\omega\_\{x\}\)=1givesd⪰c†d\\succeq c^\{\\dagger\}andp†∈P0​\(d\)p^\{\\dagger\}\\in P\_\{0\}\(d\)withωx⊧p†\\omega\_\{x\}\\models p^\{\\dagger\}\. Thenfx⋆​\(d,ωx\)=1f^\{\\star\}\_\{x\}\(d,\\omega\_\{x\}\)=1, sod⪯c†d\\preceq c^\{\\dagger\}andd=c†d=c^\{\\dagger\}\. Thusp†∈P0​\(c†\)p^\{\\dagger\}\\in P\_\{0\}\(c^\{\\dagger\}\)is live at every ledger, and its atoms lie inE†E^\{\\dagger\}\.

*Step 3 \(invariantb≥N⁡\(z\)b\\geq N\(z\)keeps the target at or abovec†c^\{\\dagger\}\)\.*Ifb≥N⁡\(z\)b\\geq N\(z\), then

κ^​\(p†,z\)≤N⁡\(z\)≤b​\[atoms ofp†⊆E†\]\\displaystyle\\hat\{\\kappa\}\(p^\{\\dagger\},z\)\\leq N\(z\)\\leq b\\ \\text\{\[atoms of $p^\{\\dagger\}\\subseteq E^\{\\dagger\}$\]\}⇒c†∈ℛ⁡\(z,b\)​\[Step 2; Eq\. \([4](https://arxiv.org/html/2610.22426#S3.E4)\)\]\\displaystyle\\Rightarrow c^\{\\dagger\}\\in\\mathcal\{R\}\(z,b\)\\ \\text\{\[Step 2; Eq\.~\\eqref\{eq:target\}\]\}⇒U⁡\(c⋆\)≥U⁡\(c†\)⇒c⋆⪰c†​\[chain\]\.\\displaystyle\\Rightarrow U\(c^\{\\star\}\)\\geq U\(c^\{\\dagger\}\)\\Rightarrow c^\{\\star\}\\succeq c^\{\\dagger\}\\ \\text\{\[chain\]\}\.
*Step 4 \(each completion step preserves the invariant\)\.*Supposeμ=1\\mu=1andb≥N⁡\(z\)b\\geq N\(z\)\. Thenc⋆c^\{\\star\}is strictly stronger than every authorized conclusion, sop⋆p^\{\\star\}is not complete\. It is live, soR⁡\(p⋆,z\)≠∅R\(p^\{\\star\},z\)\\neq\\varnothingand every literal ofR⁡\(p⋆,z\)R\(p^\{\\star\},z\)has an unknown atomee\. Becausep⋆∈P0​\(c⋆\)p^\{\\star\}\\in P\_\{0\}\(c^\{\\star\}\)andc⋆⪰c†c^\{\\star\}\\succeq c^\{\\dagger\}\(Step 3\),e∈E†e\\in E^\{\\dagger\}\. Checkingeesettles its whole class, which contains an unknown atom ofE†E^\{\\dagger\}, soNNfalls by exactly one whilebbfalls by one\. The invariant holds again, and sinceN≥0N\\geq 0falls at each step, completion stops after at mostN⁡\(z\)N\(z\)steps\.

*Step 5 \(the final ledger authorizesc†c^\{\\dagger\}\)\.*Checking ends at a ledgerzzwithb≥N⁡\(z\)b\\geq N\(z\), and by Step 4 the invariant still holds when completion stops\. Completion stops, or is skipped, in one of two cases\. Ifμ=0\\mu=0, some authorizedcchasU⁡\(c\)≥U⁡\(c⋆\)U\(c\)\\geq U\(c^\{\\star\}\), soc⪰c⋆⪰c†c\\succeq c^\{\\star\}\\succeq c^\{\\dagger\}by Step 3, and Step 1 forcesc=c†c=c^\{\\dagger\}\. Ifb=0b=0, thenN⁡\(z\)=0N\(z\)=0, every atom ofp†p^\{\\dagger\}is settled, truthfully, soz⊧p†z\\models p^\{\\dagger\}andc†∈AuthP0​\(z\)c^\{\\dagger\}\\in\\mathrm\{Auth\}\_\{P\_\{0\}\}\(z\)\. In both cases Step 1 givesMaxAuthP0​\(z\)=\{c†\}\\mathrm\{MaxAuth\}\_\{P\_\{0\}\}\(z\)=\\\{c^\{\\dagger\}\\\}, and line[15](https://arxiv.org/html/2610.22426#alg1.l15)reportsc†c^\{\\dagger\}\.

For the corollary: a charged agent request that checks an unknown atom ofE†E^\{\\dagger\}lowersbbandNNby one each, and cached repeats change neither, sob≥N⁡\(z\)b\\geq N\(z\)holds fromB≥N⁡\(z0\)B\\geq N\(z\_\{0\}\)to the end of checking\. ∎

#### Machine check\.

In the tightness example of Section[4](https://arxiv.org/html/2610.22426#S4), each atom is its own call class,c†=c2c^\{\\dagger\}=c\_\{2\}, andE†=\{e1,…,e5\}E^\{\\dagger\}=\\\{e\_\{1\},\\dots,e\_\{5\}\\\}\. Testtest\_completion\_ceiling\.pyin the released runtime checks the theorem against the runtime’s own target computation on 500 random programs with up to six atoms and shared call classes\. For each program, it covers every truth assignment, an arbitrary prefix of agent checks, and budgetsN⁡\(z\)N\(z\),N⁡\(z\)\+1N\(z\)\+1, andN⁡\(z\)\+3N\(z\)\+3, and it records instances whereN⁡\(z\)−1N\(z\)\-1fails\. It also confirms the example’s outcomes at 3, 4, and 5 calls\.

## Appendix CExperimental Setup

This appendix gives the conditions shared by all experiments\. Table[8](https://arxiv.org/html/2610.22426#A3.T8)lists the studies and the exhibits that report them\.

StudyQuestionTasks or recordsAgents and policiesWhat variesExhibitsInformation vs\. enforcement \(§[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)\)Does an agent shown the requirements and its ledger follow them?Balanced split, 480 tasksQwen2\.5\-32B\-Instruct; three other modelsInformation in the prompt; authorization gateTable[2](https://arxiv.org/html/2610.22426#S7.T2); Figure[3](https://arxiv.org/html/2610.22426#A5.F3); Table[3](https://arxiv.org/html/2610.22426#S7.T3)Guidance \(§[7\.2](https://arxiv.org/html/2610.22426#S7.SS2)\)Does guidance recover the conclusions that enforcement alone misses?Balanced splitQwen2\.5\-32B\-Instruct; scripted policiesGuidance, completion, budgetFigure[2](https://arxiv.org/html/2610.22426#S7.F2), left; Figures[4](https://arxiv.org/html/2610.22426#A5.F4)and[5](https://arxiv.org/html/2610.22426#A5.F5)Evidence location \(§[7\.2](https://arxiv.org/html/2610.22426#S7.SS2)\)Does the agent’s choice of field beat fixed\-order checking?Locator\-uncertain copyQwen2\.5\-32B\-Instruct, gpt\-oss\-20b, Mistral\-Small\-24B; scripted policiesField choice, completion, budgetFigure[2](https://arxiv.org/html/2610.22426#S7.F2), right; Table[11](https://arxiv.org/html/2610.22426#A5.T11)Text judgments \(§[7\.3](https://arxiv.org/html/2610.22426#S7.SS3)\)What happens when the model judges text?Text\-evidence split, 240 tasksQwen2\.5\-32B\-InstructGuidance; verification of attestationsTable[4](https://arxiv.org/html/2610.22426#S7.T4)Closest systems \(§[7\.4](https://arxiv.org/html/2610.22426#S7.SS4)\)What does PRIME add over the closest systems given the same requirements?Balanced split; locator\-uncertain copyAgentSpec, ResearchLoop, Proof\-or\-Stop, HESP, GLEAN; Qwen2\.5\-32B\-InstructSystem; budgetTable[5](https://arxiv.org/html/2610.22426#S7.T5); Tables[12](https://arxiv.org/html/2610.22426#A5.T12)and[13](https://arxiv.org/html/2610.22426#A5.T13)Regulation \(App\.[F](https://arxiv.org/html/2610.22426#A6)\)Can PRIME execute requirements generated from a published regulation?1,999 held\-out registrations; 600 for agentsTwo generated programs; ceiling\-targeting policy; Qwen2\.5\-32B\-Instruct agentsConstruction workflow; policyTables[14](https://arxiv.org/html/2610.22426#A6.T14)to[16](https://arxiv.org/html/2610.22426#A6.T16)Pilot \(exploratory\)How did enforcement behave on earlier hand\-built tasks?60 hand\-built tasksgpt\-4\.1, gpt\-4o\-mini; Qwen2\.5\-7B and 32B for testsEnforcement; static checklistTable[17](https://arxiv.org/html/2610.22426#A6.T17)Table 8:Study overview for Section[7](https://arxiv.org/html/2610.22426#S7)and Appendices[F](https://arxiv.org/html/2610.22426#A6)–[G](https://arxiv.org/html/2610.22426#A7)\. Pilot results are not pooled\.AtomFieldPredicateValuee1e\_\{1\}detailsexiststruee2e\_\{2\}database\_specific\.equalsTrue\-altfalsegithub\_reviewede3e\_\{3\}database\_specific\.severityexiststruee4e\_\{4\}references\.0\.typeequalsADVISORY\-altfalsee5e\_\{5\}references\.0\.urlexiststruee6e\_\{6\}database\_specific\.cwe\_ids\.0existstruee7e\_\{7\}database\_specific\.existstruegithub\_reviewede8e\_\{8\}affected\.0\.package\.ecosystemequals “PyPI”trueTable 9:Routes toc1c\_\{1\},c2c\_\{2\}, andc3c\_\{3\}are\{e1\}\\\{e\_\{1\}\\\},\{e1,e2,e3\}\\\{e\_\{1\},e\_\{2\},e\_\{3\}\\\}or\{e1,e4,e5\}\\\{e\_\{1\},e\_\{4\},e\_\{5\}\\\}, and\{e1,e2,e3,e6,e7\}\\\{e\_\{1\},e\_\{2\},e\_\{3\},e\_\{6\},e\_\{7\}\\\}, respectively\. Constructed failures ate2e\_\{2\}ande4e\_\{4\}leavec1c\_\{1\}strongest\.AgentWhat it sees or doesEnforcedGuidedReActthe request, scope, conclusions, and tools\([Yao et al\., 2023](https://arxiv.org/html/2610.22426#bib.bib39)\)nono\+verifyplus an instruction to verify before concludingnono\+specReAct plus the specification view: each atom and the field it readsnono\+spec\+verifybothnono\+program\+spec plus the committed routesnono\+program\+verifybothnonoFully informed agent\+program\+verify plus a live display of its own ledgernonoPRIME without guidancethe same prompt plus the authorized conclusions; others are refusedyesnoPRIMEplus the strongest reachable conclusion, its open atoms, and remindersyesyesTable 10:Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)information ladder\. Agents share model, tools, budget, and scorer\.#### Records and splits\.

The records were retrieved on 1 August 2026\. GitHub Advisory Database records, which OSV serves, are licensed under CC BY 4\.0 and are redistributed with attribution\. Records from openFDA are in the public domain, and ClinicalTrials\.gov and EDGAR records are public U\.S\. government information\. The sources are OSV \([https://osv\.dev](https://osv.dev/)\), ClinicalTrials\.gov \([https://clinicaltrials\.gov](https://clinicaltrials.gov/)\), openFDA \([https://open\.fda\.gov](https://open.fda.gov/)\), and SEC EDGAR \([https://www\.sec\.gov/edgar](https://www.sec.gov/edgar)\), and the records and task texts are in English\. Some advisory texts contain personal details, such as a reporter’s or vendor’s contact e\-mail address\. No atom tests such personal details, and the records are kept as published\. The SUFFICE data are released under CC BY 4\.0, with each embedded record under its source’s terms, and the code under the MIT License\. The held\-out splits share 60 families, and development \(192 tasks, 48 families\) and validation \(48 tasks, 12 families\) use the other 60\. An LLM coding assistant working with the authors drafted the families’ candidate record fields and conclusion sentences in code\. Task instances were then generated and verified mechanically\. The reference judgmentfx⋆f^\{\\star\}\_\{x\}evaluates the authored standard on the stored atom values, never reads an agent’s routes or ledger, and scores every agent identically\. The balanced split is built so that unsupported conclusions are possible\. In 199 of its 480 tasks \(41\.5%\), an atom on a route has a requirement the record does not meet\. These tasks contain 233 such atoms, of which 104 require a value taken from another record, 55 a numeric threshold the record cannot meet, 23 a date a year earlier than the record’s, and 51 a synthetic value outside the field’s valid values, such asTrue\-altfor a Boolean review flag orADVISORY\-altfor a reference type\. In 129 tasks the evidence for some atom is unavailable \(146 atoms\)\. Rates on the balanced split therefore describe agent behavior under this mix, not how often unsupported conclusions arise in practice\. The benchmark leavesΦx\\Phi\_\{x\}empty even where two atoms read the same field\. The locator\-uncertain copy keeps every task and answer of the balanced split but withholds each atom’s field\. Instead, the atom describes what it must read and lists three candidate fields, the true one among them\. The text\-evidence split has 240 clinical and security tasks, and Appendix[E\.4](https://arxiv.org/html/2610.22426#A5.SS4)gives its construction\. The released corpus has 1,898 task files, the 938 tasks plus the 480 locator\-uncertain copies, the 240 text\-evidence tasks, and a 240\-task one\-branch split that this paper does not analyze\.

#### The running example\.

The security example in Sections[1](https://arxiv.org/html/2610.22426#S1)to[3](https://arxiv.org/html/2610.22426#S3)and Figure[1](https://arxiv.org/html/2610.22426#S3.F1)is hypothetical\. It illustrates the route structure of tasksec\-v2\-0114, generated from OSV advisoryGHSA\-5pqf\-rvm7\-3wgw, not that advisory’s review status\. The task’s conclusion sentences are “The advisory identifies an affected package with a readable summary” \(c1c\_\{1\}\), “The advisory is triage\-ready: affected package identified, summary present, and its review/severity metadata are populated” \(c2c\_\{2\}\), and “The advisory satisfies the checked currency\-and\-completeness protocol” \(c3c\_\{3\}\), and the illustrated acceptance decision corresponds toc2c\_\{2\}\. Table[9](https://arxiv.org/html/2610.22426#A3.T9)gives the actual atoms and routes\. Atome1e\_\{1\}reads the record’sdetailsfield, although the conclusion sentences call it a summary\. Atome2e\_\{2\}requires the advisory’s GitHub curator\-review flag to equal the altered valueTrue\-alt, which no record can have, although this advisory’s flag istrue\. Atome4e\_\{4\}likewise requires the first reference’s type to equalADVISORY\-alt, although that reference is typedADVISORY\. These are constructed requirement failures, not evidence that the advisory was unreviewed or that its reference is not a published advisory\. The other atoms test that the severity \(e3e\_\{3\}\) and the first reference’s URL \(e5e\_\{5\}\) exist, the presence of a weakness identifier \(e6e\_\{6\}\) and of the review flag \(e7e\_\{7\}\), and whether the ecosystem is PyPI \(e8e\_\{8\}\), which lies on no route\. In this task the commitment procedure sees each atom’s tool, parameters, and field but never its value or the routes\.

#### Agents and models\.

Confirmatory runs serve Qwen2\.5\-32B\-Instruct\([Qwen Team, 2024](https://arxiv.org/html/2610.22426#bib.bib20)\)with vLLM\([Kwon et al\., 2023](https://arxiv.org/html/2610.22426#bib.bib13)\)at temperature zero, one run per task\. The checkpoints areQwen/Qwen2\.5\-32B\-Instruct,Qwen/Qwen2\.5\-7B\-Instruct,openai/gpt\-oss\-20b\([OpenAI, 2025](https://arxiv.org/html/2610.22426#bib.bib18)\), andmistralai/Mistral\-Small\-24B\-Instruct\-2501\([Mistral AI, 2025](https://arxiv.org/html/2610.22426#bib.bib16)\), all under the Apache 2\.0 license, served by vLLM 0\.24\.0 \(0\.10\.1 for part of the Mistral\-Small\-24B runs\) with a 16,384\-token context\. Qwen2\.5\-32B\-Instruct ran on two A100 GPUs for the registered comparisons and on one or two A100 80GB, H100, H200, or RTX Pro Blackwell GPUs for the later experiments\. The runs behind the reported results used about 90 GPU\-hours, and the development\-split runs that set the minimum effect for guidance used about 20 more\. Table[10](https://arxiv.org/html/2610.22426#A3.T10)lists what each agent of Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)sees\. PRIME without guidance adds the*mask*, the authorization gate of Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1), which refuses conclusions the recorded checks do not authorize\. The fully informed agent and PRIME without guidance receive identical prompts except for the list of authorized conclusions, which a regression test verifies\. The experiments of Sections[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)and[7\.2](https://arxiv.org/html/2610.22426#S7.SS2)were repeated with gpt\-oss\-20b, served on H200 GPUs, and with Mistral\-Small\-24B, served on H100 and A100 80GB GPUs\. The enforcement and guidance comparisons were also repeated with Qwen2\.5\-7B, served on one A100 GPU\. The text\-judgment experiment and the agent runs of the regulatory evaluation used Qwen2\.5\-32B\-Instruct only\. vLLM’s Mistral tool\-call parser was wrapped to accept a single JSON object where it expects a list \(in a diagnostic cell, 29 of 529 requests\) and to return as text the few outputs that name a nonexistent tool or fabricate a tool result \(19 of 529\); well\-formed outputs are unaffected\. An episode whose model calls still failed after the client’s retries carries no measurement and is left out of the rates, which are therefore taken over completed episodes; this removed at most four episodes from any reported cell \(eight of the 4,320 episodes of Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)\), and the released code lists each one\.

#### Budgets, stopping, and resolvers\.

Budgets count tool calls, and one call can settle several atoms, as in the running example\. Every request costs one call except as follows\. Only the first request of each model turn is executed, and the others are ignored at no cost\. A request that repeats an executed request, with the same tool and arguments and, for an attestation, the same read status of its source text, is answered from a cache at no cost\. An unrecognized request is refused and charged, and an identical repeat of it is answered from the cache like any other repeat\. Reporting requests are never answered from the cache, so they are always charged, whether accepted, held, or refused\. A turn without a request is free, as are the reminders and the runtime’s final statement\. Since every charge is zero or one call and checking ends when the budget reaches zero, no request is ever unaffordable\. Every reported outcome is the one this charging rule produces\. If an unenforced agent stops without stating a conclusion, it is asked once, at no cost, which conclusions it asserts, and that answer is scored\. PRIME’s runtime instead states the strongest authorized conclusion\. Field atoms are decided by deterministic resolvers that evaluate a predicate on one field of the task’s embedded record\. Four scripted policies choose their checks by code but use the same resolvers, ledger, and final statement as PRIME\. At every step, the*ceiling\-targeting*policy takes, among the live routes of all conclusions, the one whose open atoms need the fewest distinct calls, with ties going to the stronger conclusion, and checks the first of those atoms by identifier\. It continues until no live route has an open atom or the budget is spent, so it does not stop when a conclusion becomes authorized\. The*random\-order*policy \(random check in Figure[2](https://arxiv.org/html/2610.22426#S7.F2)\) checks a random open atom of a live route\. On the locator\-uncertain copy,*blind enumeration*makes the ceiling\-targeting policy’s choices but reads an atom’s candidate fields in listed order, one call per attempt, and treats the atom as impossible once the list is exhausted, and the*true\-locator*policy is ceiling\-targeting with the correct fields\. Completion on that copy is*replayed*, that is, applied to PRIME’s logged episodes from the agent’s stopping point without calling the model\. Text atoms are judged by the model, which*attests*them with a value and a quote; Appendix[E\.4](https://arxiv.org/html/2610.22426#A5.SS4)gives the admission rule and the*verified*condition\.

#### Endpoints\.

If an episode states several conclusions, false authorization counts it if any is unsupported, and utility takes the strongest supported one\. Both endpoints credit a true conclusion even when the agent did not check it, which favors unenforced agents\. The ladder runs nine agents on 480 tasks at 20 calls \(4,320 episodes\), and the two PRIME agents also run at the three other budgets \(2,880 episodes\)\.

#### Reproducibility and artifacts\.

We provide two public repositories for reproducibility: SUFFICE \([https://github\.com/HamedKhosravi99/SUFFICE](https://github.com/HamedKhosravi99/SUFFICE)\) and PRIME \([https://github\.com/HamedKhosravi99/PRIME](https://github.com/HamedKhosravi99/PRIME)\), whoselogs/folder holds the archive of every episode log behind the reported numbers\. The SUFFICE repository contains the benchmark generator, task specifications, data splits, executable checks, and scoring procedures\. The PRIME repository contains the review runtime, evidence ledger, authorization gate, guidance and completion procedures, agent configurations, and evaluation scripts\. The 938\-task corpus comprises 480 balanced, 218 natural\-prevalence, 192 development, and 48 validation tasks; locator\-uncertain and text\-evidence variants are evaluated separately\. Released experimental records and analysis scripts support inspection of tool requests, recorded evidence, final conclusions, attestation errors, budget accounting, and reported metrics\. Reproduction instructions are provided in the repository documentation\.

## Appendix DStatistical Protocol

Before any confirmatory episode was scored, we froze the utility function, endpoints, agents, budgets, tests, multiplicity groups, and the minimum effect for guidance\.

#### Unit of inference and tests\.

The family is the unit of inference, because the tasks of one family share their request, conclusions, routes, and atoms\. A contrast is a family\-mean paired difference between two agents on the same tasks, tested by a sign\-flip randomization test and reported with a 95% bootstrap interval\. An exact McNemar test that treats tasks as independent complements each randomization test, and discordant families are those in which the two compared agents differ\. Holm correction applies within three registered groups: the ladder contrasts of Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1), the guidance contrasts of Section[7\.2](https://arxiv.org/html/2610.22426#S7.SS2), and induction\-method contrasts that this paper does not report\.

#### Minimum effect for guidance\.

The minimum effect was set on development tasks with branching routes asδ=max⁡\(5\.0,0\.2​Gdev\)\\delta=\\max\(5\.0,\\,0\.2\\,G\_\{\\mathrm\{dev\}\}\)withGdev=30\.79G\_\{\\mathrm\{dev\}\}=30\.79, the utility gap between PRIME without guidance and an informed route planner \(an LLM\-free policy that knows which routes hold but still pays for their checks\), givingδ=6\.16\\delta=6\.16\. The power of an equivalence test at zero effect was 0\.708, below the registered 0\.8, so, as decided in advance, no equivalence conclusion is drawn\.

#### Confirmatory and secondary analyses\.

The registered confirmatory analysis consists of the ladder and guidance contrasts on the balanced split, with Qwen2\.5\-32B\-Instruct as the primary model and Qwen2\.5\-7B as a secondary one\. All other analyses are secondary: the premature\-conclusion rate, added after the confirmatory results as a descriptive endpoint computed from fields logged in every episode; the other models and sampled decoding; the locator\-uncertain and text\-evidence splits, including the verified\-attestation run; the flat gate and the after\-the\-fact filter; and the regulatory evaluation\. No registered test depends on them, and their intervals and tests are not corrected for multiplicity\.

#### Deviations\.

Five deviations were logged with dates and reasons; three concern the analyses reported here: \(1\) confirmatory runs were queued behind the development pilot, with no confirmatory result computed before the minimum effect was frozen; \(2\) an emission\-rate column and a flag for agents answering under 25% of answerable tasks were added after the first 7B results, before any 32B confirmatory data; and \(3\) a default width limit in the route compiler was made optional after a round\-trip test showed that 189 authored routes are seven atoms wide, and the test reproduces all 1,440 authored conclusions on all 74,784 realizable states\. The other two concern analyses this paper omits: the registered induction\-method contrasts and a descriptive failure\-mode table\. The registered four\-agent natural\-prevalence set is also not reported\.

## Appendix EAdditional Results

This appendix adds evidence for each experiment, in the order of Section[7](https://arxiv.org/html/2610.22426#S7)\. Differences reported with a confidence interval are family\-mean paired differences \(Appendix[D](https://arxiv.org/html/2610.22426#A4)\), so they can differ from differences between the pooled values in the tables\.

### E\.1The full information ladder and other models

Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)reports selected rungs of the ladder\. Of the information steps, only the ledger display changed false authorization significantly, adding 4\.8 points with a 95% confidence interval \(CI\) of \[1\.2, 8\.6\], and the mask removed 28\.0 points \(95% CI \[22\.7, 33\.5\]\)\. Here we show every step and test whether the enforcement result depends on the model or on greedy decoding\.

Figure 3:Information ladder on 480 tasks at 20 calls\. Top shows false authorization and bottom supported utility\. Annotations are family\-mean paired differences with 95% intervals\.Every Qwen2\.5\-32B\-Instruct agent without the mask stated unsupported conclusions, and the mask removed them for every model and decoding setting tested\.Figure[3](https://arxiv.org/html/2610.22426#A5.F3)shows all nine agents, including the \+spec and \+program steps without the verification instruction\. From \+verify to the fully informed agent, false authorization stayed between 19\.9% and 26\.7% while utility rose from 10\.0 to 38\.0, and the mask is the only step that brings false authorization to zero\. Information raised both quantities because the agent found more fields and stated a conclusion in more episodes: Table[2](https://arxiv.org/html/2610.22426#S7.T2)shows emission rising from 59\.0% for ReAct to 99\.0% for the fully informed agent, and each additional statement is another occasion to overclaim\.

Table[3](https://arxiv.org/html/2610.22426#S7.T3)in Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)gives the other models\. For gpt\-oss\-20b and Mistral\-Small\-24B, the mask cost family\-mean utility of 2\.5 \(95% CI \[0\.9, 4\.2\]\) and 5\.6 \(\[3\.1, 8\.1\]\) relative to the fully informed agent\. On the security domain alone, it removed 31\.8 points of false authorization for Qwen2\.5\-32B\. The sampled\-decoding runs of Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)use temperature 0\.7 and three seeds\. These settings change how the agent behaves but not the check the mask applies, which is why the enforced rate is zero in every run while the unenforced rate varies with how often the agent states a conclusion\.

### E\.2Registered guidance cells and alternatives to guidance

Section[7\.2](https://arxiv.org/html/2610.22426#S7.SS2)reports the guidance gain over all tasks at 20 calls\. Under the mask alone, utility fell from the fully informed agent’s 38\.0 to 30\.1 \(family\-mean cost 7\.4, 95% CI \[4\.5, 10\.3\]\), and guidance raised it to 45\.5 \(gain 15\.6, 95% CI \[12\.5, 18\.6\]\)\. This comparison adds the gate and also puts the list of authorized conclusions in the prompt, so its utility change reflects both\. At 20 calls, the runtime’s final statement supplied 35\.0 of PRIME’s 45\.5 points, and completion added 0\.5 to 0\.9 calls per episode\. The registered analysis tested the gain separately at each of the four budgets on nested and branching tasks, against the minimum effect of 6\.16 points that the registered protocol of Appendix[D](https://arxiv.org/html/2610.22426#A4)fixed before scoring\.

Figure 4:Guidance gains by budget and route structure \(480 tasks\)\. Points show family\-mean paired utility differences with 95% intervals\. Dashed line marks the minimum effect of 6\.16\.Guidance raised utility by more than the minimum effect in all eight registered Qwen2\.5\-32B\-Instruct cells\.Figure[4](https://arxiv.org/html/2610.22426#A5.F4)shows that the family\-mean gain of PRIME over PRIME without guidance fell with the budget, from 24\.0 \[19\.6, 28\.5\] atbminb\_\{\\min\}to 16\.2 \[12\.3, 20\.2\] at 20 calls on branching tasks and from 20\.9 \[16\.7, 25\.3\] to 14\.4 \[10\.1, 18\.6\] on nested ones; even the lowest interval bound, 10\.1, lies above 6\.16\. For Qwen2\.5\-7B, the registered secondary model, the eight gains were 0\.6 to 3\.1 points, every 95% interval ended below 6\.16, and every interval on nested tasks included zero\. The gain falls with the budget because the guided agent stops sooner when it may call more, whereas the agent without guidance stops at its first permitted conclusion at every budget\. Branching tasks, where a failed check can leave a second route to a stronger conclusion, gained more at every budget\. The scripted references depend on the budget in the same way: the random\-order policy scored 46\.5 atbminb\_\{\\min\}and matched the ceiling\-targeting policy’s 59\.2 from2​bmin2b\_\{\\min\}, so the order of checks matters only when the budget is tight\.

#### An ideal after\-the\-fact filter\.

A common alternative to enforcement during the episode is to let the agent answer freely, reject an unsupported answer afterward, and let the agent try again\. With a perfect checker and unlimited retries, such a filter can at best state the strongest conclusion that the evidence the agent gathered supports, because retrying changes what the agent says, not what it checked\. We computed this bound from the fully informed agent’s logged episodes\.

Figure 5:Utility on 480 tasks at 20 calls, comparing direct answering, unguided PRIME, the ideal filter on the fully informed agent’s evidence, PRIME, and scripted ceiling targeting\.Even this ideal filter fell short of PRIME, because a filter cannot change which evidence is gathered\.Figure[5](https://arxiv.org/html/2610.22426#A5.F5)shows that the filter reached 43\.5, against 45\.5 for PRIME and 59\.2 for the ceiling\-targeting policy; answering without evidence scores 30\.3, and PRIME without guidance 30\.1\. The mask alone falls below the ideal filter because refusing a conclusion leaves the agent with its first permitted answer, whereas the filter credits the strongest conclusion the agent’s evidence supports\. Guidance reverses the comparison because it acts while checks can still be made\.

#### A gate on a single conclusion\.

PRIME orders conclusions by strength, so partial evidence can still earn a weaker conclusion\. To test whether this order matters, the*flat gate*keeps the prompt of PRIME without guidance but exposes only the strongest conclusion and admits it once a route to it is established; otherwise the agent abstains\. It has no graded conclusions, no guidance, and no completion\.

Without graded conclusions, the gate stated nothing unsupported but lost most of the useful output\.On the 480 balanced tasks at 20 calls, the flat gate reached utility 8\.1 and stated a conclusion on 9\.8% of answerable tasks, against 30\.1 for PRIME without guidance and 45\.5 for PRIME \(PRIME’s gain 37\.3, 95% CI \[32\.6, 42\.0\], 60 of 60 families\)\. The runtime refused 364 emission attempts, each either the conclusion before its route was established or a weaker one, and the agent stated the conclusion on 39 tasks\. On the 152 tasks whose strongest conclusion is supported, the gate reached 25\.7, against 38\.8 for PRIME without guidance and 65\.8 for PRIME; on the other 328 it can score nothing by construction, where the graded agents score 26\.1 and 36\.1\. The order lets partial evidence earn a weaker conclusion, and guidance carries the agent from there to a stronger one\.

### E\.3Field choice and other models

The evidence\-location results of Section[7\.2](https://arxiv.org/html/2610.22426#S7.SS2)measured the benefit of the agent’s choice of field with one model, and the guidance results showed that the agent’s stopping limits what guidance can add\. Both behaviors belong to the model, so we repeated the experiments of Sections[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)and[7\.2](https://arxiv.org/html/2610.22426#S7.SS2)with gpt\-oss\-20b and Mistral\-Small\-24B in all four domains\.

FA \(%\)Utility, balanced splitGuidance gainLocator split,bminb\_\{\\min\}ModelAgentat 20bminb\_\{\\min\}2​bmin2b\_\{\\min\}20atbminb\_\{\\min\}\[95% CI\]Utilityvs\. blind \[95% CI\]Qwen2\.5\-32BFully informed agent26\.738\.138\.638\.037\.2−\-2\.0 \[−\-4\.7, 0\.8\]PRIME without guidance0\.030\.130\.130\.122\.0−\-16\.5 \[−\-19\.9,−\-13\.1\]PRIME0\.052\.647\.345\.523\.0 \[19\.5, 26\.3\]51\.512\.5 \[8\.9, 16\.3\]PRIME with completion0\.058\.859\.259\.253\.714\.7 \[11\.5, 18\.0\]gpt\-oss\-20bFully informed agent17\.730\.630\.530\.531\.5−\-7\.5 \[−\-9\.7,−\-5\.2\]PRIME without guidance0\.026\.926\.926\.925\.7−\-12\.8 \[−\-15\.3,−\-10\.2\]PRIME0\.055\.758\.858\.528\.8 \[25\.7, 31\.9\]52\.614\.2 \[11\.1, 17\.7\]PRIME with completion0\.056\.158\.658\.652\.213\.8 \[10\.7, 17\.2\]Mistral\-Small\-24BFully informed agent19\.434\.434\.435\.232\.3−\-6\.4 \[−\-9\.1,−\-3\.8\]PRIME without guidance0\.029\.329\.229\.325\.4−\-13\.4 \[−\-16\.0,−\-10\.9\]PRIME0\.037\.936\.736\.610\.3 \[7\.3, 13\.3\]33\.6−\-4\.7 \[−\-7\.8,−\-1\.6\]PRIME with completion0\.055\.859\.159\.142\.62\.8 \[0\.7, 4\.9\]Table 11:Three\-model results on balanced and locator\-uncertain splits\. FA is measured at 20 calls and utility at three budgets\. Differences are family\-mean contrasts, with blind enumeration as the locator baseline \(40\.3\)\. Locator completion is live, unlike the Qwen replay \(53\.6\)\. The guidance gain is defined only for PRIME\.Guidance helped every model, but only some models chose fields better than fixed\-order checking\.Table[11](https://arxiv.org/html/2610.22426#A5.T11)shows that guidance raised utility atbminb\_\{\\min\}over the mask alone by 28\.8 points \(95% CI \[25\.7, 31\.9\]\) for gpt\-oss\-20b and by 10\.3 \(\[7\.3, 13\.3\]\) for Mistral\-Small\-24B\. On the locator\-uncertain copy, gpt\-oss\-20b’s choice among the candidate fields beat blind enumeration by 14\.2 \(\[11\.1, 17\.7\]\) atbminb\_\{\\min\}, as Qwen2\.5\-32B\-Instruct’s did, but Mistral\-Small\-24B’s fell 4\.7 \(\[−\-7\.8,−\-1\.6\]\) short of it\. For Qwen2\.5\-32B\-Instruct, PRIME’s advantage over blind enumeration atbminb\_\{\\min\}\(family\-mean difference 12\.5, 95% CI \[8\.9, 16\.3\]\) held in 56 of the 60 families; the mask alone, with the same candidates but no guidance, reached 22\.0, and PRIME’s gain over it was 29\.0 \(95% CI \[25\.5, 32\.6\]\)\.

Two behaviors of the model explain these differences\. On the balanced split, Mistral\-Small\-24B’s agent stopped after fewer calls \(2\.9 atbminb\_\{\\min\}, against 4\.2 for gpt\-oss\-20b and 3\.4 for Qwen2\.5\-32B\-Instruct\) and stated no conclusion in most episodes, so the runtime’s statement at the stopping point carried most of its utility and guidance had less to add\. On the locator\-uncertain copy, it also chose fields less accurately\. Its first read hit the correct field for 44\.5% of atoms, against 71\.2% for Qwen2\.5\-32B\-Instruct and 81\.0% for gpt\-oss\-20b \(33% for a first try in listed order\), and 29\.2% of its reads went to wrong candidates, against 14\.7% and 10\.6%\. Completion compensates for both early stopping and poor field choices\. On the balanced split, it matched the ceiling\-targeting value at2​bmin2b\_\{\\min\}and 20 calls for Mistral\-Small\-24B and came within 0\.6 points of it for gpt\-oss\-20b\. Atbminb\_\{\\min\}it stayed below by family\-mean differences of 2\.4 points for gpt\-oss\-20b and 4\.0 for Mistral\-Small\-24B\. On the locator\-uncertain copy, completion tries the candidates the agent has not read, and with it Mistral\-Small\-24B finished 2\.8 points \(\[0\.7, 4\.9\]\) above blind enumeration\. The benefit of letting the model choose where to look is therefore a property of the model, and completion limits the cost of a poor choice\. A live run of completion with Qwen2\.5\-32B\-Instruct atbminb\_\{\\min\}scored 53\.7, within 0\.1 of the replayed 53\.6, and Table[11](https://arxiv.org/html/2610.22426#A5.T11)reports live runs for all three models\.

### E\.4Text judgments and verification

Each task of the text\-evidence split has one field atom \(that the title or summary is present\) and three text atoms\. For clinical registrations, the source is the eligibility\-criteria text, and the text atoms are that enrollment is restricted to adults \(minimum age 18 years or more\), that it is restricted to one sex, and that healthy volunteers are accepted;c2c\_\{2\}requires the first, andc3c\_\{3\}the first true and the other two false\. For security advisories, the source is the advisory’s details text, and the text atoms are that it names the affected package \(by its registered name or a distinctive part of it, not only the vendor or ecosystem\), that it states a version in which the issue is fixed, and that it states the first\-affected version;c2c\_\{2\}requires the first, andc3c\_\{3\}all three\. Each atom’s truth is computed from a structured field that the embedded record omits \(minimum age, sex, and healthy\-volunteer flag; the registered package name and the fixed and first\-affected versions of the advisory’s range data, the name counting as present when it or one of its distinctive tokens occurs in the text\), so a task violates an atom whenever the registry does; records without the structured field \(no fixed version, every version affected\) are not used\. The agent reads the text withread\_textand attests withattest\_atom\. The runtime admits an attestation only for a text\-evidence atom when the text was read in the episode and the quote is a verbatim span of at least eight characters\. Otherwise, it rejects the call and leaves the atom open\.

#### Rejected and wrong attestations\.

The runtime rejected 15 of 225 attestation calls for the fully informed agent, 65 of 216 for PRIME without guidance, and 72 of 370 for PRIME\. All 72 PRIME rejections involved nonverbatim quotations\. Of the other 80 rejections, 14 involved nonverbatim quotations and 66 attempted attestations on non\-text atoms\. No call was rejected for an unread source\. Rejected calls never enter the ledger\. Among admitted attestations, wrong values ran in both directions\. Under PRIME, adults\-only enrollment was judged false for 5 registrations whose minimum age is 18 or more and true for 6 whose minimum age is lower\. The one\-sex and healthy\-volunteer conditions were judged false for 5 whose structured fields hold them\. In the advisories, the package, fixed version, or first\-affected version was judged named for 11 whose text does not contain it and absent for 3 whose text does\. Each unsupported conclusion PRIME stated was authorized by a route containing a wrongly attested atom, while two of the fully informed agent’s unsupported conclusions were statements its ledger did not support\. Because each domain is one family, contrasts on this split are at the record level\. Against the mask alone, PRIME changed utility by\+10\.1\+10\.1\[7\.8, 12\.6\] and false authorization by\+2\.9\+2\.9\[0\.8, 5\.4\] \(7 of 240 tasks, exact McNemarp=0\.016p=0\.016\), and against the fully informed agent by−1\.0\-1\.0\[−3\.5\-3\.5, 1\.5\] and\+0\.4\+0\.4\[−1\.7\-1\.7, 2\.5\]\.

#### Verification\.

The verified condition tests whether screening attestations before admission removes these errors, and at what cost\. Before an attestation that passes the runtime’s checks enters the ledger, the same model is asked once more, in a fresh context that contains only the atom’s condition and the source text \(not the agent’s value, quote, or conversation\), whether the text establishes the condition\. The attestation is admitted only if the answer equals the agent’s value; otherwise the atom stays open, and the agent is told only that an independent check did not confirm it\. The prompt and rule were frozen before the run\. The arm, budget, model, and serving stack are those of the PRIME run in Table[4](https://arxiv.org/html/2610.22426#S7.T4), and the comparison is with that run\.

Screening removed most wrong judgments before they reached the ledger, at the cost of refusing many correct ones\.The last row of Table[4](https://arxiv.org/html/2610.22426#S7.T4)shows that false authorization fell from 4\.6% to 0\.8% \(2 of 240 tasks, 95% CI \[0\.2, 3\.0\]\) and that 6 of the 222 admitted attestations were wrong \(2\.7%, against 30 of 298\), while supported utility fell from 57\.5 to 55\.1 \(paired loss 2\.4 \[0\.3, 4\.3\]\)\. Emission was 100% in both runs\. The verifier refused 65 attestations in 59 episodes, 46 with values that match the benchmark reference and 19 with wrong values\. It refused all 12 wrong attestations in clinical registrations but 7 of the 13 in security advisories, and it refused right attestations of all three text atoms\. After a refusal, every episode still ended with the runtime stating the strongest authorized conclusion, never with abstention\. The final conclusion was lower than in the PRIME run of Table[4](https://arxiv.org/html/2610.22426#S7.T4)on 43 tasks and higher on 6 \(32 and 0 of them in the 59 episodes with a refusal\), and the refusals prevented 8 of the 11 unsupported conclusions of that run\. A ninth did not recur either, although its episode had no refusal\. Verification added 1\.2 model calls and 3\.6% more tokens per episode on average\. These calls fall outside the 20\-call evidence\-tool budget, which is therefore not a matched total compute budget\.

The two remaining unsupported conclusions, the same in both runs, involve product mentions in advisory text \(“AWS API MCP Server”; “Zope … Plone”\) that differ from the structured registry identifiers\. The text\-evidence score therefore measures agreement with the benchmark’s structured reference for short, specified conditions read from individual fields; the released logs keep the passages for case\-level inspection\. Code, traces, and the frozen prompt are inexperiments/blind\_verification/of the released code\.

### E\.5The closest systems

Section[7\.4](https://arxiv.org/html/2610.22426#S7.SS4)runs five of the systems discussed in Appendix[H](https://arxiv.org/html/2610.22426#A8)on the 480 balanced tasks\. Every system receives the same task prompt, the same requirement content \(the committed program’s conclusions, their order, and each conclusion’s routes over checks, with each check’s tool and field\), and the same evidence: check values come from the same deterministic resolvers applied to the same tool observations\. Each system receives the requirements in its own specification format, compiled mechanically from the program, and keeps its own control: what decides the next check, when to stop, and which conclusion is reported\. All use Qwen2\.5\-32B\-Instruct with greedy decoding and the 20\-call budget, counted as for PRIME; their own extra model calls \(planning turns, re\-plans, planner decisions, judge calls\) are outside the budget and reported in Table[12](https://arxiv.org/html/2610.22426#A5.T12)\. For the fully informed agent and PRIME, the model calls in that table are agent turns, reminders after a silent stop, and the forced final question, and completion adds none\. No system has a human in the loop, so none is offered the ask\-the\-user tool\.

#### Instantiations\.

*AgentSpec*\([Wang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib35)\)adds no text to the agent’s prompt, so the protected agent is the fully informed agent of Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1), the agent to which PRIME’s mask is added\. One rule guards its conclusion action:rule @no\_unsupported\_conclusion trigger emit\_claim check \!conclusion\_established enforce stop end, whose predicate holds when a route of the claimed conclusion has all of its checks recorded as true\. We run the enforcement the paper evaluates,*stop*, which ends the episode without a conclusion, and the corrective enforcement it describes,*self\-examine*, which returns the violated rule to the model in the released comment format and lets it re\-plan up to four times per step\.*ResearchLoop*\([Xia and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib37)\)follows its Algorithm 1: the request is the research question; the conclusions are registered in a claim ledger; one task contract per conclusion is queued from the weakest; code evaluates the evidence gates after every call \(a route gate requires all of its checks, and a conclusion’s gate passes when any of its route gates does\); a task that produces no evidence twice is blocked; and the report contains the admitted conclusions\. The model receives the paper’s*full*condition prompt with the domain nouns replaced and writes an explicit plan, which the runtime keeps with the run state\.*Proof\-or\-Stop*\([Huang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib11)\)runs the lifecycle none,c1c\_\{1\},c2c\_\{2\},c3c\_\{3\}\(done\): a conclusion is an advance request that a code gate admits only when the recorded checks establish one of its routes; a refused request returns a block report that lists each check as established, failed, or missing; the agent may repair twice; the controller, not the agent, ends the loop, at done, at the repair cap, at the budget, or after more than three consecutive turns without an action; and the highest admitted stage is reported\. Our adaptation of*HESP*\([Liu and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib15)\)keeps its configuration except the probe tables, as described below\. It has hypotheses “the strongest supported conclusion isckc\_\{k\}” plus a catch\-all hypothesis,*other*,, a Bayesian ledger over the check values with base rates counted on the development split, probes \(field reads\) chosen by expected information gain per cost, and a controller that concludes when the leading hypothesis reaches posterior 0\.8 with a supporting observation\. The model receives HESP’s released prompt and can only abstain\.*GLEAN*\([Zhang et al\., 2026b](https://arxiv.org/html/2610.22426#bib.bib42)\)verifies the fully informed agent’s logged trajectories: a same\-model judge rates every step against each route of the stated conclusion with the paper’s prompt, the ratings are accumulated and calibrated by Bayesian logistic regression on 100 development trajectories, uncertain cases receive the paper’s differential checks, and the conclusion is stated only when its calibrated probability of being correct is at least 0\.5\.

#### Code and fidelity\.

As of October 2026, HESP’s code is released under the MIT license\. AgentSpec’s and ResearchLoop’s repositories carry no license; AgentSpec’s rule engine runs only LangChain text agents, and ResearchLoop’s repository does not contain the controller its documentation invokes\. Proof\-or\-Stop and GLEAN have no public code\. We therefore reimplemented each decision procedure on the shared tool loop, reusing released prompts and constants where they exist, and record with the code every choice the papers leave open\. Deviations from the papers: greedy decoding throughout; HESP’s fixed per\-probe tables were replaced by exact elimination over check values, because a fixed table cannot represent a conjunction of checks \(with it, the posterior ofc3c\_\{3\}stays near 0\.56 after every check is read\); and GLEAN’s guideline expansion is unavailable because the routes of the stated conclusion are its only guidelines\.

SystemFA↓\\downarrowPrem\.↓\\downarrowUtil\.↑\\uparrowEmit↑\\uparrowReads↓\\downarrowCalls↓\\downarrowFully informed agent26\.728\.338\.099\.03\.094\.4AgentSpec, stop0\.00\.038\.787\.42\.964\.2AgentSpec, self\-examine0\.00\.040\.192\.93\.065\.8ResearchLoop0\.00\.047\.797\.03\.226\.0Proof\-or\-Stop0\.00\.052\.099\.24\.2112\.3GLEAN14\.414\.635\.083\.33\.099\.2HESP0\.011\.759\.2100\.03\.913\.9PRIME0\.00\.045\.5100\.02\.755\.5PRIME with completion0\.00\.059\.2100\.03\.615\.5Table 12:Closest\-system results on 480 tasks at 20 calls\. FA and Prem\. are episode percentages, Emit is among answerable tasks, and Reads counts fields\. Calls counts model turns, planning, and reminders as applicable, and for GLEAN only its judge calls on the fully informed agent’s runs\.Gates on the routes prevented unsupported conclusions but stopped short of the strongest supported one\.Table[12](https://arxiv.org/html/2610.22426#A5.T12)shows that AgentSpec, ResearchLoop, and Proof\-or\-Stop stated nothing unsupported and nothing their reads had not established\. AgentSpec’s stop rule fired in 21\.7% of episodes and ended them without a conclusion\. Self\-examination recovered some of these, at 5\.8 model calls per task, but both stayed below PRIME without completion \(by family\-mean differences of 7\.5 and 6\.1 points\)\. ResearchLoop’s task queue led the agent from the weakest conclusion upward, and its final report contained only admitted conclusions\. In 14\.4% of episodes, the agent’s own report claimed more than its gates admitted\. ResearchLoop reached 47\.7, a family\-mean 3\.0 points above PRIME without completion \(95% CI \[−\-0\.3, 6\.3\]\)\. Proof\-or\-Stop drove the agent towardc3c\_\{3\}and read more fields than PRIME’s agent alone \(4\.2 against 2\.8 per task, at 12\.3 model calls\), which put its utility a family\-mean 7\.7 points above PRIME without completion \(95% CI \[5\.0, 10\.5\]\)\. Under PRIME’s own cap, which answers at most three turns without an action per episode, its utility changed by 0\.3 points, so the difference does not come from its more lenient cap\. None of the three runs the remaining checks itself\. Running them lifts PRIME with completion to 59\.2, family\-mean differences of 10\.3 points over ResearchLoop and 5\.6 over Proof\-or\-Stop \(95% CIs \[7\.7, 13\.2\] and \[3\.8, 7\.5\]\)\.

bminb\_\{\\min\}bmin\+1b\_\{\\min\}\{\+\}12​bmin2b\_\{\\min\}20*Balanced split: utility↑\\uparrow*Ceiling\-targeting \(no model\)59\.259\.259\.259\.2HESP controller58\.059\.259\.259\.2*Locator\-uncertain copy: utility↑\\uparrow*PRIME51\.550\.748\.848\.2PRIME with completion53\.754\.6r59\.2r59\.2rBlind enumeration \(no model\)40\.344\.758\.559\.2HESP controller11\.212\.350\.359\.0True locators \(no model\)59\.259\.259\.259\.2Table 13:Budgeted PRIME–HESP comparison \(480 tasks\)\. The HESP and no\-model controllers use scripted checks\. The markerrdenotes completion replay from PRIME stopping points\. The balanced\-split premature\-conclusion rate is 0\.0% for ceiling targeting and 11\.7% for HESP at every budget\.HESP matched PRIME with completion where every check was code reading a named field, and fell behind where budgets were tight or fields had to be located\.HESP’s controller chose every probe and issued all 480 verdicts, and the model never abstained, so the live runs equal the controller’s\. Its utility equaled that of PRIME with completion on every task at 20 calls: both stated the strongest supported conclusion everywhere, which gives the ceiling of 59\.2 that the scripted policies of Section[7\.2](https://arxiv.org/html/2610.22426#S7.SS2)also reach at this budget, since every task has at most eight atoms; but in 11\.7% of tasks \(95% CI \[6\.4, 15\.3\]\) it stated a conclusion its reads had not established, and it read a family\-mean 0\.35 more fields per task \(95% CI \[0\.23, 0\.46\]\)\. When only conclusions that a system’s own reads established are credited, PRIME with completion scored 59\.2 and HESP 49\.0 \(family\-mean difference 8\.7, 95% CI \[5\.0, 12\.7\], better on 56 tasks and worse on none\)\. HESP’s conclusions rest on a posterior: with base rates counted on development data, or on the other three domains only \(utility 59\.2, 10\.2% premature\), the premature conclusions were correct, but with a uniform prior within each hypothesis it stated an unsupported conclusion on 5\.0% of tasks \(utility 49\.4\), and with independent fair\-coin checks it never reached the threshold\. Raising HESP’s threshold removes the premature conclusions at a cost: at 0\.9 none were premature and utility stayed at 59\.2 at 20 calls, but it read 4\.6 fields per task \(PRIME with completion, 3\.6\) and scored 50\.4 atbminb\_\{\\min\}; at 0\.95 it scored 36\.6 atbminb\_\{\\min\}; at 0\.99 it never concluded\. PRIME reports what the routes establish, so it needs no such threshold\. Table[13](https://arxiv.org/html/2610.22426#A5.T13)compares the two controllers by budget, with PRIME atbmin\+1b\_\{\\min\}\{\+\}1run for that table\. Atbminb\_\{\\min\}, the ceiling\-targeting policy scored 59\.2 against 58\.0 for HESP’s controller \(family\-mean difference 1\.6, 95% CI \[0\.6, 2\.7\], with 17 tasks better and none worse\) with fewer reads \(3\.4 against 3\.9\), and the live PRIME with completion scored 58\.8 \(family\-mean difference 1\.1,p=0\.04p=0\.04\)\. On the locator\-uncertain copy, HESP’s controller cannot read the descriptions and abstains unless one hypothesis is probable enough: it scored 11\.2 atbminb\_\{\\min\}, against 53\.7 for PRIME with completion \(family\-mean difference 41\.8, 95% CI \[37\.1, 46\.5\]\) and 40\.3 for blind enumeration\. At 20 calls, blind enumeration reached 59\.2, while HESP reached 59\.0 and stated one unsupported conclusion\.

GLEAN reduced unsupported conclusions but could not remove them\.Calibrated on 100 development trajectories, where its area under the receiver operating characteristic curve \(AUROC\) was 0\.85, the verifier ranked the held\-out stated conclusions with AUROC 0\.84 and expected calibration error 0\.06, and its differential checks fired on 49% of them\. It accepted 380 of the 466 stated conclusions, 69 of the 128 unsupported and 311 of the 338 supported, so false authorization fell from 26\.7% to 14\.4% and utility from 38\.0 to 35\.0, at 9\.2 judge calls per task\. A verifier of a finished trajectory can accept or reject the agent’s conclusion, but it cannot direct the agent to the checks that would establish a stronger one\.

## Appendix FExternally Derived Regulatory Requirements

#### Summary\.

Section[7\.5](https://arxiv.org/html/2610.22426#S7.SS5)gives the question, the setup, and the main results\. This appendix describes the regulation and records, the two construction workflows, how each program was validated and frozen, the held\-out sample, and the scoring, and then explains the results\. The tracker is not a legal adjudication\. The assistant\-built program’s reading of the deadline rules was chosen by agreement with the tracker on a development pool\. A statedckc\_\{k\}is*unsupported*ifkkexceeds the tracker’s level \(3: reported late; 2: due; 1: otherwise\), and*coverage*is the share of registrations with a stated conclusion\. Under the scripted ceiling\-targeting policy on all 1,999 registrations, the protocolized program covered 92\.4% with 3\.5% unsupported \(95% CI \[2\.8, 4\.4\]\), and the assistant\-built one 26\.3% with 1\.8%\.

#### Regulation and records\.

The source is the U\.S\. clinical\-trial results\-reporting regulation, 42 CFR Part 11\([U\.S\. Department of Health and Human Services, 2016](https://arxiv.org/html/2610.22426#bib.bib33)\), which implements the results\-reporting provisions of the Food and Drug Administration Amendments Act of 2007 \(FDAAA\)\. Part 11 was amended in December 2024 to update referenced web addresses\([U\.S\. Department of Health and Human Services, 2024](https://arxiv.org/html/2610.22426#bib.bib34)\)\. The programs encode its sections 11\.22\(b\), 11\.42, and 11\.44\(a\) to \(c\)\. The records are ClinicalTrials\.gov registrations, read through the registry’s public API \(version 2\)\. The development pool is a snapshot of 6,000 registrations frozen on 3 August 2026, with its inputs pinned by hash\. The reference is the FDAAA TrialsTracker\([DeVito et al\., 2018](https://arxiv.org/html/2610.22426#bib.bib5);[DeVito et al\., 2020](https://arxiv.org/html/2610.22426#bib.bib6)\), the reporting\-status tracker of the summary, which classifies each tracked trial from the same registry records as reported, reported late, overdue, or ongoing\. We use its export of 3 August 2026, which lists 49,755 trials\. Because the tracker reads the same registry, the comparison tests the rule and the decision procedure, not the data\.

#### Two construction workflows\.

In the*assistant\-built*workflow, an LLM coding assistant \(Anthropic Claude\) wrote the program as code: the three conclusions, six checks that read the study type, start date, regulatory status of the product, primary completion date, results\-submission date, and certification date, and the routes\{e1,e2,e3\}\\\{e\_\{1\},e\_\{2\},e\_\{3\}\\\},\{e1,…,e4\}\\\{e\_\{1\},\\ldots,e\_\{4\}\\\}, and\{e1,…,e5\}\\\{e\_\{1\},\\ldots,e\_\{5\}\\\}\. No field path, predicate, or route was written or edited by a person\. Every check runs through the runtime’s unextended ten\-predicate grammar, and each registration’s reference values are computed by the runtime’s own evaluator\. In the*protocolized*workflow, protocol and code were committed before any run\. Qwen2\.5\-32B\-Instruct received selected definitions of 42 CFR 11\.10\(a\), the text of 11\.22\(b\), 11\.42, and 11\.44\(a\) to \(c\), a catalog of the registry fields, and three unlabeled registrations\. It wrote programs of at most 12 single\-field atoms, routes for the three conclusions \(herec2c\_\{2\}requires that the deadline has passed by the snapshot date\), and a sandboxed function for derived values such as deadlines; each round drew one greedy and eight sampled candidates\.

#### Validation and freezing\.

The assistant\-built program’s deadline logic was refined over four cumulative readings of the statute: a tracker emulation, then the calendar\-year deadline of 11\.44\(a\), then the certification\-timeliness condition of 11\.44\(b\)\(1\), then removal of an administrative grace period\. Each reading was scored for agreement with the tracker on the 6,000 snapshot registrations \(94\.8%, 94\.8%, 94\.3%, and 98\.7%\), and the last, which agreed best, was retained; its 76 residual disagreements were inspected and traced to the tracker’s dating of certifications\. No review of the program against the regulation by a person is recorded beyond this comparison, and the program was then fixed in the instance builder\. The protocolized candidates were validated on 600 development\-pool registrations, re\-fetched in full: each candidate’s full\-evidence level was scored against the tracker \(17 of 18 candidates valid; the best of round 0 agreed on 42\.0%\), the best was returned once with 12 validation disagreements for repair, and the selected revision \(71\.0%\) was frozen and hashed\. The frozen program checks that the study is interventional and studies an FDA\-regulated drug or device, that primary completion falls after 17 January 2017, that a deadline 365 days after primary completion has passed, and that results were first submitted after it\. The 365 days approximate the one\-year deadline of 11\.44\(a\) and differ from it by a day when the year contains 29 February\. The frozen program omits the phase\-1 and feasibility exclusions and the U\.S\.\-connection condition of 11\.22\(b\), and the certification extensions of 11\.44\(b\) and \(c\)\.

#### Test samples\.

The assistant\-built program was first tested on the development pool\. Of the 6,000 snapshot registrations, it classified 4,990 as not subject to the requirement; of the remaining 1,010, 481 belonged to sponsors with a single trial in the pool or fell outside a cap of 600 and were not used, and 210 could not be classified because an applicability field could not be read by the deployed predicates\. The remaining 319 registrations, from 124 sponsors, were written as instances, validated against the task schema, and committed before any agent ran, and the agent runs saw no tracker labels\. Because the reading of the statute was chosen against the tracker on this pool, agreement on the 319 is not out of sample with respect to that choice\. The held\-out sample removes this dependence\. With the builder, its predicates, the selection rules, and the scoring rule frozen and the protocol fixed before any label was read, we sampled 2,000 of the 43,755 trials in the tracker export that lie outside the development pool and come from sponsors absent from it \(seed 20261010\), fetched each from the public API on 10 October 2026, and stored it verbatim; 1,999 fetches succeeded\. Both programs were run on all 1,999 registrations, and the agents on a random subset of 600 of them; the tracker’s labels were read once, after every episode had run\. Two earlier runs of the protocolized test were discarded before any test label was read, because the sandbox blocked modules that the date library loads; the protocol’s deviation log lists the fixes\. Table[14](https://arxiv.org/html/2610.22426#A6.T14)shows how the assistant\-built program’s own exclusions, all based on registry fields and applied before any label was read, reduce the held\-out sample to the 526 registrations it classifies; for the 353 whose applicability field the deployed predicate grammar cannot read \(for instance a month\-precision start date\), no attestation is made, so the program abstains, as it did for 210 of the development pool’s 1,010\.

Held\-out stratumValueSampled; fetched2,000; 1,999Not an applicable clinical trial \(11\.22\(b\)\)370Not yet due at the snapshot date750Applicable and due879applicability field unreadable353classified526Classified, of applicable and due59\.8%Classified, of fetched26\.3%Tracker agreement \(518/526\)98\.5%original statuses only \(499/501\)99\.6%unchanged since export \(495/503\)98\.4%Table 14:Assistant\-built held\-out sample\. Program exclusions precede tracker labels\. The first two tracker\-agreement rates have 95% intervals \[97\.0, 99\.2\] and \[98\.6, 99\.9\]\.
#### Scoring against the tracker\.

Two scores are used\. The assistant\-built program’s classifications \(compliant, late, overdue\) are compared with the tracker’s statuses by binary agreement: a registration agrees when both call it adverse \(late or overdue for the program; reported late or overdue for the tracker\) or both do not, over the registrations both classify\. For the end\-to\-end test of both programs, unsupported conclusions and coverage are as defined in the summary, utility credits the strongest supported level as in Section[6](https://arxiv.org/html/2610.22426#S6), and a registration without an instance counts as an abstention\. Every test registration is one the tracker follows, and level 1 is not an independent determination that a trial is subject to the regulation, so this test cannot penalize calling an inapplicable trial applicable\.

#### Results\.

Under the ceiling\-targeting policy the two programs reached utility 47\.5 and 18\.4, and the assistant\-built program’s unsupported rate of 1\.8% has a 95% CI of \[1\.3, 2\.5\]\. On the 1,112 registrations the tracker counts as due, the two stated a conclusion for 87\.1% and 44\.4%\. The protocolized program’s full\-evidence level agrees with the tracker’s on 71\.6% of these due registrations, close to its validation figure of 71\.0%, and on 94\.3% of the others, so its agreement over all test registrations is higher \(81\.6%\): 587 of the 600 validation registrations are due, against 1,112 of the 1,999 test registrations\.

Where the assistant\-built program classified a registration, its classification agreed closely with the tracker\. Table[15](https://arxiv.org/html/2610.22426#A6.T15)shows agreement on 317 of the 319 development registrations \(99\.4%\), 52\.0% of which were late or overdue, and on 518 of the 526 held\-out registrations it classified \(98\.5%\), with no stated conclusion lacking a route\. The 98\.5% agreement and the 1\.8% unsupported rate use different definitions\. Agreement compares the program’s adverse or non\-adverse classification with the tracker’s on the 526 registrations it classified, while a conclusion is unsupported when its level exceeds the tracker’s, for example when the program states that results are due for a trial the tracker still lists as ongoing, as in 25 of the 36 cases\. The held\-out classifications were 165 compliant, 164 late, and 197 overdue\. Because the records were fetched on 10 October against the tracker’s export of 3 August, a field updated in between can produce a mismatch that is not a policy difference\. Of the 526, 23 carry such an update \(including 3 results submissions and 1 certification\), all 23 agree with the tracker, and agreement on the 503 unchanged records is 495 of 503 \(98\.4%\)\. Two of the five trials the program calls late and the tracker overdue submitted after the export\. Both statuses are adverse, so they count as agreement\. In the cross\-tabulation of program against tracker, the registrations the program calls compliant are 146 reported and 19 ongoing, those it calls late are 157 reported late, 2 reported, and 5 overdue, and those it calls overdue are 191 overdue and 6 ongoing\.

QuantityValueLate or overdue under the assistant\-built program52\.0%Tracker agreement, development pool \(317/319\)99\.4%Tracker agreement, held out \(518/526\)98\.5%Held\-out sample classified \(526/1,999\)26\.3%Stated conclusions without a route0\.0%Filed on time \(153\): strongest conclusion statedc2c\_\{2\}Filed late \(86\):c3c\_\{3\}stated84\.9%Never filed \(80\):c3c\_\{3\}stated0\.0%Table 15:Assistant\-built program on 319 development and 526 held\-out registrations\.
#### What explains the differences\.

The differences trace mainly to the programs\. The protocolized program omits the certification extensions of 11\.44\(b\) and \(c\), and 55 of its 70 unsupported conclusions involve a filed certification\. It also omits the phase\-1 and feasibility exclusions and the U\.S\.\-connection condition of 11\.22\(b\), which this test cannot penalize\. The assistant\-built program’s builder makes instances only for registrations it classifies as applicable and due, which limits its coverage, and 25 of its 36 unsupported conclusions are registrations the tracker keeps ongoing that the program counts as due\. None of its eight held\-out disagreements was updated after the export; they are clause differences: six trials whose deadline fell in the 30 days before the export, which the tracker’s administrative grace period keeps ongoing and the program’s reading calls overdue, and two late filers that the tracker lists as reported on time because of how it dates a certification\. Of the 526 registrations, 41 carry a certification, and 3 of the 8 disagreements are among them\. The two development\-pool disagreements are of the same kind\.

The runtime also declined to call a trial late without a filing\. Table[16](https://arxiv.org/html/2610.22426#A6.T16)separates the program’s verdict, its rule’s classification of the registration, from the conclusion the runtime stated, which is what it could establish from the registry fields its checks read\. On the 319 development registrations, the runtime statedc3c\_\{3\}for 73 of the 86 late filers and for none of the 80 trials that never filed\. A trial that never filed has no submission event to establishc3c\_\{3\}, whereas the tracker counts registry absence as non\-submission, an inference an organization would have to add to the program as an explicit atom\. For the other 13 late filers, the submission date appears only in an estimated field that the program does not read, so the runtime statedc2c\_\{2\}\. The 8 trials with an FDA Notice of Noncompliance were checked separately against the live registry by a standalone implementation of the same deadline logic; none is among the 319\.

Tracker statusStatedVerdictrep\.lateoverduec2c\_\{2\}c3c\_\{3\}compliant \(153\)153001530late \(86\)28401373overdue \(80\)0080800Table 16:Development registrations \(319\)\. Program verdicts versus tracker status \(left\) and runtime\-reported conclusions \(right\)\.The agents’ results reflect stopping, not the rule\. On the 319 development registrations, with the assistant\-built program as the standard and Qwen2\.5\-32B\-Instruct at 20 calls, the fully informed agent stated no unsupported conclusion at utility 49\.1, statingc2c\_\{2\}for 151 registrations andc1c\_\{1\}for 168, neverc3c\_\{3\}, and stopping after four calls in 313 episodes\. PRIME without completion also stated none but reached only 36\.5: in 291 of the 319 episodes the agent made the three calls ofc1c\_\{1\}’s route and then answered in text through three reminders that named the one remaining field ofc2c\_\{2\}’s route, after which the runtime statedc1c\_\{1\}\. Every registration supportsc2c\_\{2\}, so stopping atc1c\_\{1\}loses 33\.3 of the 66\.7 points thatc2c\_\{2\}earns\. With completion, the runtime made the remaining calls in 299 of the 319 episodes \(1\.85 per episode\), and PRIME reached 74\.3, the scripted policies’ value cell for cell\. Table[6](https://arxiv.org/html/2610.22426#S7.T6)shows the same pattern for both programs on the held\-out subset of 600: PRIME with completion matched the ceiling\-targeting policy \(3\.2% and 1\.7% unsupported, utility 47\.7 and 19\.0\), while PRIME alone \(0\.3% and 0\.2%, utility 32\.3 and 9\.9\) and the fully informed agent \(0\.0% and 0\.2%, utility 31\.2 and 13\.1\) stopped at weaker conclusions\. Stopping atc1c\_\{1\}, which this scoring credits for every test registration, also avoided most of the programs’ errors\. The runtime states what the committed program authorizes and no more, so agreement with the tracker depends on how faithfully the program encodes the regulation\. The builder and the reading\-by\-reading comparison are insrc/suffice/construction/fdaaa/of the released code, the pinned inputs indata/fdaaa/external/, and the held\-out sample identifiers and record hashes inexperiments/fdaaa\_heldout/\.

ReActStatic checklistPRIME without guidanceDomainnnFAUtilityFAUtilityFAUtilitySoftware review2147\.624\.60\.020\.60\.037\.3Research review8100\.04\.20\.010\.40\.037\.5Security875\.025\.00\.0100\.00\.035\.4Financial825\.075\.00\.0100\.00\.083\.3Drug safety785\.714\.30\.081\.00\.045\.2Clinical trials887\.518\.80\.039\.60\.045\.8Table 17:Hand\-built exploratory pilot with gpt\-4\.1 at 20 calls\.

## Appendix GExploratory Pilot on Hand\-Built Tasks

Before building SUFFICE, we ran an exploratory pilot on hand\-built tasks to see whether enforcement behaved as intended outside generated records\. The pilot is reported separately because its tasks, models, and agents differ from the benchmark’s, and its results are never pooled with the confirmatory statistics\. It has 21 software\-review tasks on pinned repository commits, 8 research\-review tasks, and 31 record tasks over 27 records, and every conclusion has one route\. Runs used gpt\-4\.1 and gpt\-4o\-mini at 20 tool calls, except where noted\. The*static checklist*is an enforced agent that demands every atom on any route of a conclusion before stating it\.

Enforcement gave zero false authorization in every pilot domain\.Table[17](https://arxiv.org/html/2610.22426#A6.T17)shows that, with gpt\-4\.1, ReAct stated unsupported conclusions on 25\.0% to 100\.0% of the tasks in each domain, while the static checklist and PRIME without guidance stated none; with gpt\-4o\-mini on the software tasks, PRIME reached 0\.0% \(utility 38\.9\) against ReAct’s 71\.4% \(34\.1\)\. Because every conclusion has one route, the static checklist and PRIME’s program coincide here, so their utility differences come from the agent’s behavior\. The checklist beat PRIME without guidance on utility in security, financial, and drug safety; an exploratory guidance arm, added after that result was seen, raised PRIME to 100\.0 in security and financial and to 76\.2 against 81\.0 in drug safety\. The pilot’s McNemar tests with Qwen2\.5\-7B and Qwen2\.5\-32B compared false authorization between PRIME with and without guidance, which is zero for both by construction, so they could not detect a guidance effect; the confirmatory study therefore tests guidance on utility\.

## Appendix HExtended Related Work

LLM outputs, including those of agents that interleave reasoning with tool calls\([Yao et al\., 2023](https://arxiv.org/html/2610.22426#bib.bib39)\), have been made more reliable from the answer backward, through self\-critique and revision\([Shinn et al\., 2023](https://arxiv.org/html/2610.22426#bib.bib30);[Dhuliawala et al\., 2024](https://arxiv.org/html/2610.22426#bib.bib7)\), factuality checks against retrieved evidence\([Chern et al\., 2025](https://arxiv.org/html/2610.22426#bib.bib2);[Wei et al\., 2024](https://arxiv.org/html/2610.22426#bib.bib36)\), and selective prediction or calibrated withholding\([Geifman and El\-Yaniv, 2017](https://arxiv.org/html/2610.22426#bib.bib10);[Mohri and Hashimoto, 2024](https://arxiv.org/html/2610.22426#bib.bib17)\)\. Minimal evidence group identification determines small evidence sets that verify a claim, including alternative sets for one claim\([Li et al\., 2025](https://arxiv.org/html/2610.22426#bib.bib14)\)\. GLEAN\([Zhang et al\., 2026b](https://arxiv.org/html/2610.22426#bib.bib42)\)grounds verification in clinical guidelines and actively collects evidence when calibrated uncertainty is high; HALT\([Roh and Han, 2026](https://arxiv.org/html/2610.22426#bib.bib24)\)stops retrieval when evidence coverage is sufficient\. These methods motivate evidence\-aware checking, but PRIME studies a distinct target: the explicit logical requirements for*several ordered conclusions*, including alternative sufficient routes that remain open after a failed check\. Behavioral policy failures documented by[Schmied et al\. \(2026\)](https://arxiv.org/html/2610.22426#bib.bib27),[Reddy et al\. \(2026\)](https://arxiv.org/html/2610.22426#bib.bib21), and agent benchmarks\([Yao et al\., 2025](https://arxiv.org/html/2610.22426#bib.bib38)\)further motivate an enforcement boundary outside the model\.

External controllers provide the closest foundations\. Runtime shielding blocks unsafe actions\([Alshiekh et al\., 2018](https://arxiv.org/html/2610.22426#bib.bib1)\); AgentSpec\([Wang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib35)\)enforces configurable rules over agent actions and completion; Progent\([Shi et al\., 2025](https://arxiv.org/html/2610.22426#bib.bib28)\)controls tool privileges and policy changes; and[Doshi et al\. \(2026\)](https://arxiv.org/html/2610.22426#bib.bib8)derive tool\-use constraints from hazard analysis\. AGATE\([Zhang et al\., 2026a](https://arxiv.org/html/2610.22426#bib.bib41)\)emphasizes provenance\-aware protection of agent execution\. These systems primarily control*actions or transitions*, whereas PRIME controls*which evidence\-dependent conclusion may be released*\. This boundary is not exclusive: AgentSpec can check agent completion, and action guards could complement PRIME’s evidence resolvers\.

Managing the information supplied to an agent can expose requirements, tool observations, and pending checks, but Section[7\.1](https://arxiv.org/html/2610.22426#S7.SS1)shows that availability in the model’s context is distinct from authorization of its output\. PRIME keeps the ledger as runtime state and uses the same committed requirements both to guide the remaining checks and to reject conclusions the recorded checks do not authorize\. This targets a narrower property than verifying all intermediate reasoning or the factual correctness of the observations\.

More directly, ResearchLoop\([Xia and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib37)\)uses durable task contracts, evidence objects, and claim\-admission rules for AI\-assisted research\. Proof\-or\-Stop\([Huang et al\., 2026](https://arxiv.org/html/2610.22426#bib.bib11)\)requires fresh, mechanically admissible evidence before advancing coding lifecycle states and includes repair or stopping\. EG\-VAR\([Ren, 2026](https://arxiv.org/html/2610.22426#bib.bib23)\)uses tool\-attested proofs to certify empirical claims\. These systems already demonstrate evidence gating; PRIME*does not claim to originate evidence gating or precommitment*\. Its more specific control problem asks, after partial or failed observations, which*graded conclusion*is currently authorized and which*still\-live sufficient route*can potentially establish a stronger one within the remaining check budget\. The committed route representation is used for both answers\.

HESP\([Liu and Wang, 2026](https://arxiv.org/html/2610.22426#bib.bib15)\)is particularly relevant because it combines cost\-aware probing with evidence\-backed stopping\. Its Bayesian hypothesis ledger and information\-gain probe selection address diagnostic triage\. PRIME instead represents conditions under which particular conclusions are logically sufficient, including disjunctive routes and weaker authorized alternatives\. Likewise, GLEAN’s calibrated uncertainty is different from PRIME’s route\-based authorization\. These approaches are complementary\. Section[7\.4](https://arxiv.org/html/2610.22426#S7.SS4)runs adapted versions of both, with AgentSpec, ResearchLoop, and Proof\-or\-Stop, on the same tasks, requirements, and budgets\. Appendix[E\.5](https://arxiv.org/html/2610.22426#A5.SS5)reports the results\.

The formal ingredients are classical\. Minimal sufficient routes are related to prime implicants\([Quine, 1952](https://arxiv.org/html/2610.22426#bib.bib19)\), consistency\-based diagnosis and truth\-maintenance systems\([Reiter, 1987](https://arxiv.org/html/2610.22426#bib.bib22);[de Kleer, 1986](https://arxiv.org/html/2610.22426#bib.bib3)\), and abductive classifier explanations\([Shih et al\., 2018](https://arxiv.org/html/2610.22426#bib.bib29);[Ignatiev et al\., 2019](https://arxiv.org/html/2610.22426#bib.bib12)\)\. Budgeted checks are related to sequential testing\([Ünlüyurt, 2004](https://arxiv.org/html/2610.22426#bib.bib32);[Deshpande et al\., 2016](https://arxiv.org/html/2610.22426#bib.bib4)\)and active feature\-value acquisition\([Saar\-Tsechansky et al\., 2009](https://arxiv.org/html/2610.22426#bib.bib25)\)\. PRIME claims none of these ideas in isolation\. Its contribution is a*shared precommitted program for route\-aware evidence acquisition and graded answer authorization*, together with a layered evaluation showing where enforcement succeeds and where incorrect programs or fallible resolvers still cause errors\. In operational reviews, this distinction matters when blocking an unsupported claim is necessary but insufficient: another acceptable evidence route may still be worth checking before reporting a weaker result or abstaining\.