The Proof Checked. Does the Spec Say What the Guideline Says?

Compile-Time Intelligence, Part 6

A clinical guideline, a benefit policy or a lending rule contains knowledge an organization wants to apply consistently. Translating it into software could make its thresholds and exceptions available whenever a decision is made, with a record that someone can inspect afterward.

But the same repeatability can preserve a mistake. A program that misreads a requirement can apply that misreading to every relevant case, even when it runs without errors.

Formal verification offers something stronger than testing a few examples: a proof that a program satisfies a specification, a precise statement of what it must do. Producing those proofs has often required substantial specialist effort. Now AI is making more of that work possible.

On 22 October 2026, Anthropic and Theorem, co-founded by Jason Gross and Rajashree Agrawal, reported using Claude to produce machine-checked proofs for 239 test entry points across 123 open-source libraries. An entry point is a function through which a test exercises the code. The successful proofs comprised about 180 million lines in Rocq, formerly Coq, a proof assistant that checks formal arguments. They established specified no-crash properties for the compiled programs, after patching some discovered bugs, not that the libraries were correct in every respect. [1] [2]

That is a substantial development. It also brings an older question into sharper focus: if the machine can prove that a program follows its specification, how do we establish that the specification says what we intended?

This is the next step in Eventum’s Compile-Time Intelligence series. Part 1 distinguished proof validity from faithful translation. Parts 2 and 3 examined tests and the authority of their expected answers. Part 4 proposed keeping the interpretation connected to its source and review decisions. Part 5 showed that even the constraints used to generate a rule can contain an interpretation that needs justification. [3] [4] [5] [6] [7]

Part 6 turns to the evaluation itself: how can we expose a mistranslation before accepting its specification? Three approaches recur in the research: checking the answers a translation produces, comparing it with a reference, and examining whether its meaning survives translation between representations.

Each provides useful evidence. The opportunity is to combine them so that machines help find the cases that expose a disagreement, while the source and a documented review establish how that disagreement should be resolved.

A proof needs a statement worth proving

In the October project’s main experiment, the starting points were existing fuzzing harnesses: small programs that exercise a library and report certain failures as crashes. A fuzzer feeds generated inputs into a harness to look for those failures. The team instead proved their absence across all inputs below a specified size, within the modeled environment. The tests supplied properties the maintainers already cared about, without first requiring a complete specification of every library feature. [1] [2]

The appendix limits the result to inputs below 64 MiB (mebibytes) and specifies a model of programs compiled for the RISC-V processor architecture and running on Linux. [2]

Other experiments addressed functional behavior, what a program does rather than only whether it crashes. One formalized RFC 1950, the document defining the zlib compression format, and checked an implementation against it. Another built a Python interpreter in Rust, a program that executes Python code, and verified it against a formal definition of a language subset. Testing against CPython, the standard implementation, found 99.95% agreement across more than 1.7 million programs. The proof checked the interpreter against the formal definition; the tests compared its observed behavior with CPython. [1] [2]

These specifications had existing tests, implementations or language definitions to compare with. Such comparisons can expose a mismatch. They cannot, by themselves, establish that a specification captures every intended requirement: a weak statement can agree with mature code while omitting behavior that matters.

Oleg Mürk, who spent about five years at OpenAI training models on programming competitions and formal mathematics in Lean, makes this distinction in his commentary on the report: “Of course, fuzz harnesses specify only some correctness properties. In the simplest case, the proofs establish crash-safety, not full functional correctness.” He also warned: “A model could satisfy a specification simply by removing functionality.” In an earlier post, he describes the specification and verification stack as part of the trusted base: the assumptions and components on which the result depends. [8] [9]

The report penalized and audited patches to discourage such shortcuts. [1] The same concern applies when a model edits the specification. Weakening a requirement can make a proof easier without making the software more faithful to its source.

For a newly compiled guideline, that source connection may be the least established part of the system.

Start with the decision the rule is meant to express

