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

Haoran Ding; Zhaoguo Wang; Haibo Chen

cs.SEApr 13, 2026

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

Authors: Haoran Ding, Zhaoguo Wang, Haibo Chen

Organizations: Institute of Parallel and Distributed Systems, Shanghai Jiao Tong University

Abstract

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 large-scale 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. This paper presents FM-Agent, the first framework that realizes automated compositional reasoning for large-scale systems. Leveraging LLMs, FM-Agent introduces a top-down 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.

Figures & tables

Panel of Figure 2 — Figure 2. Specifications generated for the from_keyword function in Figure 1 using two methods.

Figure 5. An example of the top-down paradigm for specification generation. Each directed edge from function

F_{i}

to function

F_{j}

indicates that

F_{i}

invokes

F_{j}

. The specification of

F_{j}

is generated based on the expected specification from all its callers

F_{i}

, which is denoted as

F_{i}\vdash\{P\}F_{j}\{Q\}

on the edge.

System	Type	LoC	#Functions
CCC	Compiler	143k	4,957
VibeTensor	ML System	108k	3,031
VibeOS	Operating System	15k	452
Bespoke OLAP	Database	11k	109
Total		277k	8,549

Table 1. The complexity of systems that FM-Agent successfully reasons about.

System	#Bugs
CCC	339
VibeTensor	141
VibeOS	23
Bespoke OLAP	19
Total	522

Table 2. The number of bugs newly discovered by FM-Agent for each system.

System	Method
CCC	Integration tests and unit tests
VibeTensor	GoogleTest suites (208 cases), Pytest suites (203 cases), differential check against PyTorch, and multi-agent code review
Bespoke OLAP	Differential check against DuckDB

Table 3. The bug discovery methods already used by developers of each system.

System	#Phases	#Layers per Phase
System	#Phases	Max	Median	Min
CCC	13	19	10	4
VibeTensor	12	18	7	2
VibeOS	14	9	4	1
Bespoke OLAP	6	4	3	1

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.

Explore similar work

Jul 7, 2026

Harnessing Code Agents for Automatic Software Verification

Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it (retrieving premises and predicting tactics one step at a time, or splitting goals by divide-and-conquer), and still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary and limiting. Handing the whole lemma to a general LLM code agent (for example, Claude Code), free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving full coverage: every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs under feedback and hard constraints from the harness that keep each one sound (accepted only when the prover's kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent tactics). We evaluate this harness plus code agent along three dimensions. (1) Core logic: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior provers manage barely one in eight, Aria proves all 318. (3) Generality: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. A state-of-the-art model (Claude Opus 4.7) can write proofs for verified software development fully and automatically.

Shuangxiang Kan, Shuanglong Kan, Sebastian Ertel

Singapore Management University · Singapore · Barkhausen Institut +1

Software Engineering Agents Automated Theorem Proving Formal Verification LLM Agent Harnesses

Ask PDF

May 28, 2026

Inferring Code Correctness from Specification

Large language models (LLMs) have become integral to modern software development, enabling automated code generation at scale. However, validating the correctness of LLM-generated code remains a critical and largely unsolved challenge. Existing approaches either rely on dynamic consensus across multiple code candidates - making them costly and difficult to scale - or on static reasoning that is susceptible to dynamic bugs and order bias. In this paper, we propose TRAILS~ (Targeted Reasoning Agreement via Inputs and Specifications), an approach that grounds LLM reasoning with concrete (input, output) pairs. TRAILS~ first generates diverse test inputs via category partitioning based on the specification, then executes them against the candidate code and prompts LLMs to assess whether the resulting input-output pairs conform to the specification - without ever reasoning over the code itself. Scores are aggregated across inputs, to determines whether the program is likely correct. We evaluate TRAILS~ on two datasets, LiveCodeBench and CoCoClaNeL, across three LLMs (Qwen3Coder-30B, Devstral-Small-24B, and Olmo3.1-Instruct), comparing against HoarePrompt and a Zero-Shot Chain-of-Thought baseline. TRAILS~ improves Matthew Correlation Coefficient by up to 39% relative to Zero-Shot COT and consistently outperforms HoarePrompt. Beyond accuracy, TRAILS~ demonstrates greater stability across seeded runs, reducing sensitivity to LLM non-determinism, and assigns correct labels to a larger set of unique code samples than competing approaches.

Tambon Florian, Papadakis Mike

University of Luxembourg Luxembourg, Luxembourg

Automated Software Testing Code Generation Evaluation LLM Code Generation

Ask PDF

Jul 28, 2026

Specula: Scaling formal specifications for autonomous model checking of system code

Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code and uses the specifications for highly effective model checking and bug finding. Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications, including invariants that describe correctness properties of the target system and formal models that describe the system implementation with the right level of abstractions. Specula is fully autonomous and thus eliminates the barrier of applying formal methods to real-world system code (as in traditional human-centric approaches). Meanwhile, Specula addresses limitations of LLM-driven techniques like reward hacking and hallucinations through self-evolving loops that iteratively improve specification quality by enabling the agents to deepen their understanding of system code and its behaviors. We have used Specula to check 48 open-source system projects; Specula found 249 bugs including many deep bugs that are hard to find by existing approaches. Specula has been used by several companies and is maintained at https://github.com/specula-org/Specula.

Qian Cheng, Saad Mohammad Rafid Pial, Ruize Tang +6

Nanjing University Nanjing, China · University of Illinois Urbana-Champaign, IL, USA · Microsoft Research Asia Beijing, China +1

Software Engineering Agents Formal Verification Autoformalization

Ask PDF