FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number, table row, bug breakdown, quotation, page and section reference, the steps of the seven techniques and Algorithm 1, and the Verus forms; changed one reversed claim about the weakest requires (the disjunction of call-site facts is the strongest requires every call site can prove), one wrong page for the re-reasoning rule, widened claims (one file per component, uninterpreted functions imply vagueness, holds exactly in Verus), and three unmarked inferences; the need for a decreases clause on mutually recursive Verus exec functions is unchecked.

source: Haoran Ding, Zhaoguo Wang, Haibo Chen (Shanghai Jiao Tong University), arXiv:2604.11556v2, 18 Jun 2026, 13 pages of text plus references, no appendix. Code: https://github.com/fmagent-project/FM-Agent (as given on p.2).

earlier notes: distributed_verification_review_b/deep_17_model_agents.md and deep_11_second_pass_agents_invariants.md (same text in both) already record the human inputs, the absence of a soundness guarantee, the four systems with bug counts, the 4,910-versus-4,957 function count, the cost, and that the ablation removes two components at once. This file adds each technique as steps, the Verus form of each, and further gaps in the evidence.

nothing is proved; a bug count is measured

FM-Agent has the shape of Hoare-style verification (a contract per function, callee contracts assumed, each function checked alone) but every step is an LLM reading natural language. Contracts are English sentences, the inference is an LLM’s judgment, and what is reported to the developer is a test that fails. The paper is direct about it: “Although FM-Agent cannot ensure soundness, it realizes much better scalability than existing verification tools.” (Section 9.3, p.12) Scope: “FM-Agent currently supports only sequential functions, not concurrent functions.” (Section 3, p.4)

Measured: 522 bugs reported across four agent-written systems of 277k lines and 8,549 functions (Tables 1 and 2), with one model: all three components “use Claude Sonnet 4.6” (Section 9.1, p.10).

Trusted, or simply unknown:

• Inference: every natural-language contract. No step checks a generated contract against anything but the LLM’s reading of callers and of domain documents.
• the test oracle. Where a reference implementation exists (GCC, DuckDB) the oracle is independent; otherwise: “For systems without a reference implementation, FM-Agent instead checks execution results against the expected outcomes described in the specifications.” (Section 6, p.9) Inference: in that case the generated contract judges its own bug report.
• Inference: a function about which no bug is reported has no status at all. The paper claims nothing for such functions and measures no miss rate.

technique 1: derive a callee’s contract from what its callers expect

what it is: write a function’s pre- and post-condition from its call sites, not from its body, so that a wrong body cannot write its own contract. The unit is the expected specification (Definition 1, p.5): caller F1 expects {P} F2 {Q} when F1’s code guarantees P just before the call and F1’s code after the call needs Q.

when to use: code whose author is unavailable or is an LLM, with no written contracts; any time a contract inferred from the body would be circular.

how it is done:

1. for an entry function, the LLM writes the contract from domain knowledge and the function’s implementation (Section 4.1, p.5)
2. in the same pass, for each callee, write the expected specification from this caller’s point of view: the arguments passed give the pre-condition, the code that consumes the result gives the post-condition (Insight I, p.2; Section 2.3, p.3)
3. move down the call graph: “Each function is processed after the specifications of all its callers are generated.” (Section 4.1, p.5)
4. for an internal function, the LLM combines three sources: “For entry functions, FM-Agent uses only sources (1) and (3); for internal functions, FM-Agent uses all three sources.” (Section 4.3, p.6), the sources being domain knowledge, expected specifications from callers, and the implementation
5. with several callers, merge: the pre-condition is the disjunction of the callers’ pre-conditions and the post-condition the conjunction of their post-conditions (rule in Section 4.3, p.7). An LLM does the merge, because the parts are sentences: “It may require understanding the semantics of the specifications and rephrasing them if there are redundancies or potential conflicts.” (Section 4.3, p.7)
6. functions that call each other sit in one layer and lack each other’s expected specifications, so the implementations of their callers inside the cycle are given to the LLM in their place (Section 4.3, p.7)
7. domain knowledge is cut by component before any of this: an LLM analyses the system’s components and splits the domain knowledge into separate files by component relevance, and only the knowledge relevant to the component goes into a prompt (Section 4.3, pp.6-7)
8. output: one file per function with its contract, the expected specifications for its callees, and its body (Section 4.3, p.7)