A guideline does not necessarily arrive with a trusted executable reference. An older quality-measure system or decision-support tool may provide one, but its interpretation still needs justification. When a team is creating the first executable version, the text and its surrounding definitions are the starting point.

Return to the series’ historical blood-pressure example. A 2019 performance-measures paper from the American Heart Association and American College of Cardiology reproduces the 2017 classification and discusses lowering pressure below a target of 130/80 millimeters of mercury (mm Hg). Systolic pressure is the first value; diastolic pressure is the second. [10]

Suppose the task is to translate that paired target into a rule that returns either “below target” or “not below target”. Assume the supplied values are valid averages obtained as required, and that the target applies to the case. Measurement selection, patient eligibility and treatment decisions are outside this simplified example. It is an illustration of software translation, not clinical advice.

A candidate rule is the proposed executable logic; its specification states what that logic must do. Here, the specification can be written as the condition for returning “below target”:

Rule A requires both values to be below their thresholds:

below_target = systolic < 130
               AND diastolic < 80

Rule B accepts either value below its threshold:

below_target = systolic < 130
               OR diastolic < 80

Here, AND requires both conditions; OR requires at least one. These are not two equally supported clinical interpretations. Rule B is a possible mistranslation whose defect we want the evaluation to expose.

An implementation of Rule B could be proved to return “below target” exactly when either condition holds. That proof would be correct. The defect would be in choosing OR as the specification for a target requiring both values.

The distinction is easy to inspect once written out. The challenge is whether the checks we use will reveal it, especially when the original text expresses the relationship through compact notation rather than spelling out the operator.

Three ways to evaluate the translation

1. Check the answers it gives

The most direct approach is to run a candidate on cases with justified expected answers. Our two rules agree whenever both values are below their thresholds, and whenever neither is. A test suite containing only those cases cannot distinguish them.

Semantic parsing, the task of translating language into an executable expression, has long faced this problem. Neural Symbolic Machines (Chen Liang, Jonathan Berant, Quoc Le, Kenneth Forbus and Ni Lao) learns from question-and-answer pairs. A model proposes a program, an interpreter executes it against a database, and the resulting answer supplies a training signal. The authors identify a spurious program: one that produces the right answer for the wrong reason. Their example retrieves a person’s birthplace when the question asks where the person died. It succeeds whenever those places happen to coincide. Matching the answer does not distinguish the intended program from the accidental success. [11]

Separating translation from reasoning does not remove that evaluation question. Zhun Yang, Adam Ishay and Joohyung Lee use a language model to translate sentences into logical facts. Hand-written knowledge modules, reusable sets of logical rules, and an answer-set solver, an engine that computes solutions consistent with those rules, do the reasoning. A companion paper by Adam Ishay, Zhun Yang and Joohyung Lee generates the answer-set programs themselves for logic puzzles. Their evaluations examine whether the resulting systems answer questions or solve puzzles correctly. [12] [13]

David Oniani and colleagues, including Yanshan Wang, bring this evaluation question into a clinical setting. They compared three ways of supplying COVID-19 outpatient guidance to a model: a decision tree, a graph expressed in code within the prompt, and worked reasoning examples. A decision tree represents successive choices as branches; a graph represents connected steps or relationships. They assessed recommendations for synthetic patients using automated and human evaluation. Guideline-enhanced approaches improved on plain prompting in the study, with the decision-tree method strongest in the automated evaluation. [14]

The researchers supplied the guideline structure; the study did not establish that models could derive it faithfully from prose. That distinction matters here. Correct answers on a collection of patients are evidence about those answers, not automatically about every decision encoded in the rule.

This is not a reason to abandon answer-based testing. It is a reason to ask which differences the chosen cases make observable.

2. Compare it with a reference program

When a tested case cannot distinguish two programs, their structure may still reveal the difference. That motivates comparing a candidate with a reference program, an implementation accepted as the comparison standard for a stated reason.

