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

FM-Agent is a novel framework that leverages large language models to automate compositional reasoning for large-scale systems by generating function-level specifications from natural-language caller expectations, enabling the discovery of hundreds of critical bugs in complex codebases within days.

The Gist

Imagine you are the manager of a massive construction project. You've hired a team of incredibly fast, super-smart robots (LLMs) to build a skyscraper. These robots can draft blueprints and lay bricks faster than any human team ever could. But there's a catch: these robots sometimes get distracted, hallucinate, or make tiny mistakes that could cause the whole building to collapse later.

The problem is that the building is so huge (over 100,000 lines of code, or "bricks") that no human can read every single blueprint to check for errors. Traditional safety inspectors (old verification tools) are great, but they require a human to write a perfect, mathematical rulebook for every single room before they can start checking. Since the robots are building the rooms as they go, and humans don't fully understand the robots' weird logic, writing that rulebook is impossible.

Enter FM-Agent. Think of it as a new kind of "AI Safety Inspector" that doesn't need a human to write the rulebook first. Instead, it figures out what the building should look like by watching how the rooms connect to each other.

Here is how FM-Agent works, broken down into three simple steps using our construction analogy:

1. The "Top-Down" Detective (Specification Generation)

The Old Way: Usually, to check a room, you'd look at the bricks inside it and try to guess what the room was supposed to do. But if the robot made a mistake while laying the bricks, your guess would be wrong.
The FM-Agent Way: FM-Agent looks at the hallway (the caller) leading into the room. It asks, "What does the hallway expect this room to do?"

• If the hallway sends a package labeled "Heavy," the room must be strong enough to hold it.
• If the hallway expects a "Light" package back, the room must return something light.

By looking at the expectations of the people entering the room (the callers) rather than just the messy bricks inside, FM-Agent can write a "User Manual" (specification) for every room, even if the room itself is built poorly. It builds these manuals from the top of the building down to the basement, ensuring every room knows its job.

2. The "Natural Language" Inspector (Code Reasoning)

The Old Way: Traditional inspectors only speak "Math." If you can't translate the robot's messy work into perfect math formulas, they can't check it.
The FM-Agent Way: FM-Agent speaks "Human." It takes the "User Manual" (written in plain English) and compares it to the actual room.

• It walks through the room step-by-step.
• It asks the AI: "If I start with a heavy package, and I do this step, then that step, will I still have a heavy package at the end?"
• If the math doesn't add up, or if the final result doesn't match the User Manual, FM-Agent flags it as a potential disaster.

It's like a translator who can read the robot's messy notes and say, "Hey, you said you'd return a light package, but you actually returned a boulder. That's a bug!"

3. The "Crash Test" Driver (Bug Validator)

The Old Way: Sometimes, the inspector says, "This looks wrong," but they can't prove it. They just guess.
The FM-Agent Way: FM-Agent doesn't just guess; it tests. When it finds a suspicious room, it acts like a stunt driver.

• It builds a specific scenario (a test case) designed to trigger that specific mistake.
• It runs the building simulation.
• If the building actually shakes or the room collapses during the test, FM-Agent says, "Aha! I found a real bug!" and shows the developers exactly how to fix it.

Why is this a big deal?

The researchers tested FM-Agent on four massive systems (a compiler, an operating system, a database, and an AI framework) that were built entirely by AI robots. These systems were already tested by humans using standard methods, yet FM-Agent found 522 new, serious bugs that everyone else missed.

• The Scale: It handled systems as big as 143,000 lines of code in just two days.
• The Impact: It found bugs that could cause crashes, data loss, or security holes.

The Bottom Line

FM-Agent is like a super-intelligent quality control system that understands that what a function is supposed to do (its intent) is more important than how it was actually built (its implementation). By using AI to read the "intent" from the top down and then testing the results, it can keep our massive, AI-built software systems safe, even when the AI builders make mistakes.

It doesn't replace the need for human engineers, but it gives them a powerful new tool to catch the invisible cracks in the foundation before the building falls down.

Technical Summary

Technical Summary: FM-Agent

1. Problem Statement

The rise of Large Language Model (LLM)-assisted software development has enabled the generation of large-scale systems (e.g., compilers, operating systems) with hundreds of thousands of lines of code (LoC). However, these generated systems often contain subtle bugs due to LLM hallucinations. Verifying the correctness of such systems is critical but faces three major challenges:

1. Scalability: Traditional automated reasoning techniques (e.g., symbolic execution) struggle with path explosion and complex inter-procedural dependencies in large codebases.
2. Specification Burden: Compositional reasoning (e.g., Hoare logic) requires formal specifications for every function. Writing these manually is labor-intensive and requires deep domain expertise.
3. The "Implementation vs. Intent" Gap: In the era of LLM coding agents, developers often lack a deep understanding of the generated code. Existing methods that generate specifications by analyzing the implementation are flawed because the implementation itself may be buggy, leading to specifications that reflect the bug rather than the developer's intent. Furthermore, developers express intent in natural language, while traditional verifiers require formal formulas.

2. Methodology: FM-Agent Framework

