FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning Haoran Ding
Zhaoguo Wang✉
Haibo Chen
Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University
arXiv:2604.11556v1 [cs.SE] 13 Apr 2026
Abstract
becomes crucial. However, as codebases grow, existing automated reasoning techniques struggle to scale because system code combines complex control flow, rich state manipulation, and deep inter-procedural dependencies. Compositional reasoning is a promising method to handle this problem. The basic idea is to reason about each small component separately and compose the reasoning for each component to reason about the entire system. Hoare logic [21] realizes this idea based on the Hoare triple {𝑃 } 𝐶 {𝑄 }, which uses two formulas 𝑃 and 𝑄 to define the formal specification of a code fragment 𝐶. The pre-condition 𝑃 specifies what must hold before executing the code 𝐶, and the postcondition 𝑄 specifies what will be ensured after 𝐶 terminates. If the specification of each function is given, Hoare logic enables developers to reason about each function independently and compose the proof for each function to imply the correctness of the whole system. This makes Hoare logic a strong foundation for compositional reasoning. However, despite Hoare logic laying the foundation for compositional reasoning decades ago, existing techniques still struggle to fully realize this potential, even for sequential programs. A critical bottleneck is the need for formal and human-written specifications. It requires heavy human effort and deep understanding for large-scale systems. For a long time, this bottleneck received little attention because writing proofs was seen as the heavier burden. Recent work [5, 12, 13, 15, 18–20, 25, 27, 33, 36–38, 45–47, 55–58] has made major progress in automating proof generation. As a result, specification generation is now one of the main challenges in automated reasoning for large-scale systems. This challenge is intensifying in the era of LLM coding agents (e.g., Claude Code [1], GitHub Copilot [16], OpenAI Codex [41], Cursor [4]). Since systems are developed automatically rather than manually, developers often lack a deep understanding of the generated code. Thus, it becomes more difficult to write accurate specifications. This paper presents FM-Agent, the first framework that enables automated compositional reasoning for large-scale systems. It leverages LLMs to generate specifications at function granularity. Each function can then be reasoned about concurrently under the principles of Hoare logic. However, realizing FM-Agent faces three key challenges: Challenge I: Specification generation must capture function behavior expected by the developer. However, existing methods [12] generate specifications from implementations, which may not capture the expected behavior, because the
LLM-assisted software development has become increasingly prevalent, and can generate large-scale systems, such as compilers. It becomes crucial to strengthen the correctness of the generated code. However, automated reasoning for largescale systems remains challenging due to code complexity. Hoare logic offers an approach to decomposing a large system into smaller components and reasoning about them separately (i.e., compositional reasoning). However, existing works still struggle to scale, because Hoare logic requires writing formal specifications for each function, imposing a heavy human burden. The problem is exacerbated when code is generated by LLMs, as developers lack a deep understanding of each function’s expected behavior and struggle to write accurate specifications. This paper presents FM-Agent, the first framework that realizes automated compositional reasoning for large-scale systems. Leveraging LLMs, FM-Agent introduces a topdown paradigm to automatically generate function-level specifications. Specifically, FM-Agent derives the specification of a function from how its callers expect the function to behave, so the generated specifications can reflect the developer’s intent of a function even if the implementation is buggy. Developers’ intent is usually expressed in natural language, while existing verifiers only support formulas. Therefore, FM-Agent generalizes Hoare-style inference to reason about functions against natural-language specifications. Finally, to confirm bug existence and explain bug causes, FM-Agent automatically generates test cases to trigger potential bugs. In our evaluation, FM-Agent successfully reasons about large-scale systems within 2 days, each of which has up to 143k LoC. These systems have already been tested by their developers, but FM-Agent still finds 522 newly discovered bugs. These bugs can cause serious consequences, including system crashes and incorrect execution results.
1
Introduction
LLM-assisted software development has become increasingly popular and can even generate systems with more than 100k LoC, such as the compiler CCC [3]. However, due to hallucinations of LLMs, the generated code may contain bugs. Thus, reasoning about the correctness of such large-scale systems ✉ Corresponding author.
1
implementation itself may be buggy or may fail to reflect original design intent. Challenge II: Developers’ intent is naturally expressed in natural language, whereas existing verifiers reason only about formulas. Specifically, developers usually write documents in natural language to describe the design of the whole system. In the era of LLMs, prompts for code generation are also usually written in natural language. However, existing verifiers support only formal specifications and cannot be applied. Challenge III: If verification via Hoare logic inference rules fails, verifiers cannot tell bug causes, which is important for bug fixing. This challenge stems from the undecidability of program verification: no verifier can ensure both soundness and completeness. Hoare logic ensures soundness without completeness and cannot even confirm the existence of bugs when verification fails. To tackle these challenges, FM-Agent proposes approaches based on three key insights: Insight I: LLMs can better capture the expected behavior of a function based on how its callers use it. Then, FM-Agent proposes a top-down paradigm to generate specifications. To capture the design intent of each function, FM-Agent uses LLMs to analyze the implementation of its caller to generate pre-conditions and post-conditions for the function. For example, the arguments passed by the caller can help infer the pre-condition, and the subsequent code after invoking the callee can help infer its post-condition. If a function is invoked by multiple callers, FM-Agent merges the expected behavior inferred from each caller to generate a more comprehensive specification. In this way, FM-Agent will not be misled by buggy implementations. Insight II: LLMs are able to accurately predict the execution results of small code blocks. For example, we generate random inputs and use LLMs to infer the outputs of functions from Microsoft VerusBench [34], a benchmark of Rust verification. LLMs accurately predict the results for 98.6% of the functions. This insight enables FM-Agent to directly perform reasoning against natural language specifications. This is because LLMs understand both code semantics and natural language. Specifically, FM-Agent generalizes Hoare logic inference rules to support natural language pre-conditions and postconditions. Then, from the pre-condition in the specification, FM-Agent uses LLMs to iteratively infer the post-condition of statements. If the post-condition of the last statement in an execution path cannot imply the post-condition in the specification, FM-Agent reports a potential bug. Insight III: LLMs can capture the correlation between the system entry input and internal function behavior. Test cases that trigger bugs provide rich information for bug fixing. Some commonly used methods, such as unit testing, focus on test cases for individual functions. They cannot capture the correlation between system-entry inputs and bugs in internal functions. This insight enables FM-Agent to generate
test cases at the system-entry level instead of the function level. System-entry inputs are more intuitive for developers and less likely to obscure the root cause. Thus, FM-Agent iteratively generates test cases based on the reasoning process and runs test cases against the system to confirm whether the predicted bug is genuine. In our evaluation, FM-Agent reasons about multiple largescale systems within 2 days, whose sizes range from 11k to 143k LoC. The systems are automatically developed by various coding agents in different programming languages. FM-Agent still finds 522 newly discovered bugs even though their developers have already used various methods to test and fix these systems, such as unit testing, integration testing, differential checks, and multi-agent code review. These bugs can lead to serious issues, such as system crashes and incorrect query results.
2
Hoare Logic Meets LLMs
This section introduces how Hoare logic enables compositional reasoning (Section 2.1) and why existing works struggle to scale to large systems (Section 2.2). 2.1
Hoare-Style Compositional Reasoning
The core of Hoare logic is the Hoare triple: {𝑃 } 𝐶 {𝑄 } It means that if 𝑃 holds before executing command 𝐶, then 𝑄 holds after executing 𝐶. For example, {𝑥 > 0} 𝑦 := 𝑥 + 1 {𝑦 > 1} is a valid Hoare triple. At the function level, Hoare triples serve as contracts: a function’s pre-condition and postcondition together specify its expected behavior. Callers must establish the pre-condition and may assume the postcondition, while the callee must ensure that its body satisfies the post-condition whenever the pre-condition holds. This separation of concerns enables compositional reasoning: each function can be verified independently against its contract, and the resulting local proofs compose into end-to-end guarantees for the entire program. Thus, based on compositional reasoning, Hoare logic becomes a promising foundation for scalable verification. Hoare logic provides many inference rules to realize compositional reasoning. For example, the following rule means that if both Hoare triples above the line hold, then the triple below the line also holds. {𝑃 } 𝐹 1 {𝑅} {𝑅} 𝐹 2 {𝑄 } {𝑃 } 𝐹 1 ; 𝐹 2 {𝑄 } One then proves {𝑃 } 𝐹 1 {𝑅} and {𝑅} 𝐹 2 {𝑄 } independently in parallel. The rule then directly composes them to prove the larger code fragment 𝐹 1 ; 𝐹 2 . Although Hoare logic has provided a solid theoretical foundation, realizing compositional reasoning in large-scale systems remains difficult. Hoare-style verification requires formal specifications for all 2
functions, which requires deep domain expertise and manual effort.
1 pub fn from_keyword ( s : & str , gnu_extension : bool ) { 2 let first = s . as_bytes () [0]; 3 // Fast reject by first character : keywords
2.2
4 5 6 7 8 9 10 11 12 }
Existing Automated Reasoning Techniques
We first introduce the limitations of traditional verification techniques and then discuss recent works that leverage LLMs to assist formal verification. Automated and semi-automated verification. Symbolic execution [5, 36–38, 45, 46, 56] explores many feasible paths with symbolic inputs and checks desired properties on each path. It can realize completely automated verification. But it faces the issue of path explosion, which means that the number of paths grows quickly with massive branches and loops. It also cannot handle some program structures, such as unbounded loops. A loop is unbounded if the number of iterations cannot be determined statically, which is common in systems. To handle the limitations of symbolic execution, semi-automated verifiers [13, 15, 18–20, 25–27, 33, 47, 57, 58] ask developers to provide annotations to assist the verification, which have stronger verification capabilities. Developers need to manually write specifications for each function and some proofs, such as loop invariants and assertions. Then, the verifier automatically generates and checks proof obligations based on SMT solvers. However, manually writing these annotations requires substantial human effort, especially for large systems with many functions and complex logic. This limits the scalability of these verifiers.
Figure 1. An example of a buggy Rust function simplified from a C compiler [3] developed by Anthropic. Pre-condition: - “s” is a valid UTF-8 string. - “gnu_extensions” is a boolean that indicates if GNU C extension keywords should be recognized. Post-condition: - Returns Some(TokenKind::T) if and only if “s” exactly matches a known C/GCC keyword. - Returns None if “s” does not match any recognized keyword, including: 1) the first byte of “s” is not one of the 16 permitted starting characters regardless of “gnu_extensions”. 2) …
(a) The specification generated based on the implementation, which is buggy. The bolded part is incorrect. Pre-condition: - “s” is a non-empty string slice. - “gnu_extensions” reflects the active language mode.
LLM-assisted verification. Recent work [12, 24, 55] has explored using large language models (LLMs) to automatically reduce the manual effort of semi-automated verification. For example, AutoVerus [55] leverages LLMs to infer loop invariants from code. This alleviates part of the annotation burden. However, developers must still manually provide formal pre-conditions and post-conditions for each function, so these approaches cannot fully realize automated compositional reasoning. Some other works [12, 24] go further by using LLMs to generate function specifications as well. However, they heavily rely on analyzing the program implementation, which reflects the implementation behavior rather than the expected behavior from developers. The limitations of these works are further exacerbated in the era of LLM-based coding agents for two reasons. First, LLMgenerated code may contain subtle bugs that specificationfrom-implementation methods cannot detect. Second, developers often lack a deep understanding of code they did not write, which makes it less feasible to manually write specifications. In our scenario, we need to automatically generate specifications that reflect the design intent of developers regardless of implementation bugs. 2.3
only start with these 16 chars . if ! matches !( first , ... | b 'l ' | b 'r ' | ...) { return None ; } match s { " auto " = > Some ( TokenKind :: Auto ) , ... _ = > None , }
Post-condition: - Returns Some(token_kind) if “s” is a reserved keyword. The keyword set covers C standard keywords for C89 through C23, ... - Returns None for all other identifiers.
(b) The specification generated based on callers, which is correct. The bolded part fixes the error in the buggy specification.
Figure 2. Specifications generated for the from_keyword function in Figure 1 using two methods.
First, LLMs can better capture the expected behavior of a function based on how its callers use it. When writing caller functions, developers or LLMs usually have a clear intent of how callee functions should behave. Thus, generating the specification of the callee based on the caller’s implementation and specification can better capture the expected behavior. For example, the invocation parameters from callers can help infer the callee’s pre-condition. The subsequent code manipulating the output of the callee in callers can help infer the callee’s post-condition. In this way, the generated specification is less likely to be misled by the buggy implementation of the callee itself.
Insights and Our Approach
To handle the limitations of prior works, FM-Agent is motivated by the following insights: 3
from entry function to the buggy function from_keyword in Figure 1 contains 7 functions. This insight is useful for bug fixing, because if we can directly generate system entry inputs rather than function-level inputs, developers can easily understand the root cause and fix the bugs. Thus, FMAgent provides a function-level reasoning process for LLMs to generate system-entry inputs that trigger function bugs. For example, the post-condition of line 5 in Figure 1 is that the return value is None and “s” does not start with those 16 characters. It cannot imply the post-condition in the specification shown in Figure 2b. Based on the reasoning process, the bug validator successfully generates a C program shown in Figure 3. The program uses a keyword “nullptr” that starts with a character other than the 16 characters, which cannot be recognized by from_keyword due to the fast rejection code.
1 int main () { 2 int * ptr_a = nullptr ; 3 return 0; 4 }
Figure 3. A test case generated by Claude Code to trigger the bug in Figure 1. For example, Figure 1 shows a buggy function simplified from a C compiler called CCC [3], which is generated by Anthropic using Claude Code. The function checks whether a string “s” is a keyword of C. It fast rejects “s” by checking the first character of “s”, and then checks whether the whole string matches any keyword in match arms. However, it incorrectly rejects some keywords that start with characters other than the 16 characters in the fast rejection condition, such as “nullptr”. Figure 2a shows the specification generated by Claude Code merely based on the implementation of from_keyword. It is clear that the specification is misled by the incorrect fast rejection code, which only considers keywords starting with the 16 characters as valid keywords. As a result, the subsequent reasoning process based on this specification will miss the bug. In contrast, Figure 2b shows the specification generated based on the caller of from_keyword. Compared with the specification in Figure 2a, it does not claim that only keywords starting with the 16 characters are valid keywords. Thus, it allows the subsequent reasoning process to find the bug.
3
FM-Agent Overview
Figure 4 shows the workflow of FM-Agent, which automatically generates specifications and performs compositional reasoning. The specification generator (Section 4) produces pre-conditions and post-conditions for each function. It first determines the order in which specifications are generated. This order is a partial order rather than a total order, which enables FM-Agent to generate specifications for multiple functions concurrently. As a result, the specification generator can scale to large-scale systems. Then, for each function, the specification generator uses LLMs to derive the specification from three sources: the function’s implementation, the expected behavior from callers, and domain knowledge (e.g., the C standard for compiler systems). After generating specifications, the code reasoner (Section 5) checks whether each function’s implementation is consistent with its specification. It generalizes the inference rules of Hoare logic to operate over natural-language specifications and leverages LLMs to perform the reasoning. Based on the principle of Hoare-style compositional reasoning, the code reasoner verifies each function concurrently and independently. FM-Agent currently supports only sequential functions, not concurrent functions. Finally, the bug validator (Section 6) generates test cases and executes them to trigger potential bugs. Note that it is impossible to completely avoid hallucinations of LLMs. As a result, the code reasoner may produce false positives, i.e., cases where correct code is flagged as buggy. Thus, we set a threshold to limit the number of attempts at test-case generation. The bug validator reports it to developers only when the test cases successfully trigger the potential bug within this limit.
Second, LLMs are able to accurately predict the execution results of small code blocks. For example, we perform a preliminary experiment based on all functions in VerusBench [34], a popular benchmark of Rust verification developed by Microsoft. 98% of the functions in VerusBench have loops. For each function, we randomly generate 3 inputs and use Claude Code to predict the execution results. 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. Thus, the insight enables stepwise Hoare-style reasoning in natural language: starting from the function’s pre-condition, we use the LLM to infer the post-conditions of each small code block (e.g., a statement) and feed them as the next code block’s pre-condition. If the final post-condition of an execution path cannot satisfy the post-condition in the specification, we can report a potential bug. Third, LLMs can capture the correlation between the system entry input and internal function behavior. We perform a preliminary experiment based on 10 bugs in a C compiler called CCC [3]. We tell LLMs the reason why a function is buggy and ask LLMs to generate a C program to trigger the bug. Even if the buggy function may be far from the compiler entry, LLMs still successfully understand the workflow and trigger all 10 bugs. For example, the call chain
4
Specification Generator
Given a system codebase, the specification generator satisfies two key requirements. First, for each function, the generated 4
Bug Report
System Code FM-AGENT 1
Step1: Determine Generation Order
Specification Generator
Spec + Code 2
Step2: Generate the Specification of Each Function F
Code Reasoner
3
Bug Validator
Step3: Reason against Natural Language Spec
Step4: Trigger Potential Bugs
Pre-Condition Statements
Test Cases Generator & Checker
Hoare-Style Inference
Test Case
Implementation of F Expected Behavior
Potential Bugs
Spec of F
Domain Knowledge
Execution Result
Testing Environment
Post-Condition
Figure 4. The workflow of FM-Agent. specification describes its expected behavior rather than the implementation steps. Second, the specification generator fully exploits the concurrency potential of generating specifications for massive functions. It allows FM-Agent to be scaled to large codebases. 4.1
F2
F1:
F3
F1⊢{PF2} F2 {QF2}
F2:
Basic Idea
F2⊢{PF4} F4 {QF4}
Before introducing more details, we define expected behavior from caller functions as a new concept called expected specification.
F4:
Definition 1 (Expected Specification). Assume a caller function 𝐹 1 invokes a callee function 𝐹 2 . The following formula represents that the expected specification of 𝐹 2 from 𝐹 1 is {𝑃 }𝐹 2 {𝑄 }. 𝐹 1 ⊢ {𝑃 }𝐹 2 {𝑄 }
… …
F: Function Body
F1⊢{PF3} F3 {QF3}
F4
F3:
F5 F2⊢{PF5} F5 {QF5}
F5:
F5 … F3 ⊢ {P’F5} F5 {Q’F5}
… …
F
F ⊢ {P} C {Q}
Function Call
Expected Spec
Figure 5. An example of the top-down paradigm for specification generation. Each directed edge from function 𝐹𝑖 to function 𝐹 𝑗 indicates that 𝐹𝑖 invokes 𝐹 𝑗 . The specification of 𝐹 𝑗 is generated based on the expected specification from all its callers 𝐹𝑖 , which is denoted as 𝐹𝑖 ⊢ {𝑃 }𝐹 𝑗 {𝑄 } on the edge.
Specifically, the formula means that: 1) the implementation of 𝐹 1 ensures that the program state immediately before the invocation of 𝐹 2 satisfies the condition 𝑃, and 2) the subsequent code of 𝐹 1 requires that the program state immediately after the invocation of 𝐹 2 satisfies the condition 𝑄. The specification generator proposes a new top-down paradigm to automatically generate specifications. Figure 5 shows the basic idea of the paradigm. It starts from generating specifications for the entry functions (i.e., F1 ). Using LLMs, FM-Agent analyzes the function implementation and domain knowledge of the whole system to generate the specification for the entry function. Furthermore, FM-Agent also generates the expected specifications for all its callees F2 and F3 , which are denoted by 𝐹 1 ⊢ {𝑃𝐹 2 }𝐹 2 {𝑄 𝐹 2 } and 𝐹 1 ⊢ {𝑃𝐹 3 }𝐹 3 {𝑄 𝐹 3 }, respectively. Then, FM-Agent proceeds down the invocation graph. Each function is processed after the specifications of all its callers are generated. For each non-entry function, FM-Agent generates its specification based on the expected specifications from its callers, the
function implementation, and the domain knowledge. Particularly, if a function is invoked by multiple caller functions, FM-Agent combines the expected specifications from all its callers to generate its specification such that the generated specification can capture the expected behavior of the function in different invocation contexts. For example, F5 has two callers F2 and F3 . Its specification is generated by combining 𝐹 2 ⊢ {𝑃𝐹 5 }𝐹 5 {𝑄 𝐹 5 } and 𝐹 3 ⊢ {𝑃𝐹′ 5 }𝐹 5 {𝑄 𝐹′ 5 }. 4.2
Deciding Specification Generation Order
We now describe how to determine the specification generation order, which is essential for enabling concurrent 5
algorithm replaces all cross-SCC edges with edges between the corresponding condensed nodes. Finally, it performs a layered topological sort on the condensed DAG (Algorithm 1–Algorithm 1). It first calls getIndegree to compute the in-degree of every node in ⟨𝑉 ′, 𝐸 ′ ⟩ (Algorithm 1) and initializes a set Q with all zero-in-degree nodes (Algorithm 1). The initial Q represents all entry functions without callers in the system. In each iteration, the current Q becomes the next layer L𝑘 . The algorithm then calls GetSucc to enumerate each successor of nodes in L𝑘 (i.e., their callees), and decrements their in-degrees. If any successor’s in-degree drops to zero, it is added to the next Q for processing in the next iteration. The process repeats until Q is empty, yielding [L1, L2, . . . , L𝑘 ]. During specification generation, FM-Agent processes the layers from L1 (the entry functions) to L𝑘 . This ensures that, when generating the specification for a function, the specifications of all its callers outside its SCC (if any) have already been generated. Functions within the same layer are generated concurrently. For functions that share an SCC, they are in the same layer. FM-Agent generates their specifications simultaneously. Section 4.3 discusses how specifications are generated for functions within the same SCC. To further improve efficiency, FM-Agent leverages batching and phase-level concurrency. The specification generator can batch the specification generation for functions in the same layer. Assume the batch size is 𝑁 , the specification generator groups the prompts for up to 𝑁 functions in the same layer into a single batch and sends them to LLMs together. This can reduce network round trips and improve overall throughput. The batch size 𝑁 can be tuned for different codebases and models. Too large a batch may increase latency and degrade inference quality, while too small a batch may underutilize available concurrency. Phase-level concurrency means that some systems naturally consist of multiple self-contained phases, where each phase can be processed independently and concurrently. This is because, for each phase, most functions only invoke functions in the same phase. For example, a compiler can be split into multiple self-contained phases, such as lexing, parsing, IR generation, optimization, and executable file generation.
Algorithm 1: Determining Specification Generation Order Input: A set of functions F in the codebase. Output: A sequence of function layers [L1 , L2 , . . . , L𝑘 ], where each layer L𝑖 is a function set. 3 OrderPlanner(F): 4 ⟨𝑉 , 𝐸 ⟩ := ConstructCallGraph(F) 5 𝑆𝐶𝐶𝑠 := FindSCCs(⟨𝑉 , 𝐸 ⟩) 6 ⟨𝑉 ′ , 𝐸 ′ ⟩ := CondenseGraph(⟨𝑉 , 𝐸 ⟩, 𝑆𝐶𝐶𝑠) 7 𝐼 := getIndegree(⟨𝑉 ′ , 𝐸 ′ ⟩) 8 Q := {𝑣 ∈ 𝑉 ′ | 𝐼 (𝑣) = 0} 9 𝑘 := 0 10 while Q ̸= ∅ do 11 𝑘 := 𝑘 + 1 12 L𝑘 := Q 13 Q := ∅ 14 foreach 𝑣 ∈ L𝑘 do 15 foreach 𝑢 ∈ GetSucc(𝑣, ⟨𝑉 ′ , 𝐸 ′ ⟩) do 16 𝐼 (𝑢) := 𝐼 (𝑢) − 1 17 if 𝐼 (𝑢) = 0 then Q := Q ∪ {𝑢 } 18 return [L1 , L2 , . . . , L𝑘 ] 1 2
generation across large-scale systems. Because some functions are independent of one another, the generation order is a partial order rather than a total order: functions in the same layer of Figure 5 can be processed concurrently, as they depend only on the specifications of functions in earlier layers. For instance, the specifications of F2 and F3 can be generated concurrently once the specification for F1 is ready. Algorithm 1 presents the order-planning algorithm. Given a set of all functions F in the system, the algorithm produces a layered sequence [L1, L2, . . . , L𝑘 ], where each L𝑖 is a set of functions whose specifications can be generated concurrently. The sequence guarantees that every caller of a function in L𝑖 belongs to some layer L 𝑗 with 𝑗 ≤ 𝑖; equality holds only when the caller and callee invoke each other. Therefore, FM-Agent can follow the top-down paradigm by processing the layers in order, from L1 to L𝑘 . The algorithm proceeds in four steps. First, ConstructCallGraph constructs a function call graph ⟨𝑉 , 𝐸⟩ from F (Algorithm 1), where each node represents a function and a directed edge from 𝐹 1 to 𝐹 2 indicates that 𝐹 1 invokes 𝐹 2 . Second, FindSCCs identifies all strongly connected components (SCCs) in the call graph (Algorithm 1). An SCC is a maximal subgraph in which every node is reachable from every other node. This step is necessary because recursive function invocation can construct cycles. The specification of functions in the same SCC will be generated simultaneously, as their specifications are interdependent. Third, CondenseGraph condenses the call graph by collapsing each SCC into a single node, yielding a directed acyclic graph ⟨𝑉 ′, 𝐸 ′ ⟩ (Algorithm 1). Because functions in the same SCC will be specified simultaneously, the algorithm treats them as one unit for ordering purposes. The
4.3
Generating Caller-Driven Specifications
For each function, the specification is derived by LLMs from three sources: 1) domain knowledge of the system, 2) expected specifications from callers (Definition 1), and 3) the function implementation. For entry functions, FM-Agent uses only sources (1) and (3); for internal functions, FMAgent uses all three sources. Domain knowledge helps LLMs understand the expected behavior of the system, so they can generate accurate specifications, especially for new kinds of systems. For example, when reasoning about a C compiler, the domain knowledge about the C standard can help LLMs understand what C 6
programs are valid. If the system is common, domain knowledge can be summarized from standards. If the system is new, developers can write documents that provide the necessary domain knowledge for LLMs. However, such documents may be very long, so providing all of them to LLMs is often impractical because of context window limits. We also observe that systems are usually modular, and different modules require different domain knowledge. For example, in a C compiler, the lexer and IR modules rely on different knowledge. Therefore, before specification generation, we use LLMs to analyze system components and split domain knowledge into separate files by component relevance. When generating the specification for functions in a component, FM-Agent only provides the domain knowledge that is relevant to the component to LLMs. For each function, after generating its own specification, FM-Agent also generates expected specifications for its callees. These expected specifications, defined in Definition 1, are natural-language pre/post conditions that guide the next layer. If a function is invoked by multiple callers, FM-Agent combines all caller-provided expected specifications to construct a comprehensive specification. The basic idea of combination is shown as follows.
Based on the above method, the specification generator finally generates a separate file for each function, which contains three parts. The first part is the function specification, including the pre-condition and post-condition in natural language. The second part is the expected specifications for its callees, which are also in natural language. The third part is the function body. FM-Agent will reason about each function against the specification concurrently (Section 5). 4.4 Top-Down vs. Bottom-Up Traditionally, when manually writing specifications, some developers prefer a top-down manner while others prefer a bottom-up manner. In the bottom-up manner, developers first write specifications for callee functions and then for their callers. There is no clear consensus on which manner is better for manually written specifications. In this subsection, we first explain why some developers favor the bottomup manner when manually writing specifications, and then discuss why the top-down manner is more suitable when automatically generating specifications, especially for LLMgenerated code. Developers who manually write specifications may prefer the bottom-up manner for two reasons. First, because systems are traditionally developed by hand, developers usually have a clear understanding of the semantics of each function and the system as a whole. With this understanding, they can capture the intended function behavior regardless of whether they work top-down or bottom-up, even when the implementation contains bugs. Second, the bottom-up manner avoids the need to directly write a formal specification for the entire system at the outset, which can be difficult because formal specifications are precise and may involve many details. Instead, the specification of a caller function can reuse the formulas or data structures already defined in the specifications of its callees, reducing the overall burden. In particular, recent layer-based verification methods [17] make bottom-up specification writing especially natural. These methods split the system into multiple layers, where upper-layer functions invoke lower-layer functions, and verify each layer in turn. Because sub-formulas and data structures from a lower-layer specification are typically reused when reasoning about the upper layer, writing specifications in a bottom-up manner aligns well with this verification strategy. However, when we aim to automatically generate specifications or the code is produced by LLMs, the two reasons above no longer hold, and the top-down manner becomes more suitable. First, when the code is written by LLMs rather than humans, developers lack a deep understanding of the expected behavior of each function, so the first reason no longer applies. Second, the implementation may contain bugs, which can mislead specification generation under the bottom-up manner: because callee specifications are generated before those of their callers, they are derived primarily
𝐹 1 ⊢ {𝑃1 }𝐹 {𝑄 1 } . . . 𝐹𝑛 ⊢ {𝑃𝑛 }𝐹 {𝑄𝑛 } 𝑃𝐹 ≔ (𝑃1 ∨ . . . ∨ 𝑃𝑛 ) 𝑄 𝐹 ≔ (𝑄 1 ∧ . . . ∧ 𝑄𝑛 ) Specifically, assume a function 𝐹 is invoked by 𝑛 callers 𝐹 1, . . . , 𝐹𝑛 . Given the expected specifications from all callers, we can combine them to derive the specification for 𝐹 . The pre-condition 𝑃 𝐹 is the disjunction 𝑃1 ∨ . . . ∨ 𝑃𝑛 , because 𝐹 may be invoked from the context of any caller 𝐹𝑖 . The post-condition 𝑄 𝐹 is the conjunction 𝑄 1 ∧ . . . ∧ 𝑄𝑛 , because 𝐹 should satisfy the expected post-conditions from all of its callers simultaneously. Note that the formula just illustrates the basic idea of combination. The actual combination is implemented by LLMs rather than directly concatenating sub-formulas by ∨ and ∧, because 𝑃𝑖 and 𝑄𝑖 are expressed in natural language rather than formulas. Combining naturallanguage specifications is more complex than combining formal specifications. It may require understanding the semantics of the specifications and rephrasing them if there are redundancies or potential conflicts. Although a function implementation may be buggy, it can still provide useful information. In particular, entry functions have no callers, so their specifications are mainly based on domain knowledge and implementation. The implementation is also useful for functions in the same call-graph cycle, which invoke each other. When generating specifications for a function in a cycle, FM-Agent lacks the expected specifications from its callers in the same cycle. This is because these functions are placed in the same layer, as described in Section 4.2. Thus, for a function in a cycle, the implementations of its callers in that cycle help LLMs infer the function’s expected behavior from their perspective. 7
from potentially buggy implementations. In contrast, the topdown manner generates caller specifications first, capturing expected behavior from the perspective of the whole system even when implementations are buggy. Third, automatically generated specifications are typically expressed in natural language, which tolerates fewer details than formal specifications; thus the second reason no longer applies either. With the top-down manner, specifications can be generated starting from the entry functions and progressively introducing more details for inner functions as needed.
5
1 // {" s " is a non - empty string slice . "
gnu_extensions " reflects the active language mode .} 2 let first = s . as_bytes () [0]; 3 // {" s " is a non - empty string slice . " gnu_extensions " reflects the active language mode . " first " is the first byte of s .} 4 if ! matches !( first , ... | b 'l ' | b 'r ' | ...) { 5 // {" s " is a non - empty string slice . " gnu_extensions " reflects the active language mode . " first " is the first byte of s . " first " is not in ( ' l ', 'r ', ...) .} 6 return None ; 7 // {" s " is a non - empty string slice . " gnu_extensions " reflects the active language mode . " first " is the first byte of s . " first " is not in ( ' l ', 'r ', ...) . The function return value is None .} 8 }
Code Reasoner
For each function, the input of the code reasoner includes the function implementation, its natural language specification, and the expected specifications for all of its callees. The code reasoner reasons about whether the implementation of the function is consistent with its specification via Hoare-style inference. 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.
Figure 6. The reasoning process of the function from_keyword in Figure 1. For brevity, we only show the code fragment that contains the bug. Every comment is the post-condition of the preceding code and the pre-condition of the following code. 5.2
Post-Condition Inference
Now we introduce the details of inferring the post-condition, which is derived from the pre-condition and the statement itself. The pre-condition of the first statement is the precondition in the function specification. The pre-condition of 5.1 Basic Idea the subsequent statements is derived from the post-conditions As described in Section 2.3, FM-Agent leverages LLMs to of the previous statements. With the pre-condition, FMreason about the implementation directly against natural Agent generalizes different Hoare logic inference rules to language specifications. The basic idea is to generalize Hoareinfer the post-condition for different types of statements. style inference rules to generate natural language post-conditions For simplicity, we only explain the inference method for for statements. Then, the code reasoner checks whether the some important types of statements. The inference method post-condition of the last executed statement in each execuof other statements is similar to Hoare logic inference rules, tion path implies the post-condition of the function, such which are omitted. as a return statement. If the check fails, it indicates that the implementation of the function may be inconsistent with its Branch statement. The post-condition is the disjunction specification, which will be reported as a potential bug. The of the natural language post-conditions of all branches. This report includes the specific statement where the violation is consistent with the classic Hoare-style inference rules for occurs and the reasoning process. if-else statements, except that the pre-conditions and postFor example, Figure 6 shows the reasoning process of the conditions are in natural language rather than formulas. function from_keyword in Figure 1. The code reasoner gen{𝑃 ∧ 𝐶}𝐶 1 {𝑄 1 } {𝑃 ∧ ¬𝐶}𝐶 2 {𝑄 2 } erates the post-condition for each statement based on the {𝑃 }𝑖 𝑓 (𝐶) 𝐶 1 𝑒𝑙𝑠𝑒 𝐶 2 {𝑄 1 ∨ 𝑄 2 } pre-condition and the statement itself. The pre-condition of the first statement comes from the specification (Figure 2b). Loop statement. For a loop statement, FM-Agent first The post-condition of the first statement adds a new propogenerates the post-condition of the loop via LLMs. Then, it sition: first is the first byte of s. Then, the if statement tries to generate a loop invariant based on the pre-condition further constrains first to be outside a character set. FMof the loop, the loop body, and the generated post-condition. Agent then checks whether the post-condition of the reThe loop invariant should satisfy: 1) it should be implied turn statement entails the post-condition in the specification, by the pre-condition of the loop; 2) it should be maintained which is “if s is a keyword, return Some; otherwise return after each iteration of the loop; 3) the conjunction of the None”. The entailment fails because the inferred condition is loop invariant and the negation of the loop condition should insufficient to establish the “otherwise return None” branch. imply the post-condition of the loop. If FM-Agent cannot Accordingly, FM-Agent reports the return statement as a find a valid loop invariant, the post-condition of the loop may potential violation site. be invalid. FM-Agent will generate another post-condition 8
for the loop and repeat the above process. Traditionally, developers usually first write a loop invariant and then use the loop invariant to derive the post-condition of the loop. FM-Agent adopts a different order, which first generates the post-condition of the loop and then tries to find a loop invariant to validate the post-condition. This is because we observe that generating loop invariants is actually a more difficult task than directly generating the post-condition of the loop. The post-condition just needs to hold after the loop, while the loop invariant needs to hold before and after each loop iteration. Section 2.3 also shows that LLMs can accurately predict the results of functions with loops. In practice, reasoning about statements one by one may lead to numerous invocations of LLMs, which can be slow and expensive. Thus, FM-Agent does not infer the postcondition for every single statement. It groups statements into larger blocks and reasons about them collectively, reducing the number of LLM invocations. This works due to the insight that LLMs are able to accurately predict the execution results of small code blocks, which has been illustrated in Section 2.3. For example, FM-Agent can directly put the code block in Figure 6 into the prompt and ask LLMs to infer the post-condition of the whole code block, which can save multiple invocations of LLMs for each statement in the code block. Although FM-Agent directly performs reasoning based on natural language pre-conditions and post-conditions, it can still be combined with formal methods to enhance the precision of the reasoning process. Specifically, if a condition is precise enough, FM-Agent can use LLMs to translate it into formulas. Then, FM-Agent can use an SMT solver to check the proof obligations, which can be more precise than reasoning based on natural language. To check whether a natural language condition is precise enough, we observe that if a natural language condition is ambiguous, the generated formula will usually contain some uninterpreted functions, which can represent the ambiguous concepts 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.
6
managed by agents, it is easy to add extra steps before executing FM-Agent. 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. N can be set by developers, which is 10 in our evaluation. This can help reduce false positives caused by LLM hallucinations. The specific test case generation and bug confirmation strategies vary across systems, but FM-Agent handles them automatically using LLMs based on the description of potential bugs. For example, when checking bugs of a C compiler in our evaluation (Section 8), the bug validator generates a C program as the test case, compiles it with the target compiler, and checks whether the expected bug is triggered. Bugs such as compilation crashes can be directly observed, while incorrect compilation results are detected by compiling the same program with a reference compiler implementation (e.g., GCC) and comparing the outputs. Similarly, when checking bugs of a SQL query engine, the bug validator executes the generated test cases and compares the results against a reference implementation (e.g., DuckDB). For systems without a reference implementation, FM-Agent instead checks execution results against the expected outcomes described in the specifications.
7
Implementation
We implement FM-Agent in Python, and the implementation consists of three components: a specification generator, a code reasoner, and a bug validator. Directly invoking LLMs will usually be limited by TPM (tokens per minute) and RPM (requests per minute), which limits the concurrency of FMAgent. Thus, all three components invoke LLMs via OpenRouter [51], which is a proxy for LLM services and supports much higher concurrency. For each function, the specification generator writes the implementation, specification, and expected specifications of each callee into a separate file. The code reasoner takes such a file as input and reports potential bugs in JSON files. The bug validator takes JSON files as input and generates test cases to validate potential bugs. Different systems use different programming languages and test-case execution commands. To easily generalize FM-Agent to various systems, we write some markdown files to guide an agent called OpenCode [50] and integrate it with other code in FMAgent to execute the workflow. For example, it will generate different parsers for various programming languages and autonomously run test cases on different systems.
Bug Validator
To confirm the potential bugs and help understand the bug causes, FM-Agent designs a bug validator. As described in Section 3, for each potential bug, the bug validator first leverages LLMs to generate a test case. Then, it executes the test case on the system and checks the output. The testing environment can be manually set up by developers in advance. Note that FM-Agent also supports developers writing markdown files to guide agents in setting up the testing environment. Since the overall workflow of FM-Agent is
8
Evaluation
The evaluation aims to answer the following questions: 1) Could FM-Agent scale to real-world large-scale systems? 2) How many newly discovered bugs could FM-Agent effectively detect in large-scale systems? 3) What is the time and token cost of running FM-Agent? 9
Table 1. The complexity of systems that FM-Agent successfully reasons about.
Table 2. The number of bugs newly discovered by FM-Agent for each system.
System
Type
LoC
#Functions
CCC VibeTensor VibeOS Bespoke OLAP
Compiler ML System Operating System Database
143k 108k 15k 11k
4,957 3,031 452 109
CCC VibeTensor VibeOS Bespoke OLAP
339 141 23 19
277k
8,549
Total
522
Total
8.1
System
#Bugs
Table 3. The bug discovery methods already used by developers of each system.
Experimental Setup
We run all experiments on a machine with 16 vCPUs and 32 GiB memory. It uses a third-generation Intel Xeon Scalable processor and runs Ubuntu 24.04 Server 64-bit. All three components of FM-Agent, including specification generator, code reasoner, and bug validator, use Claude Sonnet 4.6 [2]. The maximum number of attempts to generate test cases is set to 10. FM-Agent is evaluated on four large-scale systems shown in Table 1. We evaluate the scale of each system in terms of lines of code (LoC) and the number of functions. The number of LoC is measured by cloc [14], which counts the number of lines of code excluding blank lines and comments. We only count the LoC of source code files, excluding test files and documentation files. Specifically, the LoC of each system ranges from 11k to 143k. The number of functions in each system ranges from 109 to 4,910. Here is a brief introduction to each system.
System
Method
CCC VibeTensor
Integration tests and unit tests GoogleTest suites (208 cases), Pytest suites (203 cases), differential check against PyTorch, and multi-agent code review Bespoke OLAP Differential check against DuckDB
• CCC (Claude’s C Compiler) [3]. CCC is a C compiler that was autonomously developed by Anthropic using Claude Code. CCC supports various C standards and hardware architectures. It implements all compilation components from scratch, such as the preprocessor, optimizer, linker, and executable file generator. • VibeTensor [39, 54]. VibeTensor is a deep learning framework that was autonomously developed by NVIDIA using its coding agent. VibeTensor covers various components, such as Cuda runtime, core runtime, and GPU kernels. • VibeOS [22]. VibeOS is an operating system vibe-coded from scratch using Claude Code. It implements various OS components, such as process management, memory management, and file systems. It also contains GUI and some user space applications. Our evaluation focuses on the kernel part of VibeOS, whose LoC and number of functions are reported in Table 1. • Bespoke OLAP [52, 53]. Bespoke OLAP provides SQL query processing engines developed from scratch using GPT-5.2 Codex. It achieves an order-of-magnitude speedup over DuckDB. Bespoke OLAP also provides scripts to generate query engines. For fairness, we 10
do not re-generate the engine using these scripts, but directly reuse the artifact provided by the developers. These systems are selected for the following reasons. First, they are large enough and automatically developed by coding agents, which makes it harder to manually write specifications. Thus, they are suitable for evaluating the scalability and bug detection capability of FM-Agent. Second, they are developed by different coding agents in various programming languages, such as C++, Python, Cuda, and Rust. They also cover different domains, such as compilers, deep learning frameworks, operating systems, and databases. This allows us to evaluate the generality of FM-Agent. We do not compare FM-Agent with existing verification tools, such as symbolic execution engines [5, 36], Verus [25, 26], and Dafny [27]. This is because they usually require manually written accurate specifications, which is infeasible for large-scale systems in our evaluation. Specifications generated by FM-Agent cannot be used by these tools, as they target formal specifications rather than natural language specifications. Note that these systems have been tested by their developers using various methods, which will be introduced in Section 8.2. 8.2
Capability of Bug Discovery
To evaluate the bug discovery capability of FM-Agent, we download the latest version (at submission time) of each system from GitHub repositories and run FM-Agent on them. Note that 3 of 4 systems have already been well tested and fixed by their developers (Table 3). VibeOS has been partially tested, but its developers do not release the testing details. Table 2 shows that FM-Agent can still discover 522 new
Table 4. The concurrency space of specification generation for each system, including the number of phases and the maximum/median/minimum numbers of layers in each phase. More phases and fewer layers per phase indicate higher concurrency in specification generation.
bugs. The evaluation results demonstrate the effectiveness of FM-Agent in discovering previously undetected bugs. We further analyze the contribution of our techniques to bug discovery. For example, we implement and run an ablation version on the largest system CCC in our evaluation. The ablation version generates specifications only based on function implementations rather than using our top-down paradigm. Besides, it does not use our code reasoner to check the implementation against the specification. Instead, it directly asks LLMs to answer whether the implementation satisfies its specification without Hoare-style reasoning. Finally, it uses the same bug validator as FM-Agent to confirm potential bugs. As a result, it discovers only 57 bugs in CCC, which is much fewer than 339 bugs discovered by FM-Agent. We further analyze the bugs reported by FM-Agent to show that they can cause serious consequences. In CCC, FM-Agent discovers 339 bugs. Here are some of the main bug types. 111 bugs cause incorrect code generation at the IR level. 68 bugs involve incorrect runtime outputs. 39 bugs result in missing or incorrect diagnostic messages. 14 bugs result in compilation crash or hang. 9 bugs are about compilation optimization, such as failing to remove unnecessary instructions. In VibeOS, FM-Agent discovers 23 bugs. Specifically, 4 bugs cause memory corruption or stack overflow. 4 bugs result in incorrect return values of system calls. 2 bugs lead to infinite loops. 1 bug causes a failed process creation to still increment the PID counter. The remaining 12 bugs involve incorrect or missing logic in code. For example, net_ping always fails immediately if the timeout value is under 10ms, because integer division truncates the loop bound to zero. In Bespoke OLAP, FM-Agent discovers 19 bugs. Specifically, 7 bugs cause the query execution to return incorrect results. Bespoke OLAP synthesizes SQL query engines for specific SQL queries, such as the TPC-H benchmark. It generates C++ functions to execute the workflow of SQL queries, which brings significant performance improvement. However, some of these functions contain bugs and break the intended semantics. For example, one bug causes a number in the query result to be truncated rather than rounded. 3 bugs lead to process crashes. 9 bugs result in silent acceptance of invalid inputs. In VibeTensor, FM-Agent discovers 141 bugs. Here are some of the main bug types. Specifically, 50 bugs cause silently incorrect execution results, such as incorrect tensor values, shapes, or data types. 51 bugs result in missing or incorrect error handling. 19 bugs cause memory safety issues, such as memory leaks. 3 bugs lead to program crashes.
8.3
System
#Phases
CCC VibeTensor VibeOS Bespoke OLAP
13 12 14 6
#Layers per Phase Max
Median
Min
19 18 9 4
10 7 4 3
4 2 1 1
verification tool that can handle all these large-scale systems. Although FM-Agent cannot ensure soundness, it realizes much better scalability than existing verification tools. However, note that we do not claim FM-Agent can replace existing formal verification tools. FM-Agent realizes high scalability, while prior verification tools ensure soundness. They target different scenarios. The scalability of FM-Agent can be attributed to its topdown specification generation paradigm, which allows concurrency for the specification generator, code reasoner, and bug validator. This is critical for scaling to large systems, as LLM invocation is time-consuming. Regarding the specification generator, FM-Agent decomposes the system into self-contained phases and splits each phase into layers based on function call graphs. As shown in Table 4, the number of phases ranges from 6 to 14, and the number of layers per phase ranges from 1 to 19. The specification generation of different phases can be executed concurrently. Within each phase, the specification generation of functions in the same layer can also be executed concurrently. Although the layers in each system should be handled sequentially in topdown order, the maximum number of layers per phase is 19. This still provides concurrency space. For code reasoner and bug validator, FM-Agent can handle each function independently and concurrently, which can further improve the scalability of FM-Agent. This comes from the functionlevel specification, which enables compositional reasoning in FM-Agent.
9
Related Work
Formal verification. Recent work has made strong progress in formal verification for systems. Some works [6–11, 17, 23, 28, 29, 44, 48, 59, 60] use interactive theorem provers, such as Coq [49], to verify system correctness against formal specifications. They introduce new theories and verify critical properties. However, they require manual proofs. This creates a heavy human burden and does not scale well to large systems. For example, FSCQ [11], a sequential verified file system, takes several researchers about 1.5 years
Scalability of FM-Agent
Compositional reasoning of systems in Table 1 takes about 2 days and 3.4 billion tokens in total. There is no existing 11
to complete. Other works [13, 15, 18–20, 33, 47, 57, 58] use semi-automated verifiers to reduce manual proof effort. However, developers still need to provide formal specifications, loop invariants, and partial proofs. This also limits scalability. For example, implementing and verifying a cluster management controller with Anvil [47] takes around 2.5 person-months, with a proof-to-code ratio ranging from 4.5 to 7.4 across different controllers. Other works based on symbolic execution [5, 36–38, 45, 46, 56] achieve fully automated verification. However, they struggle with path explosion and cannot handle unbounded loops, which are common in system code. FM-Agent avoids manual effort and scales to large systems. Although it does not ensure soundness, our evaluation shows that it effectively finds many bugs in real-world systems. Therefore, FM-Agent offers a feasible direction for improving system reliability, especially in the era of LLMs. Note that FM-Agent does not aim to replace existing formal verifiers. Rather, it aims to complement existing works by providing a practical method to reason about large systems and find bugs. Integrating existing verification theories with FM-Agent is an interesting future direction that can further improve system reliability.
guide LLMs to automatically generate file systems. Unlike SysSpec, FM-Agent focuses on automatically generating specifications for existing systems, which helps reason about system correctness. SysSpec relies on standard test suites rather than reasoning to check correctness.
10
Discussion
FM-Agent vs. formal verifiers. There is no automated formal verifier that can scale to systems in our evaluation, but FM-Agent does not aim to replace them. FM-Agent and formal verifiers target different scenarios and have their own advantages. Formal verifiers ensure soundness, while FM-Agent targets scalable reasoning. How to combine FMAgent with formal verifiers to achieve better results is an interesting future research direction. Reasoning vs. testing. Both testing and reasoning are important for improving large-scale system reliability. Testing is lightweight and scales well, while reasoning analyzes code semantics to find bugs that testing may miss. The evaluation shows FM-Agent finds bugs that testing methods cannot detect. FM-Agent enables reasoning about largescale systems and can be combined with testing to improve reliability. Additionally, FM-Agent-generated specifications can guide testing. Testing requires a testing oracle to verify results, which is difficult to construct automatically. Using FM-Agent specifications to help build testing oracles is a promising research direction.
LLM-assisted formal verification. To reduce human proof effort, some works [12, 35, 42, 55] combine LLMs with traditional verification techniques. The key idea is to use LLMs to automatically generate proofs or annotations (e.g., loop invariants and assertions) for verification tools (e.g., Coq and Verus), enabling fully automated verification. Although these works reduce human proof effort, they focus on generating proofs rather than specifications. They still require pre-defined formal specifications, which is a major barrier to compositional reasoning for large systems. Moreover, LLM-generated code makes manually writing specifications harder, as developers lack a deep understanding of the code. In contrast, FM-Agent automatically generates specifications, enabling automated compositional reasoning.
Support for concurrency. Currently, FM-Agent focuses on reasoning about sequential programs. Since we have integrated Hoare logic inference rules into FM-Agent to reason about sequential programs, it may also be feasible to integrate more theories about concurrent programs, such as relyguarantee [30, 31] and concurrent separation logic [40, 43]. It is a possible future direction to extend FM-Agent to support reasoning about concurrent programs.
Generation of specifications. Prior works [12, 24] have explored automatically generating specifications for programs. For example, SAFE leverages LLMs to synthesize formal specifications for Rust programs. Its specification generation heavily relies on analyzing the program implementation and reflects implementation behavior. This is because SAFE generates specifications to synthesize training data, where each sample is a Rust program paired with a formal specification and proof. The training data are then used to enhance the capability of LLMs to generate formal proofs. As a result, SAFE and FM-Agent target different goals, and FM-Agent cannot reuse the method of SAFE. In FM-Agent, the generated specifications guide the reasoning process. They reflect the expected behavior of functions from the system’s perspective, regardless of implementation bugs. Some other works, such as SysSpec [32], propose a new paradigm for manually writing specifications that can
Reasoning about LLM-based applications. LLMs are increasingly integrated into various applications, creating new challenges for reasoning about their behavior. It is difficult to formally define what properties LLM outputs must satisfy. One possible way is to assume LLM outputs satisfy the requirements in prompts, usually expressed as natural language rather than formulas. This scenario requires reasoning about code against natural language specifications like FM-Agent. Extending FM-Agent to reason about LLMbased applications is a promising future research direction.
11
Conclusion
This paper presents the first framework that enables automated compositional reasoning for large-scale systems. The evaluation shows that FM-Agent can successfully find newly discovered bugs in systems with up to 143k LoC. 12
References
[17] Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, Savannah, GA, 653–669. https://www. usenix.org/conference/osdi16/technical-sessions/presentation/gu [18] Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. 2020. Storage Systems are Distributed Systems (So Verify Them That Way!). In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). [19] Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. 2023. Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). [20] Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. 2015. IronFleet: Proving Practical Distributed Systems Correct. In Proceedings of the 25th Symposium on Operating Systems Principles (Monterey, California). Association for Computing Machinery, New York, NY, USA, 1–17. doi:10.1145/2815400.2815428 [21] C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576–580. doi:10.1145/363235.363259 [22] Kaanse. 2026. VibeOS. https://github.com/kaansenol5/VibeOS/tree/ main,. [23] Gerwin Klein. 2009. Operating System Verification—An Overview. Sadhana 34 (Feb 2009), 27–69. doi:10.1007/s12046-009-0002-4 [24] Shuvendu K. Lahirie. 2024. Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages. In 2024 Formal Methods in Computer-Aided Design (FMCAD). 142–147. doi:10.34727/2024/isbn. 978-3-85448-065-5_19 [25] Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024. Verus: A Practical Foundation for Systems Verification. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles (Austin, TX, USA) (SOSP ’24). Association for Computing Machinery, New York, NY, USA, 438–454. doi:10.1145/3694715.3695952 [26] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. In Proceedings of the ACM on Programming Languages (OOPSLA). ACM. [27] K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Springer, 348–370. [28] Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. 2022. Design and Verification of the Arm Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, Carlsbad, CA, 465–484. https://www.usenix.org/conference/osdi22/ presentation/li [29] Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh. 2023. Spoq: Scaling Machine-Checkable Systems Verification in Coq. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23). USENIX Association, Boston, MA, 851–869. https://www. usenix.org/conference/osdi23/presentation/li-xupeng [30] Hongjin Liang and Xinyu Feng. 2013. Modular Verification of Linearizability with Non-Fixed Linearization Points. SIGPLAN Not. 48, 6 (jun 2013), 459–470. doi:10.1145/2499370.2462189 [31] Hongjin Liang, Xinyu Feng, and Ming Fu. 2012. A Rely-GuaranteeBased Simulation for Verifying Concurrent Program Transformations. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium
[1] Anthropic. 2026. Claude Code. https://claude.com/product/claudecode,. [2] Anthropic. 2026. Claude Sonnet 4.6. https://www.anthropic.com/ claude/sonnet,. [3] Anthropics. 2026. CCC — Claude’s C Compiler. https://github.com/ anthropics/claudes-c-compiler/,. [4] Anysphere. 2026. Cursor. https://cursor.com/,. [5] Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, 209–224. [6] Tej Chajed, Frans Kaashoek, Butler Lampson, and Nickolai Zeldovich. 2018. Verifying Concurrent Software Using Movers in CSPEC. In 13th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, Carlsbad, CA, 306–322. https://www.usenix.org/ conference/osdi18/presentation/chajed [7] Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2019. Verifying Concurrent, Crash-Safe Systems with Perennial. In Proceedings of the 27th ACM Symposium on Operating Systems Principles. Hunstville, ON, Canada. [8] Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich. 2021. GoJournal: A Verified, Concurrent, Crash-safe Journaling System. In 15th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, 423– 439. https://www.usenix.org/conference/osdi21/presentation/chajed [9] Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2023. Verifying vMVCC, a high-performance transaction library using multi-version concurrency control. In Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI ’23). [10] Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay undefinedleri, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2017. Verifying a High-Performance Crash-Safe File System Using a Tree Specification. In Proceedings of the 26th Symposium on Operating Systems Principles (Shanghai, China). Association for Computing Machinery, New York, NY, USA, 270–286. [11] Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash Hoare Logic for Certifying the FSCQ File System. In Proceedings of the 25th Symposium on Operating Systems Principles (Monterey, California). Association for Computing Machinery, New York, NY, USA, 18–37. [12] Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, Fan Yang, Shuvendu Lahiri, Tao Xie, and Lidong Zhou. 2024. Automated Proof Generation for Rust Code via Self-Evolution. In ICLR 2025. https://www.microsoft.com/en-us/research/publication/ automated-proof-generation-for-rust-code-via-self-evolution/ [13] Xiangdong Chen, Zhaofeng Li, Jerry Zhang, Vikram Narayanan, and Anton Burtsev. 2025. Atmosphere: Practical Verified Kernels with Rust and Verus. In Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles (Lotte Hotel World, Seoul, Republic of Korea) (SOSP ’25). Association for Computing Machinery, New York, NY, USA, 752–767. doi:10.1145/3731569.3764821 [14] cloc Development Team. 2026. cloc - Count Lines of Code. https: //github.com/aldanial/cloc,. [15] Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. 2017. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the ACM Symposium on Operating Systems Principles (SOSP). [16] GitHub. 2026. GitHub Copilot. https://github.com/features/copilot,.
13
on Principles of Programming Languages (Philadelphia, PA, USA). Association for Computing Machinery, New York, NY, USA, 455–468. [32] Qingyuan Liu, Mo Zou, Hengbin Zhang, Dong Du, Yubin Xia, and Haibo Chen. 2026. Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC. In 24th USENIX Conference on File and Storage Technologies (FAST 26). 291–311. [33] Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao. 2020. Armada: Low-Effort Verification of High-Performance Concurrent Programs. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (London, UK). Association for Computing Machinery, New York, NY, USA, 197–210. [34] Microsoft. 2026. VerusBench. https://github.com/microsoft/verusproof-synthesis/tree/main/benchmarks/VerusBench,. [35] Eric Mugnier, Emmanuel Anaya Gonzalez, Nadia Polikarpova, Ranjit Jhala, and Zhou Yuanyuan. 2025. Laurel: Unblocking Automated Verification with Large Language Models. Proc. ACM Program. Lang. 9, OOPSLA1, Article 134 (April 2025), 27 pages. doi:10.1145/3720499 [36] Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (Huntsville, Ontario, Canada). Association for Computing Machinery, New York, NY, USA, 225–242. [37] Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th Symposium on Operating Systems Principles (Shanghai, China). Association for Computing Machinery, New York, NY, USA, 252–269. doi:10.1145/3132747.3132748 [38] Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and Verification in the Field: Applying Formal Methods to BPF Just-in-Time Compilers in the Linux Kernel. USENIX Association, USA. [39] NVIDIA. 2026. VibeTensor. https://github.com/NVlabs/vibetensor,. [40] Peter W. OHearn. 2007. Resources, Concurrency, and Local Reasoning. Theor. Comput. Sci. 375, 1-3 (apr 2007), 271–307. doi:10.1016/j.tcs.2006 .12.035 [41] OpenAI. 2026. OpenAI Codex. https://openai.com/codex/,. [42] Jianxing Qin, Alexander Du, Danfeng Zhang, Matthew Lentz, and Danyang Zhuo. 2025. Can Large Language Models Verify System Software? A Case Study Using FSCQ as a Benchmark. In Proceedings of the 2025 Workshop on Hot Topics in Operating Systems (Banff, AB, Canada) (HotOS ’25). Association for Computing Machinery, New York, NY, USA, 34–41. doi:10.1145/3713082.3730382 [43] Jung Ralf, Swasey David, Sieczkowski Filip, Svendsen Kasper, Turon Aaron, Birkedal Lars, and Dreyer Derek. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai, India). Association for Computing Machinery, New York, NY, USA, 637–650. doi:10.1145/2676726.2676980 [44] Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, Frans Kaashoek, and Nickolai Zeldovich. 2023. Grove: a Separation-Logic Library for Verifying Distributed Systems. In Proceedings of the 29th ACM Symposium on Operating Systems Principles (SOSP 2023). Koblenz, Germany, 113–129. [45] Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In 12th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, Savannah, GA, 1– 16. https://www.usenix.org/conference/osdi16/technical-sessions/ presentation/sigurbjarnarson [46] Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018. Nickel: A Framework for Design and Verification of Information Flow Control Systems.
In 13th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association, Carlsbad, CA, 287–305. http: //www.usenix.org/conference/osdi18/presentation/sigurbjarnarson [47] Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. 2024. Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association, Santa Clara, CA, 649–666. https://www.usenix.org/conference/osdi2 4/presentation/sun-xudong [48] Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, and Ronghui Gu. 2021. Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles (Virtual Event, Germany). Association for Computing Machinery, New York, NY, USA, 866–881. doi:10.1145/3477132.3483560 [49] Coq Development Team. 2024. The Coq Proof Assistant. https://coq. inria.fr/,. [50] OpenCode Development Team. 2026. The open source AI coding agent. https://opencode.ai/,. [51] OpenRouter Development Team. 2026. OpenRouter. https://openrouter. ai/,. [52] Johannes Wehrstein, Timo Eckmann, Matthias Jasny, and Carsten Binnig. 2025. Bespoke OLAP: Synthesizing Workload-Specific OneSize-Fits-One Database Engines. arXiv preprint arXiv:2603.02001 (2025). https://arxiv.org/abs/2603.02001 [53] Johannes Wehrstein, Timo Eckmann, Matthias Jasny, and Carsten Binnig. 2026. Bespoke-OLAP. https://github.com/DataManagementLab/ BespokeOLAP,. [54] Bing Xu, Terry Chen, Fengzhe Zhou, Tianqi Chen, Yangqing Jia, Vinod Grover, Haicheng Wu, Wei Liu, Craig Wittenbrink, Wen mei Hwu, Roger Bringmann, Ming-Yu Liu, Luis Ceze, Michael Lightstone, and Humphrey Shi. 2026. VibeTensor: System Software for Deep Learning, Fully Generated by AI Agents. arXiv:arXiv:2601.16238 [55] Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu. 2025. AutoVerus: Automated Proof Generation for Rust Code. Proc. ACM Program. Lang. 9, OOPSLA2, Article 396 (Oct. 2025), 29 pages. doi:10.1145/3763174 [56] Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, and George Candea. 2019. Verifying software network functions with no verification expertise. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (Huntsville, Ontario, Canada) (SOSP ’19). Association for Computing Machinery, New York, NY, USA, 275–290. doi:10.1145/3341301.3359647 [57] Zihao Zhang, Ti Zhou, Christa Jenkins, Omar Chowdhury, and Shuai Mu. 2025. AutoMan: Facilitating Verified Distributed Systems Development Through Automatic Code Generation and Manual Optimizations. In Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles (Lotte Hotel World, Seoul, Republic of Korea) (SOSP ’25). Association for Computing Machinery, New York, NY, USA, 768–785. doi:10.1145/3731569.3764822 [58] Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, and Weidong Cui. 2024. VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association, Santa Clara, CA, 599–614. https://www.usenix.org/conference/osdi24/presentation/ zhou [59] Mo Zou, Haoran Ding, Dong Du, Ming Fu, Ronghui Gu, and Haibo Chen. 2019. Using Concurrent Relational Logic with Helpers for Verifying the AtomFS File System. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (Huntsville, Ontario, Canada). Association for Computing Machinery, New York, NY, USA, 259–274.
14
[60] Mo Zou, Dong Du, Mingkai Dong, and Haibo Chen. 2024. Using Dynamically Layered Definite Releases for Verifying the RefFS File System. In 18th USENIX Symposium on Operating Systems Design and
Implementation (OSDI 24). USENIX Association, Santa Clara, CA, 629– 648. https://www.usenix.org/conference/osdi24/presentation/zou
15