FM-Agent deeply integrates formal methods with large language models to enable push-button correctness reasoning for large software systems. Today, we introduce Incremental Reasoning, a new capability that automatically identifies and reasons about the correctness of code affected by newly added features or new developer intent.
Instead of re-analyzing the entire system after every change, FM-Agent focuses only on the parts relevant to the current development intent. This significantly reduces reasoning costs during software evolution while preserving the ability to catch correctness defects caused by intent changes.
FM-Agent combines Hoare-style reasoning with large language models to automatically generate correctness specifications for software systems and reason about code against those specifications. This lets FM-Agent detect potential correctness defects without manual intervention or formal-methods expertise.
Previous versions of FM-Agent had a practical limitation: during software evolution, even when only a small portion of a codebase changed, FM-Agent still needed to perform full-system correctness reasoning. Incremental Reasoning addresses common development scenarios such as feature additions, developer-intent changes, and localized code modifications.
In real software evolution, new developer intent often affects multiple modules. Some code is modified and must be checked. Some code remains unchanged but should have been updated, creating missed-modification defects. Some changes may also go beyond the stated intent and introduce unnecessary or incorrect behavior.
FM-Agent analyzes these relationships and can detect issues such as:
- Missing code modifications
- Incomplete implementations
- Incorrect modifications
- Unnecessary changes
- Correctness defects introduced by newly added functionality
Incremental Reasoning is now integrated into both the Claude Code and Codex plugins, allowing users to invoke FM-Agent directly from familiar AI-assisted programming environments.
Usage
Both the Claude Code and Codex plugins support Incremental Reasoning. The following example demonstrates the workflow using the Claude Code plugin.
Step 1: Run the auto-fix Command in Claude Code
Enter the FM-Agent plugin command:
/fm-agent:auto-fixFM-Agent automatically loads previous execution results and enters Incremental Reasoning mode. The plugin combines information from the Vibe Coding Prompt and Git logs to infer the purpose of the current modification.
The plugin also allows users to manually specify the development intent. In the example below, the goal is to adjust the structure of a B+ Tree.
Step 2: Configure the Maximum Repair Iterations
The plugin prompts the user to specify the maximum number of repair iterations. This parameter controls how many rounds of automated repair FM-Agent may attempt. If issues remain after one repair round, FM-Agent continues until the issues are resolved or the maximum number of iterations is reached.
Step 3: Generate Incremental Reasoning Results
After the reasoning process completes, FM-Agent outputs a summary report. In this example, one bug was detected and fixed, the reasoning mode is incremental, and the repair iteration count is 1.
Technical Details
Incremental Reasoning is not merely a targeted re-check of modified code. Instead, FM-Agent actively identifies functions affected by new developer intent, enabling it to detect missed updates, unnecessary modifications, specification inconsistencies, and other evolution-related issues.
The perspective shifts from "Which code has changed?" to "What intent is this development effort trying to achieve?"
Rather than relying solely on modified files, FM-Agent identifies functions relevant to the development intent and determines whether their specifications should be updated.
A function is included in the re-reasoning scope if any of the following conditions hold:
- The function implementation has changed.
- The function specification has changed.
- The specifications of functions it depends on have changed.
This has two advantages. First, even if developers forget to update a function that should have changed, FM-Agent can still bring that function into the reasoning process when it is relevant to the current intent. Second, if a modification is unrelated to the stated intent, FM-Agent can identify it as an unnecessary change.
Three-Stage Function Discovery Strategy
FM-Agent uses a progressive filtering strategy to narrow the search space from the entire repository to a small set of critical functions.
1. Module-Level Filtering
FM-Agent first uses an LLM to partition the codebase into functional modules and generate concise descriptions for each module. By comparing these descriptions with the development intent, unrelated modules are eliminated quickly.
2. File-Level Filtering
Within the candidate modules, FM-Agent uses an LLM to determine whether each source file is relevant to the development intent, further narrowing the scope.
3. Function-Level Filtering
Within selected files, FM-Agent computes a relevance score for each function using multiple signals:
- Textual similarity between function code and the development intent
- Relevance propagated through caller-callee relationships in the call graph
- Relevance of the enclosing class
The top-N highest-scoring functions are selected as relevant functions, where N is configurable. If the score distribution is ambiguous, FM-Agent invokes an LLM for second-stage ranking.
Specification Updates
Once relevant functions are identified, FM-Agent regenerates or updates specifications for newly added or modified functions, as well as relevant functions discovered through filtering.
For newly added functions, FM-Agent generates new specifications. For existing functions, FM-Agent provides the current specification, latest implementation, and development intent to the LLM, which determines whether the specification should be updated and how.
Through this mechanism, FM-Agent avoids the high cost of full-system re-reasoning while proactively detecting complex software-evolution issues.
Conclusion
Incremental Reasoning enables FM-Agent to fit more naturally into modern iterative software development workflows.