Linzi Xing, Xinglu Wang and colleagues, including Yong Zhang, study this approach for linear-programming word problems. A linear program expresses an objective to maximize or minimize and constraints on the allowed solutions, using weighted sums of decision variables. Their metric represents these elements as a graph and measures graph edit distance, the cost of changes needed to transform one representation into another. It accommodates reordered variables and constraints rather than mistaking every difference in presentation for a difference in meaning. [15]

The comparison can reveal differences hidden by an identical answer. But its authority still depends on the reference.

If a justified reference requires both blood-pressure values below their thresholds, comparison can expose Rule B. If the reference also mistakenly accepts either value, agreement preserves the shared error. A structural score measures a relationship between programs; it does not independently establish what the guideline meant.

And a small structural difference need not be a small practical difference. In our example, changing one operator changes which cases satisfy the target.

3. Check what it says in another representation

Without a trusted reference, another approach is to translate the candidate back into language and compare that account with the source. This gives a reviewer a way to inspect the proposed meaning without reading code.

For our two rules, a precise read-back would say “both values must be below” for Rule A and “either value may be below” for Rule B. That exposes the difference immediately. But a loose summary could describe both as “below 130/80”, erasing exactly the distinction under review.

Research explores related cycles that test whether meaning survives a change of representation. Round-trip correctness (Miltiadis Allamanis, Sheena Panthaplackel and Pengcheng Yin) starts with code, describes it in language, generates code from that description, and compares the result with the original. In the code-synthesis evaluation, unit tests stand in for a full proof of equivalent behavior. This is not a direct test of a guideline translation, but it shows why the comparison that closes the loop matters: repeating a transformation is not enough unless the final check detects lost meaning. [16]

Clover (Chuyue Sun, Ying Sheng, Oded Padon and Clark Barrett) checks consistency among code, a natural-language description and formal annotations, statements of what the code requires and guarantees. It combines a language model with Dafny, a language and verification system. On its textbook-level benchmark, it accepted up to 87% of correct instances and rejected all the evaluated adversarial incorrect instances. It also found six incorrect programs in an existing human-written dataset. Those are results from the evaluated examples, not a universal guarantee of translation fidelity. [17]

A related approach compares the two representations directly. FormalAlign (Jianqiao Lu and colleagues) trains a model to judge whether an informal mathematical statement matches its formal translation. It is an alignment judge, not a proof that the judge’s interpretation is right. [18]

Part 1 discussed why this distinction matters. Alexander Bastounis, Fabian Circelli and Anders Hansen identified mismatches between parts of a written Navier-Stokes argument and their translation into Lean, another proof assistant, including a weaker formal bound. Their critique concerns the correspondence between the arguments; successful checking of the formal version does not establish that correspondence. [3] [19]

Reading back helps when it preserves the consequential choices. Repeating the source’s shorthand is not the same as checking its meaning.

The methods answer different questions: did the rule produce the expected answers, does it match a justified reference, and does another representation preserve its meaning? None makes an interpretation authoritative merely because another representation agrees with it.

Ask for the case that separates the rules

A comparison can show that two rules differ without settling which is right. We can still make progress: ask for an input on which that difference changes the answer. That turns a disagreement about code into a concrete question for the source and its reviewer.

Consider these ten illustrative blood-pressure pairs:

110/70, 118/76, 124/78, 128/79, 129/79, 130/80, 135/85, 142/92, 156/98 and 160/100.

Rules A and B agree on all ten. The first five have both values below the thresholds; the remaining five have neither below. Their agreement says something about this set, not about whether mixed cases are rare in practice.

Both rules also pass two plausible internal checks. Every permitted input receives an answer. And lowering either pressure, while holding the other fixed, never changes “below target” into “not below target”. These properties describe consistent behavior, but they do not choose between AND and OR.

A solver searches for values that satisfy a stated logical condition. Here the condition is simple:

Find systolic and diastolic values
for which Rule A and Rule B disagree.