the paper’s example (Figures 1 and 2, p.3): from_keyword in Claude’s C Compiler rejects any string whose first byte is not one of 16 characters before matching keywords, so it rejects nullptr. A contract written from the body says the function returns None when the first byte is outside those 16. The contract written from the caller says it returns Some(token_kind) if the string is a reserved keyword of C89 through C23 and None for all other identifiers, which the body violates.

Verus form. Inference: Verus already enforces the two halves of Definition 1: at each call site the caller must prove the callee’s requires, and after the call it may use only the callee’s ensures. So the top-down order is: write the entry function’s requires/ensures; for each callee write a signature whose ensures is exactly what the caller’s proof needs and whose requires is no stronger than what every call site can prove; give the callee a body that ends in admit() for now; run Verus on the caller. When the caller verifies, the callee’s contract is by construction what the caller expects, and the admit() is removed when the callee’s turn comes. Step 5 becomes exact instead of rephrased: with callers needing Q1 and Q2, the ensures lists both; a requires that is the disjunction of call-site facts is the strongest one that every call site can still prove, which gives the body the most to assume. What changes: a too-strong ensures is caught (the callee’s body will not verify), which FM-Agent can only suspect. What does not carry over: the English contract in Figure 2b needs a spec fn defining the keyword set, and writing that definition is the whole difficulty the paper sidesteps; it says of Verus and Dafny that “Specifications generated by FM-Agent cannot be used by these tools, as they target formal specifications rather than natural language specifications.” (Section 9.1, p.11)

evidence: one ablation on one system, with two changes at once. The ablated version writes contracts from implementations only and also replaces the stepwise reasoning with a direct question to the LLM, keeping the same bug validator. “As a result, it discovers only 57 bugs in CCC, which is much fewer than 339 bugs discovered by FM-Agent.” (Section 9.2, p.11) The share owed to caller-driven contracts alone is not measured.

where it fails or what it assumes: Inference: it assumes callers are right more often than callees; a caller that was written to work around a callee’s bug will export the bug as the expected behaviour; and an entry function has no caller, so its contract comes from its own body plus documents, the very circularity the technique is meant to avoid. The paper measures neither the accuracy of generated contracts nor how often the merge in step 5 met a conflict.

technique 2: layered order over the call graph, for parallel generation

what it is: Algorithm 1 (p.6), a layered topological sort that tells which functions can have contracts generated at the same time.

how it is done (Section 4.2, pp.5-6):

1. build the call graph: a node per function, an edge from caller to callee
2. find strongly connected components, since recursion makes cycles
3. collapse each component to one node, giving an acyclic graph
4. compute in-degrees; the nodes with in-degree zero (entry functions) form layer 1
5. repeat: for every node in the current layer, decrement the in-degree of each successor; successors that reach zero form the next layer
6. generate contracts layer by layer, all functions of a layer concurrently, the functions of one component together
7. batch up to N prompts of one layer into one request; N is tuned per codebase and model (Section 4.2, p.6)
8. where the system splits into phases whose functions mostly call within the phase (lexing, parsing, IR generation, optimization, executable generation for a compiler), run phases concurrently (Section 4.2, p.6)

Verus form. Inference: the algorithm is about scheduling agents, so it applies unchanged to a crate: layers come from the Rust call graph, and each layer’s functions can be given to separate workers because each needs only its callers’ finished contracts. One Verus-specific point: functions in one component are mutually recursive, and Verus asks for a decreases clause on each; their contracts must be written together for the same reason the paper gives.

