Coding agents can now generate system-level codebases with more than 100,000 lines of code, and even assemble complete compilers. The harder question is what happens next: how do we reason about whether that generated code is actually correct?
FM-Agent is a formal-methods agent designed for this problem. By combining formal verification ideas with LLMs, FM-Agent performs fully automated correctness reasoning for large software systems. Across more than 270K lines of heavily tested system code, it found 522 previously missed bugs.
The project is open source and also provides an online service:
Autonomously Understanding Design Intent
Traditional formal methods require experts to manually write mathematical specifications for each function. That workflow becomes impractical when AI systems can generate hundreds or thousands of functions at once.
FM-Agent addresses this by proposing a top-down specification generation paradigm. Starting from a natural-language description of the whole system, FM-Agent uses an LLM to infer the developer's design intent, generate a specification for the entry function, and then derive what each callee must guarantee to satisfy that higher-level specification.
This process continues layer by layer, assigning each function its expected responsibility without manual specification writing. When a function has multiple callers, FM-Agent merges the expectations from those callers into a specification that satisfies all relevant contexts.
Reasoning with Natural-Language Hoare Logic
Hoare logic is a classic theory for program verification. It uses inference rules to reason about the program state after each code block and then checks whether the final state satisfies the expected specification. The classical version, however, is designed for mathematical formulas, while real developer intent is often expressed in natural language.
FM-Agent generalizes Hoare-style reasoning to natural language. The key observation is that modern LLMs are highly effective at predicting the execution effects of small code fragments. FM-Agent guides the model to act as a reasoning engine: it infers the program state after each step in natural language, then checks whether the final state violates the intended specification.
When FM-Agent finds a violation, it can use the complete reasoning trace to diagnose the root cause and generate a test case that triggers the bug. This gives developers concrete evidence and useful context for debugging.
Finding Bugs Behind Existing Defenses
The evaluation used four large systems generated by leading coding agents such as Claude Opus and GPT Codex. The largest subject, Claude C Compiler, contains 143K lines of code. These systems had already gone through unit tests, integration tests, differential testing, and multi-agent cross review.
Even under these defenses, FM-Agent found 522 previously unknown bugs. Many were silent failures that are difficult to catch with ordinary testing, such as compilation pipelines that complete successfully while producing executables with incorrect behavior and no obvious crash or exception.
Getting Started
FM-Agent can be used through source code or directly through the online service. To start a run, users provide a code archive or GitHub repository URL, an API key, and the target model name.
During analysis, the service displays reasoning progress in real time. For functions with detected bugs, users can download Markdown reports that explain the likely cause.
Conclusion
Hoare logic was introduced by Turing Award winner Tony Hoare roughly sixty years ago, but the manual cost of formal methods has limited their adoption in large-scale software. FM-Agent does not aim to replicate traditional theorem proving with strict symbolic formulas. Instead, it uses the reasoning capability of large language models to make automated correctness reasoning practical for large system code.
In that sense, FM-Agent keeps the core idea of Hoare logic while making it usable in a modern AI programming workflow: generated code should not only compile and run, but also be reasoned about.