At 134/76, Rule A returns “not below target” and Rule B returns “below target”. The same disagreement occurs at 124/84. These inputs are counterexamples to the claim that the rules always agree, not yet judgments about which rule matches the guideline. More generally, the rules differ exactly when one value is below its threshold and the other is not.

The input-output comparisons and logical properties in this example were checked programmatically. The read-back discussion above illustrates a possible failure; it is not a measured result from running a language model.

The solver does not need to know the intended answer to find a disagreement. It needs the two formal rules and a shared definition of their inputs. Those rules could come from a candidate and a reviewer’s proposed correction, two independently written implementations, or separate model-generated candidates.

This is the useful change in the review process: instead of debating two expressions in the abstract, the reviewer sees a case whose outcome depends on the choice.

The solver has found the question that matters. It has not supplied the authority for the answer.

For more complex programs, the search may be bounded or inconclusive, and agreeing candidates may share an omission. The method does not generate every interpretation the source could require. It makes the consequences of the candidates under consideration easier to inspect.

Return to the source with a concrete question

The document provides a more explicit statement than the isolated 130/80 notation. In its discussion of treated patients, it describes above-goal pressure as systolic at least 130 or diastolic at least 80. For the paired-target task, being below therefore requires both values below their thresholds. Its classification table and higher-category instruction are consistent with that reading: the low diastolic value at 134/76 does not cancel the raised systolic value. Rule A preserves the paired target; Rule B does not. [10]

The solver made the consequential case visible. The fuller source supplied the basis for resolving it. The target was never simply an uninterpreted slash that made AND and OR equally defensible.

A model can help retrieve the relevant passage or assess its support, as Part 5 discussed through the knowledge-extraction system ODKE+, and as FormalAlign explores for mathematical statements. The important requirement is that the basis for the interpretation remains inspectable rather than disappearing into a model’s verdict. [7] [18]

The same document can define a different task

The paper also defines performance measures, specified criteria for reporting the quality of care. In PM-1b, PM-2 and PM-3, the pressure criterion is systolic below 130. Those measures have their own eligible populations and reporting conditions. That systolic-only criterion is not interchangeable with the paired treatment target. [10]

At 124/84, the paired target is not met, while the systolic-only threshold is. That does not establish overall compliance with a performance measure, whose other requirements still apply. It shows why the compiled rule must identify which task it implements.

This is a second specification problem, beyond mistranslating AND as OR. A program can faithfully implement a real criterion from the document and still implement the wrong criterion for its intended use.

Naming the source document is therefore not enough. The record needs the relevant passage, the purpose of the rule and the assumptions that connect that passage to the decision being automated.

The operator is only the simplest part of this example. A fuller implementation must also resolve the questions we set aside: which patients the target applies to, which measurements count, and what happens when the required evidence is missing. Those decisions interact. Changing the measurement rule changes the values being compared; changing eligibility changes which cases the target should govern.

Keep the resolved interpretation with the rule

Once the source has justified Rule A, the disagreement cases acquire a new role. They become tests with supported expected answers: 134/76 and 124/84 should both return “not below target” for this paired-target check.

Before review, the cases exposed a disputed output. After review, their justified expected answers become part of the test oracle, the criterion used to judge the program’s outputs. This is Part 3’s answer-key problem made concrete: the expected result comes from a justified interpretation, not from copying the candidate’s behavior. [5]

Part 4’s interpretation record can preserve that connection. For this illustrative example, the record could contain:

This is an illustrative record, not a claim of clinical approval. Its purpose is to make the reasoning available to the next person who reviews or changes the rule.

When the source does not resolve a choice, the record can preserve that uncertainty rather than convert a candidate’s assumption into an approved requirement. Recording an interpretation also means recording where interpretation remains unfinished.

A proof can then establish that the implementation follows the selected formal specification over its stated domain. That proof is valuable precisely because its claim is clear. It need not also settle which guideline applies, whether the measurements were obtained correctly, or whether treatment should change.