evidence: Table 4 (p.12) gives the room for concurrency: CCC 13 phases with 19, 10 and 4 layers per phase (maximum, median, minimum); VibeTensor 12 phases with 18, 7, 2; VibeOS 14 with 9, 4, 1; Bespoke OLAP 6 with 4, 3, 1. No timing with and without layering is given, and the batch size used is not stated.

where it fails or what it assumes: step 8 says most, not all, calls stay inside a phase. Inference: a cross-phase call then reaches a callee whose other callers may not be processed yet, and the paper does not say how such edges are ordered. The text’s line references into Algorithm 1 are all printed as “Algorithm 1”, so the mapping of prose to lines is by reading.

technique 3: Hoare-style inference in natural language, block by block

what it is: starting from the function’s pre-condition, the LLM writes the condition that holds after each statement or block, as a sentence, and at each exit checks that the accumulated condition implies the function’s post-condition.

when to use: as a bug finder where no formal contract exists. It is preceded by a small experiment that motivates it: on VerusBench functions, three random inputs each, “Claude Code correctly predicts the results for 98.6% of cases (438 out of 444 cases), which demonstrates the capability of LLMs to accurately understand the semantics of small code fragments.” (Section 2.3, p.4) 438/444 is 98.6%.

how it is done (Section 5, pp.8-9):

1. input per function: its body, its contract, and the expected specifications of all its callees
2. take callee contracts as given: “During the reasoning process, we assume that expected specifications of its callees are satisfied, which allows us to focus on the current function and realize compositional reasoning.” (Section 5, p.8)
3. the first statement’s pre-condition is the function’s; each later pre-condition is the previous post-condition (Section 5.2, p.8)
4. branch: the post-condition is the disjunction of the branches’ post-conditions, each branch reasoned with the condition or its negation added (Section 5.2, p.8)
5. loop: see technique 4
6. do not go statement by statement: “It groups statements into larger blocks and reasons about them collectively, reducing the number of LLM invocations.” (Section 5.2, p.9)
7. at the last statement of every path (for example a return), ask whether its post-condition implies the function’s post-condition; if not, report a potential bug with the statement and the chain of conditions (Section 5.1, p.8)

the paper’s example (Figure 6, p.8), conditions shortened:

// {s is a non-empty string slice. gnu_extensions reflects the active language mode.}
let first = s.as_bytes()[0];
// {... first is the first byte of s.}
if !matches!(first, ... | b'l' | b'r' | ...) {
    // {... first is not in ('l', 'r', ...).}
    return None;
    // {... first is not in ('l', 'r', ...). The function return value is None.}
}

The last condition does not establish that s is not a keyword, so the return None is reported.

Verus form. Inference: Figure 6 is what a Verus proof looks like with assert(...) in place of each comment; the difference is that Z3 checks each implication and nothing is taken on the LLM’s word. Step 2 is Verus’s built-in treatment of calls. Step 4 needs no annotation. Step 7 is the ensures check at each return. A use that does carry over as a new thing: run the natural-language pass first as a cheap screen on unverified Rust, and spend proof effort where it reports nothing; a function it flags probably has a bug that would make the proof impossible anyway. What does not carry over: block grouping (step 6) trades precision for cost in FM-Agent, whereas in Verus larger blocks cost nothing in soundness, only in solver time.

evidence: the 522 bugs are the evidence for the pipeline as a whole. For this step alone there is only the confounded ablation quoted under technique 1.

where it fails or what it assumes: the 98.6% experiment tests predicting outputs for concrete inputs, which is not the same task as inferring a condition that holds for all inputs. The paper’s own wording of the result differs between sections: the introduction says “LLMs accurately predict the results for 98.6% of the functions.” (Section 1, p.2), while Section 2.3 gives 98.6% of cases, 438 of 444; with 3 inputs per function that is 148 functions (my division), and the per-function rate is not given. The paper does not say how many potential bugs this step raised before validation, so its false-alarm rate is unknown.

technique 4: for a loop, guess the post-condition first, then find an invariant that justifies it

