Skip to content

README.md

Latest commit

 

History

History
399 lines (300 loc) · 21.3 KB

README.md

File metadata and controls

399 lines (300 loc) · 21.3 KB
Raw

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

English | 中文

Website · Paper

FM-Agent is the first framework that realizes fully automated reasoning for large-scale systems (e.g., Claude's C Compiler with 143K LoC). It contains three steps:

  • Specification generation: Autonomously understand developers' intent of system design. Generate correctness specification for each function.
  • Code reasoning: Reason about the code against the specification without any human effort.
  • Bug diagnosis: Analyze the root cause and location of bugs based on the reasoning process.

The website of FM-Agent provides an online service for reasoning about codebases. You can try it easily!

⚠️ Warning: The effectiveness of this framework is heavily influenced by the capability of the underlying model. Weaker models may produce hallucinations, leading to incorrect reasoning conclusions. We recommend using models with strong reasoning abilities (Claude Opus 4.6/4.7, Claude Sonnet 4.6) for more reliable results.

Table of Contents

File Structure

|-- main.py                       # Entry point — orchestrates the full pipeline
|-- dashboard.py                  # Standalone real-time TUI dashboard for a run
|-- config.py                     # Configuration (models, granularity, concurrency, timeouts)
|-- install.sh                    # Dependency installation script
|-- pyproject.toml / uv.lock      # Python project metadata and pinned dependencies (uv)
|-- .env.example                  # Template for the .env runtime config
|-- src/                          # Core source modules (extraction, reasoning, LLM interaction, etc.)
|-- md/                           # Workflow instructions that guide the agent
|-- docs/                         # Additional documentation (e.g. OpenCode/LLM provider setup)

Environment Setup

Requirements

  • Ubuntu (22.04 LTS, 24.04 LTS is tested)
  • Python 3.12
  • pip >= 23
  • openai 2.15.0
  • OpenCode 1.4.6
  • Bun
  • oh-my-openagent plugin (installed via bunx)
  • @lucentia/opencode-trace plugin — captures raw OpenCode LLM request/response traces (see Structured Trace)
  • An LLM API key for your provider (the examples use OpenRouter)
  • Erlang Language Platform (ELP) — optional; required only when analyzing Erlang projects
    • The Erlang integration has been tested on Ubuntu with Erlang/OTP 26 or newer; select an ELP release binary built for a compatible OTP version.
    • rebar3 3.24.0 or newer is required for ELP to auto-discover projects containing rebar.config.
    • The macOS Erlang toolchain has not been tested as part of this integration; ./install.sh --with-erlang installs the current Homebrew formula versions.

Tested macOS Environment

The following macOS environment has been tested with the install script:

  • macOS 14.5 (Build 23F79), arm64
  • Darwin 23.5.0
  • Python 3.11.7
  • pip 23.3.1
  • uv 0.7.9
  • OpenCode 1.17.9
  • Bun/bunx 1.3.14
  • Homebrew 6.0.3
  • UnZip 6.00

Install Dependencies

Set the LLM API key used by both FM-Agent and OpenCode. We recommend OpenRouter: FM-Agent invokes LLMs concurrently, and OpenRouter is generous on RPM (requests per minute) and TPM (tokens per minute) — but any compatible provider works.

The easiest setup path is the interactive wizard:

uv run python src/configure_llm.py

It previews the changes, backs up existing files, updates the active FM-Agent TOML file, stores the API key in .env plus a private local key file for standalone OpenCode, and syncs the matching OpenCode provider entry in ~/.config/opencode/opencode.json (or the platform-equivalent config path) without requiring you to hand-edit JSON. If you choose auto, codex-cli, or claude-cli in the wizard, it updates the backend in the active FM-Agent TOML file and clears stale non-secret LLM overrides from the project .env. Any model and effort values found there are first retained in the TOML; no API key or OpenCode provider setup is needed.

If you prefer to edit files manually, put your API key in .env (gitignored, loaded automatically via python-dotenv); every other setting has a committed default in fm-agent.toml. Copy the template:

cp .env.example .env
# then edit .env and set LLM_API_KEY
# .env  (secret only)
LLM_API_KEY=your-api-key-here

Non-secret settings — model, endpoint, backend, provider, etc. — live in fm-agent.toml under [llm]. Edit them there for a permanent change. To override without touching the committed file — e.g. on a git clone you update with git pull — set the matching environment variable in .env or your shell. Precedence is env > .env > fm-agent.toml; because .env wins over the toml, a stale value there overrides a later toml edit, so check .env first if a change isn't taking effect. The wizard removes the common legacy LLM override keys from .env for you. See docs/config_llm.md for details and OpenCode provider setup. The wizard also warns about LLM variables already exported by the launching shell; use its displayed unset command before starting FM-Agent if the saved configuration should take effect.

To change just one non-secret LLM setting without manually editing the file, use the configuration command. For example, select the local Codex CLI backend:

uv run python src/configure_llm.py set --backend codex-cli

It previews and backs up fm-agent.toml, then changes only the setting(s) you pass. The command also supports --name, --provider, --base-url, --effort, and --api-style; see docs/config_llm.md for the complete syntax. It warns when a legacy .env value would still override a requested TOML setting.

Then, all of the above dependencies (except Ubuntu and Python) can be installed via the provided script:

./install.sh

Erlang support is optional because its toolchain is not needed for other languages. To install or verify Erlang/OTP 26+, rebar3 3.24.0+, and a compatible ELP release automatically, run:

./install.sh --with-erlang

The Erlang option uses Homebrew on macOS and the RabbitMQ Team Erlang PPA on Ubuntu when the system OTP is missing or too old. The Ubuntu configuration has been tested with Erlang/OTP 26+; the macOS Erlang configuration has not been tested and uses the current formula versions selected by Homebrew. On Linux, rebar3 and ELP are installed into ~/.local/bin; ensure this directory is on PATH in new shells. You can still install these tools manually, verify rebar3 version and elp version, and set ELP_COMMAND to an absolute ELP path if needed.

FM-Agent configures OpenCode's provider automatically from fm-agent.toml, so you do not need to hand-edit ~/.config/opencode/opencode.json for the model or key. The configuration wizard above can still keep that file synchronized for standalone OpenCode usage by writing the API key to a private provider-specific key file under your user state/config directory (see docs/config_llm.md). If you already use OPENCODE_CONFIG, the wizard updates that file instead of the default global path. It also honors OPENCODE_CONFIG_DIR, using that directory's opencode.jsonc when present or its opencode.json otherwise.

Important: FM-Agent automatically derives test cases based on the reasoning process to trigger potential bugs, which help developers locate and fix them. Before running FM-Agent, please ensure the execution environment for test cases is ready. If project-specific validation instructions are needed, provide them with --bug-validator; otherwise, the agent will decide how to execute the tests.

Configuration

Settings live in fm-agent.toml (with inline comments); each can also be overridden by its environment variable. See docs/configuration.md for the full reference of every parameter, default, and description.

(Optional) FM-Agent uses oh-my-openagent plugin to enhance OpenCode. The comment-checker hook built into this plugin should be disabled, otherwise it may intercept every comment block that FM-Agent writes, which are specifications of functions. It may force the agent to waste tokens justifying or removing them. You can open your oh-my-openagent config file (typically ~/.config/opencode/oh-my-openagent.json) and add disabled_hooks:

{
  "disabled_hooks": ["comment-checker"],
}

Structured Trace

FM-Agent always writes structured execution traces under fm_agent/trace/:

Path Content
fm_agent/trace/events.jsonl Structured events for OpenCode calls and verification LLM calls
fm_agent/trace/payloads/ Event payloads such as OpenCode stdout and selected LLM messages
fm_agent/trace/opencode/ Optional raw OpenCode LLM request/response JSONL files

To capture raw OpenCode LLM traffic, install the OpenCode trace plugin manually by adding it to ~/.config/opencode/opencode.json:

{
  "$schema": "https://opencode.ai/config.json",
  "plugin": ["@lucentia/opencode-trace"]
}

FM-Agent automatically passes TRACE_DIR and TRACE_FILENAME to each OpenCode process. The plugin writes fm_agent/trace/opencode/<event_id>.jsonl, where <event_id> matches the corresponding opencode_call event in events.jsonl. OpenCode may cache the @latest package; to force a refresh, remove ~/.cache/opencode/packages/@lucentia/opencode-trace@latest.

Quick Start

uv run python main.py <proj_dir> [--resume] [--all-bugs] [--domain-knowledge FILE ...] [--bug-validator FILE] [--submodule PATH [PATH ...]]
Argument Description
proj_dir Directory of codebase that you want to check correctness
--resume Continue a previous, interrupted run instead of starting over
--incremental INTENT_FILE Run in incremental mode. The value is the path to an intent file describing the goal of the modification.
--all-bugs Continue reasoning after a mismatch and report every candidate. Full and incremental modes validate each candidate; entry mode does not run bug validation.
--domain-knowledge FILE [FILE ...] Copy extra Markdown domain-knowledge files into the run and provide them to setup, spec generation, and bug validation agents. Alias: --knowledge; may be repeated.
--bug-validator FILE Use a custom Markdown prompt for bug validation instead of the built-in md/bug_validator.md.
--isolate Run against an isolated git worktree snapshot of the project instead of the project directory itself.
--submodule PATH [PATH ...] Only process source code under one or more subdirectories of proj_dir.
--extra-edge FILE Add supplemental caller-to-callee edges to the static call graph from a JSON file or directory.
--only-spec Only generate behavioral specs; skip the reasoning and bug validation stages. Cannot be combined with --incremental.
--plugin NAME Load a pipeline plugin from plugins/NAME/.
--list-plugin List valid pipeline plugins and exit.

Pipeline plugins

FM-Agent plugins can pass, replace, or modify each of the six pipeline stages through trusted Python hooks. Every hook uses the same signature:

def hook(proj_dir: str) -> None:
    ...

See Pipeline Plugins for the plugin layout, JSON configuration, execution modes, lifecycle, and trust boundary.

proj_dir must be a git repository.

To provide project-specific domain knowledge without editing FM-Agent's built-in prompts, pass one or more Markdown files:

uv run python main.py <proj_dir> --domain-knowledge docs/invariants.md docs/protocol.md

FM-Agent stages these files under fm_agent/spec_prompts/domain_context/user_knowledge/ for the current run. You can also set FM_AGENT_DOMAIN_KNOWLEDGE to an os.pathsep-separated list of Markdown files.

To customize how candidate bugs are tested, pass a Markdown file with --bug-validator:

uv run python main.py <proj_dir> --bug-validator prompts/compiler_bug_validator.md

The selected file replaces the built-in md/bug_validator.md instructions. When a custom --bug-validator is used for --all-bugs candidate validation, FM-Agent specifies the output path, required fields, and allowed values for the final result JSON so it can reliably read and validate the result and safely reuse it during --resume. Relative --bug-validator paths are resolved from the directory where FM-Agent is launched, not from proj_dir. FM-Agent still adds the current bug ID, target verification result, and any --domain-knowledge files to each generated bug-validation prompt.

Use --submodule to limit a full or incremental run to selected project subdirectories:

uv run python main.py <proj_dir> --submodule src/core src/runtime
uv run python main.py <proj_dir> --incremental intent.md --submodule src/core src/runtime

--submodule paths must point to directories inside proj_dir. The option can be combined with --resume, --isolate, and --incremental, but not with --entry-func.

Use --all-bugs with full, incremental, or entry-point analysis:

uv run python main.py <proj_dir> --all-bugs
uv run python main.py <proj_dir> --incremental intent.md --all-bugs
uv run python main.py <proj_dir> --entry-func src::main --all-bugs

The option is off by default. When enabled, FM-Agent continues through later reasoning checkpoints and writes one standard mismatch result per candidate. Full and incremental modes validate each candidate independently. Entry-point reasoning reports the candidates and their count but intentionally does not run bug validation.

For a result such as path/to/function.json, all-bugs candidates are written beside it as path/to/function.bug-001.json, bug-002.json, and so on. The primary result records bug_count and reasoning_complete. Resume treats a complete primary result as the reasoning checkpoint and only reruns candidate validations that do not yet have a terminal result. If reasoning stopped partway through, FM-Agent clears that function's intermediate candidates and validations and reruns the function without disturbing completed functions.

By default, every invocation wipes the existing fm_agent/ directory and restarts from scratch, so an interrupted run loses all prior progress. Pass --resume (or set the environment variable FM_AGENT_RESUME=1) to continue where the previous run left off. In resume mode FM-Agent keeps the existing fm_agent/ directory and only does the remaining work. Resume with the same reasoning mode: an all-bugs workspace requires --resume --all-bugs; default-mode resume rejects it so existing candidates and validation records are not mixed with legacy output.

Use --only-spec to stop after generating behavioral specs, skipping the reasoning and bug validation stages. This produces adjacent .spec.json and .info.json metadata files for each function without spending time on verification, which is useful when you only want the specs or want to review them before running the full analysis. It cannot be combined with --incremental, which is inherently a reasoning/bug-validation flow.

uv run python main.py <proj_dir> --only-spec

Use --extra-edge FILE when the static parser cannot see an important call relationship, such as indirect syscall dispatch. Supplemental edges are applied to full, entry-point-scoped, and incremental runs. The JSON shape is:

{
  "edges": [
    {
      "caller": {
        "fqn": "third_party::musl::src::time::nanosleep-c::nanosleep",
        "callsite_names": ["nanosleep"]
      },
      "callee": {
        "fqn": "kernel::liteos_a::syscall::time_syscall-c::SysNanoSleep",
        "info_names": ["__NR_nanosleep", "SYS_nanosleep", "nanosleep"]
      }
    }
  ]
}

Extra-edge field rules:

  • caller.fqn: exact FQN for a single caller, adding one edge to callee.fqn. It may be empty.
  • caller.callsite_names: source callsite function names. Any function containing these callsites becomes a caller and gets an edge to callee.fqn. It may be empty.
    • At least one of caller.fqn and caller.callsite_names must be non-empty.
  • callee.fqn: exact FQN for a single callee.
  • callee.info_names: optional names used to match callee entries in generated .info.json files. They are only used for .info.json matching and passing caller expectations.

Incremental Mode

In incremental mode, FM-Agent reuses the results of a previous run and only re-checks what changed. It diffs the current code against the commit recorded by the previous run in fm_agent/version.log. Each run records the processed commit id to that file, so a subsequent --incremental run automatically picks it up:

python3 main.py <proj_dir> --incremental <intent_file>

If fm_agent/version.log does not exist (no previous run to compare against), FM-Agent falls back to a full run.

Live Dashboard

FM-Agent ships a standalone real-time TUI dashboard (dashboard.py) that visualizes a run as it progresses: per-stage progress, token usage and cost, prompt-cache hit rate, and bug-validation verdicts. It reads the trace files FM-Agent writes under fm_agent/, so run it in a second terminal while main.py is going:

uv run python dashboard.py <proj_dir>
Argument Description
proj_dir Same codebase directory passed to main.py (monitors <proj_dir>/fm_agent/). You can also point it directly at any workspace directory containing a trace/ subdir, e.g. an archived run

Press Ctrl-C to exit the dashboard; it does not affect the running pipeline.

Output

FM-Agent creates an fm_agent/ directory under your codebase directory. The key outputs are:

Bug Reports (fm_agent/bug_validation/<bug_id>.md)

Each confirmed or investigated bug produces a Markdown report containing:

Section Content
Specification Claim The post-condition that the function specification requires
Actual Behavior The post-condition that the code actually implements
Code Evidence The specific code statements (with line numbers) that cause the violation
Trigger Condition A description of the condition that triggers the bug
How to Trigger Concrete input parameters, expected vs. actual output, and reproduction steps
Probe Script The full test script used to confirm the bug
Probe Output Raw stdout from executing the probe script

A summary.json file in fm_agent/bug_validation/ aggregates all bug results with counts of total reported, confirmed, not confirmed bugs. In --all-bugs mode, the summary additionally reports pending candidates; a missing, corrupt, or non-terminal validation is pending instead of disappearing from the totals. Default-mode summary behavior is unchanged.

Important Notes

  1. FM-Agent will create an fm_agent/ directory under your codebase directory. Make sure there is no name conflict.
  2. The markdown files under md/ provide general instructions that guide the agent's reasoning process. Prefer --domain-knowledge for project-specific context such as invariants, protocols, encoding rules, and domain terminology. For project-specific bug-validation procedures, use --bug-validator instead of editing the built-in prompt; for example, a compiler-specific validator can instruct the agent to compare outputs against a reference implementation such as GCC.
  3. Supported languages: Rust, C, C++, Python, Java, Go, CUDA, JavaScript, TypeScript, ArkTS, Erlang. Erlang function extraction and call graphs require ELP; if ELP is unavailable, Erlang files are skipped with a warning.

Citation

If you use FM-Agent in your projects or research, please kindly cite our paper:

@misc{ding2026fmagent,
Author = {Haoran Ding and Zhaoguo Wang and Haibo Chen},
Title = {FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning},
Year = {2026},
Eprint = {arXiv:2604.11556},
}

Contact

If you have any questions, please submit an issue or send email.