If the source or intended use changes, the record identifies what needs reconsideration. A new proof against an edited specification is not, by itself, evidence that the edit was justified.

What becomes easier when machines can carry more of the proof

Theorem’s roadmap puts the ambition well: “Human review should scale with how complex the software’s intended behavior is, not with how much code there is.” [20]

The October appendix gives one encouraging example. In proofs comparing two compiled versions of a program, agents often introduced intermediate specifications with a median size of about 110 lines, compared with programs with a median size of 86 KB. These concerned behavior exercised by the testing entry points, not complete specifications of every library feature. [2]

For guideline compilation, the parallel is not that every specification must fit into 110 lines, or that proof construction has become trivial. It is that the record a reviewer needs can be much more focused than the full implementation and its proof.

Three responsibilities remain distinct.

Make the intended behavior reviewable. A reviewer needs to see which source requirement became which condition, including the supporting context and any unresolved choice. A short specification is useful only if it has not become short by omitting requirements.

Use disagreement to focus attention. Automated comparison can turn a difference between candidates into a concrete case. The source, applicable conventions and qualified review can then establish the expected outcome. These cases add to existing tests rather than replacing them.

Treat specification changes as consequential changes. Weakening a condition may make a proof easier while changing which outputs are accepted. The specification’s history needs to show what changed and why, just as the implementation’s history does. Oleg Mürk’s emphasis on reviewing critical specifications and generated patches applies to both sides of that relationship. [8] [9]

The opportunity is larger than producing a green verification result. It is to use models and formal tools to make the connection between written knowledge and executable decisions easier to examine.

A machine can check a proof and find where two rules disagree. The remaining task is to establish which requirement the organization intended to implement, preserve the evidence for that choice, and keep it attached as the software changes.

The proof checked. The interpretation still needs a reason someone else can inspect.

Building a system that turns policies, contracts, or clinical guidance into executable logic? Talk to Eventum about the translation, evaluation, and review process around it.

Sources