what it is: an order of work. Classic practice writes the invariant and derives the loop’s post-condition; here the LLM states what holds after the loop, then looks for an invariant that proves it, and discards the post-condition if none is found.

how it is done (Section 5.2, pp.8-9):

1. the LLM generates the loop’s post-condition
2. it then proposes an invariant from the loop’s pre-condition, the body and that post-condition
3. the invariant must pass three checks: “The loop invariant should satisfy: 1) it should be implied by the pre-condition of the loop; 2) it should be maintained after each iteration of the loop; 3) the conjunction of the loop invariant and the negation of the loop condition should imply the post-condition of the loop.” (Section 5.2, p.8)
4. on failure: “If FM-Agent cannot find a valid loop invariant, the post-condition of the loop may be invalid.” (Section 5.2, p.8) It generates another post-condition and repeats.

The stated reason for the order: “This is because we observe that generating loop invariants is actually a more difficult task than directly generating the post-condition of the loop.” (Section 5.2, p.9)

Verus form. Inference: write assert(post) directly after the while first; Verus reports it as failing. Then add invariant clauses until three things hold, which are the paper’s three checks and which Verus reports separately: the invariant holds on entry, it holds at the end of the body, and the assert(post) after the loop passes from the invariant plus the negated condition. If no invariant can be found, weaken or correct post. What changes: Verus also wants a decreases clause to prove the loop terminates; the paper’s three checks are for partial correctness and say nothing of termination. Verus by default forgets, inside a loop, facts from before it that are not restated in the invariant; #[verifier::loop_isolation(false)] relaxes that.

evidence: none separate. The observation in the quoted sentence is reported without numbers.

where it fails or what it assumes: the paper does not say how the three checks are carried out (Inference: by the LLM in English, except where the SMT route of technique 5 applies); it gives no count of loops, of retries, or of loops for which no invariant was found. No limit on the number of post-condition retries is stated.

technique 5: use a formula only when the sentence translates without uninterpreted functions

what it is: an ambiguity test for a natural-language condition. Ask the LLM to translate it into a formula; if the formula needs a function symbol with no definition, the sentence was usually vague, and the formula is not used.

how it is done (Section 5.2, p.9):

1. translate the condition into a formula with an LLM
2. inspect the formula for uninterpreted functions, which can stand for concepts the sentence left undefined (the paper says an ambiguous condition will usually produce them)
3. if there are none, check the proof obligation with an SMT solver
4. otherwise stay in natural language: “Thus, if the generated formula contains some uninterpreted functions, FM-Agent will not use the formula to check the proof obligations, but will still reason about the natural language conditions.” (Section 5.2, p.9)

Verus form. Inference: the same test works when turning a requirement into requires/ensures. Each time the translation needs a spec fn whose body cannot be written from the requirement text, that name marks a question to put to the requirement’s author; a contract that mentions only defined spec fns and program variables is ready for the verifier. This is a practical trigger for the ask-don’t-guess rule; the paper does not use it that way.

evidence: none. The evaluation does not say how many conditions were translated, how many passed the test, or whether any bug was found or dismissed through the solver.

where it fails or what it assumes: Inference: a translation can be wrong without using an uninterpreted function (for example, a wrong inequality), so the test detects vagueness, not mistranslation.

technique 6: confirm each suspected bug with a test from the system’s entry point

what it is: before a potential bug is reported, an LLM must write an input for the whole system (a C program for a compiler, a query for a database) that makes the bug observable. The reasoning chain from technique 3 is given to it.

when to use: whenever the checker is unsound or incomplete and a failure cannot be told from a false alarm. The paper’s argument is that Hoare logic itself, on failure, cannot confirm a bug (Challenge III, p.2).

how it is done (Section 6, p.9; Section 3, p.4):