FM-Agent is the first framework to realize automated compositional reasoning for large-scale systems by leveraging LLMs. It addresses the challenges through three core components and a novel top-down paradigm.

A. Core Insights

1. Caller-Driven Intent: LLMs can better infer a function's expected behavior by analyzing how its callers use it, rather than analyzing the buggy implementation itself.
2. Natural Language Reasoning: LLMs can accurately predict the execution results of small code blocks and understand both code semantics and natural language. This allows Hoare-style reasoning to be performed directly against natural language specifications rather than formal formulas.
3. System-Level Correlation: LLMs can correlate system-entry inputs with internal function behaviors, enabling the generation of high-level test cases that trigger specific internal bugs.

B. Workflow Components

1. Specification Generator (Top-Down Paradigm)

Instead of the traditional bottom-up approach (analyzing implementation first), FM-Agent uses a top-down approach:

• Process: It starts with entry functions and analyzes the caller's implementation to derive the Expected Specification (pre-conditions and post-conditions) for the callee.
• Logic: If a function $F$ is called by multiple callers, FM-Agent merges their expected behaviors (disjunction of pre-conditions, conjunction of post-conditions) to create a comprehensive specification.
• Concurrency: It constructs a call graph, identifies Strongly Connected Components (SCCs), and condenses the graph into a Directed Acyclic Graph (DAG). It then generates specifications in layers, allowing functions in the same layer (independent of each other) to be processed concurrently.
• Sources: For entry functions, it uses domain knowledge and implementation. For internal functions, it prioritizes caller expectations to avoid being misled by buggy implementations.

2. Code Reasoner (Hoare-Style Inference)

• Mechanism: It generalizes Hoare logic inference rules to operate on natural language.
• Process: Starting from the pre-condition, the LLM iteratively infers the post-condition of each statement (or code block).
• Verification: It checks if the inferred post-condition of the final statement in an execution path implies the function's specification post-condition. If the implication fails, a potential bug is flagged.
• Optimization: To reduce LLM costs, it groups statements into blocks and reasons about them collectively. It can also translate precise natural language conditions into formal formulas for SMT solvers when necessary.

3. Bug Validator

• Function: To confirm potential bugs and reduce false positives caused by LLM hallucinations.
• Process: Upon detecting a potential bug, the validator uses an LLM to generate a system-entry test case (not just a unit test) that triggers the specific internal failure.
• Execution: It runs the test case against the system. If the bug is reproduced within a set number of attempts (e.g., 10), it is reported as a genuine bug. It compares results against reference implementations (e.g., GCC, DuckDB) or expected outcomes.

3. Key Contributions

1. First Automated Compositional Reasoning Framework: FM-Agent is the first system to automate the generation of function-level specifications and perform compositional reasoning for large-scale systems without human-written formal specs.
2. Top-Down Specification Generation: It introduces a paradigm where specifications are derived from caller expectations, effectively decoupling the "intent" from potentially buggy "implementations."
3. Natural Language Hoare Logic: It extends Hoare logic to support natural language pre/post-conditions, leveraging LLMs to bridge the gap between developer intent (natural language) and formal verification.
4. System-Level Bug Triggering: It generates system-entry test cases that correlate external inputs with internal failures, providing actionable bug reports for developers.

4. Evaluation Results

The framework was evaluated on four large-scale systems (ranging from 11k to 143k LoC) automatically developed by various coding agents (Anthropic, NVIDIA, etc.) in languages including C, Rust, and Python.

• Scale: FM-Agent successfully reasoned about systems up to 143k LoC (CCC compiler) within 2 days.
• Bug Discovery: Despite these systems having undergone extensive testing (unit tests, integration tests, differential checks, multi-agent reviews), FM-Agent discovered 522 newly found bugs.
  • CCC (Compiler): 339 bugs (including incorrect IR generation, runtime output errors, and compilation crashes).
  • VibeTensor (ML Framework): 141 bugs (including silent incorrect tensor values and memory leaks).
  • VibeOS (OS): 23 bugs (including memory corruption and infinite loops).
  • Bespoke OLAP (Database): 19 bugs (including incorrect query results).
• Ablation Study: An ablation version using a bottom-up approach (implementation-based specs) and direct LLM checking (without Hoare reasoning) found only 57 bugs in the CCC system, demonstrating the superiority of FM-Agent's top-down, compositional approach.
• Cost: The evaluation consumed approximately 3.4 billion tokens total, highlighting the feasibility of scaling LLM-based reasoning with proper concurrency management.

5. Significance

• Scalability: FM-Agent demonstrates that compositional reasoning can be scaled to industrial-sized systems, a task previously impossible for fully automated tools due to the specification bottleneck.
• LLM Era Relevance: It specifically addresses the unique challenges of verifying LLM-generated code, where human understanding of the code is limited, and traditional manual specification is infeasible.
• Complement to Formal Methods: While it does not guarantee soundness (like traditional theorem provers), it offers a practical, high-throughput method to find critical bugs in systems where formal verification is currently too expensive or impossible.
• Future Direction: It opens a new research path for combining natural language reasoning with formal verification theories, potentially leading to hybrid systems that offer both scalability and soundness.