1. Anthropic Frontier Red Team, with Theorem. LLMs are making formal software verification feasible at a much larger scale. October 22, 2026. Reports 239 entry points across 123 OSS-Fuzz libraries and about 180 million lines of successful Rocq proofs, as well as the zlib and Python experiments. The guarantees concern specified properties under the modeled execution assumptions. The report also describes patch penalties and audits, and cites the historical seL4 effort as an illustration of verification cost.
2. Anthropic. Appendix: LLMs are making formal software verification feasible at a much larger scale. October 22, 2026. States the input bound as 64 MiB and describes the modeled binaries, Python semantics and intermediate specifications. The 110-line and 86-KB figures concern specifications and programs in the sanitizer-equivalence work, not comprehensive specifications of all library behavior.
3. Bressler D. AI Is Discovering New Mathematics. The Hard Part Is Knowing Exactly What It Proved. Eventum AI, October 13, 2026. Compile-Time Intelligence, Part 1.
4. Bressler D. The Rule Passed Its Tests. What Did the Tests Establish? Eventum AI, October 19, 2026. Compile-Time Intelligence, Part 2.
5. Bressler D. AI Can Write the Tests. Who Checks the Answer Key? Eventum AI, October 19, 2026. Compile-Time Intelligence, Part 3.
6. Bressler D. The Guideline Compiled Cleanly. Where Did the Interpretation Go? Eventum AI, October 22, 2026. Compile-Time Intelligence, Part 4.
7. Bressler D. The Output Matched the Schema. What Did the Schema Guarantee? Eventum AI, October 27, 2026. Compile-Time Intelligence, Part 5.
8. Mürk O. Commentary on the Anthropic and Theorem report. X, October 23, 2026. Discusses the scope of fuzz-harness specifications and the need to review critical specifications and model-generated patches.
9. Mürk O. Alignment is Dead (for now), Long Live Control! X, September 17, 2026. Describes the specification and verification stack as part of the trusted base. His OpenAI background is described in his August 20 post.
10. Casey DE Jr, Thomas RJ, Bhalla V, et al. 2019 AHA/ACC Clinical Performance and Quality Measures for Adults With High Blood Pressure. Journal of the American College of Cardiology 74(21), 2661-2706 (2019). Section 1.1 explicitly describes above-goal BP as systolic at least 130 or diastolic at least 80 mm Hg; Table 2 supplies the historical classification and category-precedence instruction. PM-1b, PM-2 and PM-3 use systolic pressure below 130 mm Hg within specified populations and measurement conditions. The article’s paired-target example is not a complete implementation of these measures or current clinical guidance.
11. Liang C, Berant J, Le Q, Forbus KD, Lao N. Neural Symbolic Machines: Learning Semantic Parsers on Freebase with Weak Supervision. ACL 2017. Describes answer-based learning and the spurious-program problem, including the birthplace-versus-place-of-death example.
12. Yang Z, Ishay A, Lee J. Coupling Large Language Models with Logic Programming for Robust and General Reasoning from Text. Findings of ACL 2023, 5186-5219. The model translates sentences into logical form for reusable, hand-written answer-set knowledge modules.
13. Ishay A, Yang Z, Lee J. Leveraging Large Language Models to Generate Answer Set Programs. KR 2023. Investigates model generation of answer-set programs for logic puzzles.
14. Oniani D, Wu X, Visweswaran S, Kapoor S, Kooragayalu S, Polanska K, Wang Y. Enhancing Large Language Models for Clinical Decision Support by Incorporating Clinical Practice Guidelines. IEEE ICHI 2024. Compares guideline-informed prompting methods on synthetic patient descriptions across four models, with automated and human evaluation. The study supplies guideline structure; it is not an evaluation of autonomous prose-to-specification compilation.
15. Xing L, Wang X, Feng Y, Fan Z, Xiong J, Guo Z, Fu X, Ramamonjison R, Mostajabdaveh M, Han X, Zhou Z, Zhang Y. Towards Human-aligned Evaluation for Linear Programming Word Problems. LREC-COLING 2024, 16550-16556. Introduces a graph-edit-distance metric that accommodates reordered variables and constraints and compares it with expert judgments. Structural proximity is not a measure of clinical impact or independent evidence of source fidelity.
16. Allamanis M, Panthaplackel S, Yin P. Unsupervised Evaluation of Code LLMs with Round-Trip Correctness. ICML 2024. Uses unit tests as the equivalence proxy in its code-synthesis evaluation; the editing evaluation uses exact match. The paper discusses dependence on the quality of the comparison metric.
17. Sun C, Sheng Y, Padon O, Barrett C. Clover: Closed-Loop Verifiable Code Generation. arXiv:2310.17807, version 4 (2024). Checks consistency among code, docstrings and formal annotations. The up-to-87% acceptance and zero observed false positives concern the evaluated CloverBench instances; six errors were found in MBPP-DFY-50.
18. Lu J, Wan Y, Huang Y, Xiong J, Liu Z, Guo Z. FormalAlign: Automated Alignment Evaluation for Autoformalization. arXiv:2410.10135 (2024). Trains an alignment judge and evaluates it on mathematical benchmarks augmented with constructed misalignments. It is distinct from round-trip translation and does not supply a formal guarantee of source fidelity.
19. Bastounis A, Circelli F, Hansen AC. Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs. arXiv:2610.08144 (2026). Identifies mismatches between written arguments and formalized statements. The claim discussed here concerns correspondence, not a finding that the Lean proof checker accepted an invalid formal inference.
20. von Ebers M, Hampton I, Agrawal H, Champine L, Agrawal R, Gross J. Bootstrapping the Verified Software Stack. Theorem, September 29, 2026. The human-review sentence is from the Setup section. The article cites the stated design goal, not the roadmap’s forecast as an established outcome.