1. a developer, or an agent following markdown instructions, sets up the test environment
2. for each potential bug, the LLM writes a system-entry test case from the bug description and reasoning
3. run it; a crash is observed directly; a wrong result is detected by running the same input on a reference implementation (GCC for the compiler, DuckDB for the query engine) and comparing
4. with no reference, compare with the outcome the contract describes
5. retry up to N times: “If the bug cannot be triggered after N attempts to generate test cases, the potential bug will be marked as unconfirmed and will not be reported as a genuine bug.” (Section 6, p.9) N is 10 in the evaluation.
6. report only confirmed bugs: “The bug validator reports it to developers only when the test cases successfully trigger the potential bug within this limit.” (Section 3, p.4)

the worked case is Figure 3 (p.4): for the from_keyword bug the validator writes int main() { int *ptr_a = nullptr; return 0; }. A preliminary experiment precedes the design: on 10 known bugs in the same compiler, “We tell LLMs the reason why a function is buggy and ask LLMs to generate a C program to trigger the bug.” (Section 2.3, p.4), and all 10 were triggered; the call chain from entry to from_keyword has 7 functions.

Verus form. Inference: a Verus failure has the same ambiguity (wrong code, wrong contract, or missing proof), and verified Rust is still runnable Rust. So when a function resists proof after a set number of repairs, have the agent write a test through the crate’s public entry that would violate the ensures, and run it with the ordinary Rust test harness. A failing test settles that the code or the contract is wrong and gives the repair agent a concrete input; no failing test after N tries is weak evidence that the proof is what is missing. What does not carry over: FM-Agent drops unconfirmed suspicions, which is right for a bug finder; a verifier cannot drop an unproved obligation, so the test only directs the next step.

evidence: 522 confirmed bugs (Table 2, p.11): CCC 339, VibeTensor 141, VibeOS 23, Bespoke OLAP 19; the sum checks. Breakdown given: CCC 111 wrong IR, 68 wrong runtime output, 39 diagnostics, 14 crash or hang, 9 optimization, which add to 241 of 339, the paper calling these “some of the main bug types”; VibeOS 4 + 4 + 2 + 1 + 12 = 23; Bespoke OLAP 7 + 3 + 9 = 19; VibeTensor 50 + 51 + 19 + 3 = 123 of 141 (Section 9.2, pp.11-12).

where it fails or what it assumes: the paper does not report how many potential bugs entered validation, how many stayed unconfirmed, whether the 522 are deduplicated by root cause, or whether any was acknowledged or fixed by the systems’ developers. Inference: bugs with no reachable trigger from the entry point, and bugs in systems where step 4 is the oracle, are respectively missed and unreliable. “Note that 3 of 4 systems have already been well tested and fixed by their developers (Table 3).” (Section 9.2, p.11); for the fourth, VibeOS, testing details were not released.

technique 7: incremental re-reasoning after a change

what it is: rules for which contracts to update and which functions to re-check after an edit, driven by a natural-language statement of what the change is for.

how it is done (Section 7, pp.9-10):

1. obtain the developer goal: given by hand, or taken from commit messages or coding prompts
2. find relevant functions coarse to fine: an LLM splits the codebase into modules, summarises them and selects modules; an LLM selects files in those modules; a scoring heuristic ranks functions and keeps the top N
3. the score: “The relevance score of a function is a weighted sum of: 1) text overlap between the function and the developer goal description, 2) relevance scores of the function’s callers and callees, and 3) the relevance score of the class to which the function belongs.” (Section 7, p.10) If the top score is under a threshold, or a file has too many functions, an LLM re-ranks.
4. update contracts caller before callee, for modified, added and relevant functions; discard contracts of removed functions. For an existing function the LLM sees the current contract, the expected specification, the source and the goal, and decides whether and how to revise.
5. when a contract changes, revisit the expected specifications of its callees and push any change down; also update the expected specifications held by its callers
6. re-check by rule: “A function is subsequently re-reasoned about if it satisfies one of the following conditions: 1) it is modified or newly added, 2) its specification is updated, and 3) it calls a function whose specification is updated.” (Section 7, p.10)

The reason relevance is needed at all: an edit may omit a function that had to change, and that function is neither modified nor new (Section 7, p.9).

