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

arXiv: https://arxiv.org/abs/2604.11556 · HTML: https://mlsanity.com/paper/2604.11556/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 8 of its 54 references that are in the map.
- First posted on arXiv 13 Apr 2026.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)
- LLM agents and tool use / [Software engineering coding agents](https://mlsanity.com/agents/software-engineering-coding-agents/)

## Builds on (most cited first, 8 of 8)

- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages](https://mlsanity.com/paper/2406.09757/) (2024)
- [Bespoke OLAP: Synthesizing Workload-Specific One-size-fits-one Database Engines](https://mlsanity.com/paper/2603.02001/) (2026)
- [VibeTensor: System Software for Deep Learning, Fully Generated by AI Agents](https://mlsanity.com/paper/2601.16238/) (2026)
- [Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version)](https://mlsanity.com/paper/2309.03046/) (2023)
- [Sharpen the Spec, Cut the Code: A Case for Generative File System with SYSSPEC](https://mlsanity.com/paper/2512.13047/) (2025)

## Built on by (most cited first, 6 of 6)

- [SMetric: Rethink LLM Scheduling for Serving Agents with Balanced Session-centric Scheduling](https://mlsanity.com/paper/2607.08565/) (2026)
- [Agentic Model Checking](https://mlsanity.com/paper/2605.21434/) (2026)
- [VeriGraph: Towards Verifiable Data-Analytic Agents](https://mlsanity.com/paper/2606.16603/) (2026)
- [Code-Augur: Agentic Vulnerability Detection via Specification Inference](https://mlsanity.com/paper/2606.18619/) (2026)
- [Specula: Scaling formal specifications for autonomous model checking of system code](https://mlsanity.com/paper/2607.25333/) (2026)
- [SkillSpec: Intent-Masked Specification Reasoning for Agent Skill Correctness](https://mlsanity.com/paper/2609.06052/) (2026)

## Abstract (arXiv)

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.