Verus form. Inference: rule 6 is the dependency rule of modular verification and holds in Verus: a function must be re-verified if its body changed, if its own requires/ensures changed, or if the contract of something it calls changed; one more case exists in Verus that the paper lacks, a changed spec fn body, which affects every function whose contract or proof mentions it. The relevance search (steps 2-3) has no Verus counterpart and is the useful import: after a requirement change, it proposes which contracts should have changed but did not.

evidence: none. Section 9 poses three questions (scale, bugs found, cost) and reports no incremental run; weights, thresholds and N for the score are not given.

numbers that do not agree, and claims wider than the data

• Function count: “The number of functions in each system ranges from 109 to 4,910.” (Section 9.1, p.11), but Table 1 (p.10) gives 4,957 for CCC; the table’s total of 8,549 is the sum using 4,957.
• Time: the abstract says the systems are reasoned about “within 2 days”, and the body says “Compositional reasoning of systems in Table 1 takes about 2 days and 3.4 billion tokens in total.” (Section 9.3, p.12) The figure is for all four together; no per-system time or cost is given. Inference: 3.4 billion tokens over 522 bugs is about 6.5 million tokens per reported bug (my division).
• Table 3 lists testing methods for three systems only (CCC, VibeTensor, Bespoke OLAP).
• The title and abstract speak of formal methods and Hoare-style reasoning; the SMT path (technique 5) and incremental reasoning (technique 7) are described and not evaluated.
• Inference: the claim to be the first framework for automated compositional reasoning at this scale rests on the choice not to compare with any tool: “We do not compare FM-Agent with existing verification tools, such as symbolic execution engines [5, 36], Verus [25, 26], and Dafny [27].” (Section 9.1, p.11) No LLM-based bug finder or code-review agent is compared either, apart from the paper’s own ablation.
• Figure 1’s signature names the parameter gnu_extension and has no return type, while the contracts in Figure 2 call it gnu_extensions; the figure is labelled simplified.

already done here; VL need not repeat it

• Inference: the demonstration that caller-side expectations expose bugs that body-derived contracts hide, with a worked case (from_keyword), and the layered call-graph schedule for generating contracts in parallel. Both can be adopted as described.
• Inference: what remains open and is VL’s ground is everything after the English contract: a formal statement, a checked proof, and a status for functions with no reported bug.

how far this competes with agent-written Rust verified by Verus

Inference: moderate as a substitute, low as a rival in kind. It needs no annotations, runs on existing C++, Python, CUDA and Rust (Section 9.1, p.11), found hundreds of bugs in systems their makers had tested, and its code is public; a team wanting more trust in agent-written code at low effort could stop there. It offers no guarantee, and its authors say so: “However, note that we do not claim FM-Agent can replace existing formal verification tools.” (Section 9.3, p.12) The weak point of a Verus-based product that this paper presses on is contract authoring at scale; its answer (caller-driven, top-down, in parallel) is one VL can take over and then make checkable.

techniques for the catalog

• caller-driven contract — write a function’s pre-condition from what call sites establish and its post-condition from what callers consume, merging callers by disjunction and conjunction, so a buggy body cannot define its own contract
• layered call-graph schedule — collapse recursion cycles, sort the call graph into layers from the entry points, and generate contracts for a whole layer in parallel
• natural-language Hoare pass — carry a prose condition through each block from the pre-condition and flag any exit whose condition does not imply the post-condition
• post-condition-first loops — state what holds after the loop, then search for an invariant meeting the three classic checks, and replace the post-condition if none is found
• uninterpreted-function ambiguity test — translate a prose condition to a formula and treat any undefined function symbol as a sign the prose is too vague to formalise yet
• system-entry bug confirmation — report a suspected violation only after a generated whole-system input reproduces it within N tries, using a reference implementation as oracle where one exists
• goal-driven incremental re-check — after an edit, find functions whose contracts should change from the stated goal, update caller before callee, and re-check changed functions and their callers

Last edited: 2026-10-13