FM-Agent：通过基于大模型的霍尔逻辑推理将形式化方法扩展至大规模系统软件

FM-Agent 是首个实现大规模系统正确性全自动推理的框架，支持的软件包括14万行代码的 Claude C Compiler。

它包含三个步骤：

• 规约生成：自主理解开发者的系统设计意图，为每个函数生成正确性规约。
• 代码推理：无需任何人工干预，自动推理出代码实现是否符合正确性规约的要求。
• 缺陷诊断：对于有 bug 的函数，基于推理过程分析bug的根因与位置。

FM-Agent 的官方网站提供了在线代码库推理服务，欢迎体验！

⚠️ 注意：本框架的推理效果受所使用模型的能力影响较大。使用能力较弱的模型时，可能出现幻觉（hallucination），导致错误的推理结论。建议选择推理能力较强的模型，以获得更可靠的结果。

目录

• 文件结构
• 环境配置
  • 依赖要求
    • 已测试macOS环境
  • 安装依赖
• 参数配置
• 快速开始
• 注意事项
• 论文引用
• 联系方式

文件结构

|-- main.py                       # 程序入口 —— 编排整个流水线
|-- dashboard.py                  # 独立的实时 TUI 监控面板
|-- config.py                     # 配置（模型、粒度、并发、超时等）
|-- install.sh                    # 依赖安装脚本
|-- pyproject.toml / uv.lock      # Python 项目元数据与锁定的依赖（uv）
|-- .env.example                  # .env 运行时配置模板
|-- src/                          # 核心源码模块（提取、推理、LLM 交互等）
|-- md/                           # 引导 Agent 推理的工作流说明文档
|-- docs/                         # 补充文档（如 OpenCode/LLM provider 配置）

环境配置

依赖要求

• Ubuntu（已在 22.04 LTS, 24.04 LTS 上测试）
• Python 3.12
• pip >= 23
• openai 2.15.0
• OpenCode 1.4.6
• Bun
• oh-my-openagent 插件（通过 bunx 安装）
• @lucentia/opencode-trace 插件 —— 采集 OpenCode 原始 LLM 请求/响应 trace
• 你所用 provider 的 LLM API 密钥（示例使用 OpenRouter）
• Clang——可选；可用时用于生成更准确的 C/C++ 调用图，Clang 无法分析的函数会逐函数回退到 codegraph。FM-Agent 会读取项目根目录或 build/ 下的 compile_commands.json；其他位置可通过 CLANG_COMPILE_COMMANDS 指定。
• Erlang Language Platform（ELP）——可选，仅分析 Erlang 项目时需要
  • 本 Erlang 集成已在 Ubuntu 的 Erlang/OTP 26 或更高版本上验证；请选择基于兼容 OTP 版本构建的 ELP 发布包。
  • ELP 自动识别包含 rebar.config 的项目时，要求 rebar3 3.24.0 或更高版本。
  • 本集成尚未测试 macOS Erlang 工具链；./install.sh --with-erlang 会安装 Homebrew 当前提供的公式版本。

已测试macOS环境

以下 macOS 环境已使用安装脚本测试：

• 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

安装依赖

设置 FM-Agent 和 OpenCode 共用的 LLM API 密钥。推荐使用 OpenRouter：FM-Agent 会并发调用 LLM，而 OpenRouter 的 RPM（每分钟请求数）和 TPM（每分钟 Token 数）限制更宽松——不过任何兼容的 provider 都可以。

把 API 密钥放进 .env（已 gitignore，FM-Agent 通过 python-dotenv 自动加载）；其余所有配置在 fm-agent.toml 里都有 committed 的默认值。最简单的配置方式是运行交互式向导：

uv run python src/configure_llm.py

该向导会先展示预览、备份已有文件，然后更新当前生效的 FM-Agent TOML、把 API 密钥写入 .env 和供独立 OpenCode 使用的私有本地密钥文件，并同步对应的 OpenCode provider 到 ~/.config/opencode/opencode.json（或当前平台上的等价路径），无需手写 JSON。 若在向导中选择 auto、codex-cli、claude-cli 或 dsh，则会询问模型 ID，将后端和所选模型写入当前生效的 FM-Agent TOML，并清除项目 .env 中残留的非密钥 LLM 覆盖项，保留 effort 到 TOML。Codex 和 Claude 使用各自 CLI 的认证；DSH 需要 DEEPSEEK_API_KEY，使用网关时再设置 DEEPSEEK_BASE_URL。

如果你更希望手动编辑文件，可以复制模板：

cp .env.example .env
# 然后编辑 .env，填入 LLM_API_KEY

# .env（只放密钥）
LLM_API_KEY=your-api-key-here

非密钥配置——模型、endpoint、backend、provider 等——在 fm-agent.toml 的 [llm] 段，直接改它是永久生效的做法。若不想动这个被 git 跟踪的文件（比如你是 git clone、之后会 git pull 更新），可以用对应的环境变量覆盖，写在 .env 或 shell 里即可。优先级为 env > .env > fm-agent.toml；由于 .env 会盖过 toml，残留的旧值会覆盖你后来对 toml 的修改——所以改了 toml 不生效时，先检查 .env。向导会顺手清理常见的旧 LLM 覆盖变量，并在启动向导的 shell 已导出 LLM 变量时提示使用 unset，否则该变量仍会覆盖保存的配置。详情及 OpenCode provider 配置见 docs/config_llm.md。

如需只修改某一项非密钥 LLM 配置，无需手动编辑文件。例如，将模型后端切换到本地 Codex CLI：

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

该命令会预览并备份 fm-agent.toml，只修改命令中指定的配置项。它还支持 --name、--provider、--base-url、--effort 和 --api-style；完整语法见 docs/config_llm.md。若 .env 中仍有会覆盖本次 TOML 修改的旧值，命令会在写入前给出警告。

上述核心依赖可通过以下脚本一键安装；可选的 Clang 与 Erlang 工具链默认不安装：

./install.sh

Erlang 工具链不影响其他语言，因此默认不安装。如需自动安装或检查 Erlang/OTP 26+、rebar3 3.24.0+ 和兼容的 ELP 发布包，请运行：

./install.sh --with-erlang

该选项在 macOS 上使用 Homebrew；在 Ubuntu 上，当系统 OTP 缺失或版本过低时使用 RabbitMQ Team Erlang PPA。Ubuntu 配置已使用 Erlang/OTP 26+ 验证；macOS Erlang 配置尚未测试，将使用 Homebrew 选择的当前公式版本。Linux 下的 rebar3 和 ELP 会安装到 ~/.local/bin，请确保新终端的 PATH 包含该目录。你也可以手动安装这些工具，确认 rebar3 version 和 elp version 可执行，并在需要时将 ELP_COMMAND 设置为 ELP 的绝对路径。

FM-Agent 会从 fm-agent.toml 自动配置 OpenCode 的 provider，因此无需手动编辑 ~/.config/opencode/opencode.json 来设置模型或密钥。上面的配置向导仍然可以把该文件同步好，并把 API 密钥写入用户状态/配置目录下按 provider 区分的私有本地文件，方便独立使用 OpenCode（见 docs/config_llm.md）。 如果你已经设置了 OPENCODE_CONFIG，向导会优先更新那个文件，而不是默认的全局路径。若未设置该变量但设置了 OPENCODE_CONFIG_DIR，向导会更新该目录中的 opencode.jsonc（存在时）或 opencode.json。

重要提示： FM-Agent 会根据推理过程自动生成测试用例，以触发潜在 Bug，帮助开发者定位和修复问题。运行 FM-Agent 前，请确保目标代码库的测试环境已就绪。如需提供项目特定的验证指令，请使用 --bug-validator；否则，Agent 将自主决定测试用例的执行方式。

参数配置

配置项都在 fm-agent.toml 里（每一项都有就近注释），也可用对应的环境变量覆盖。完整参数、默认值与描述的参考表见 docs/configuration_zh.md。

重要说明： 建议选择推理能力较强的模型，以提高发现 Bug 的可靠性。请确保 API 密钥有权访问所选模型。

（可选）FM-Agent 使用 oh-my-openagent 插件增强 OpenCode。该插件内置的 comment-checker 钩子应当禁用，否则它会拦截 FM-Agent 写入的每一个注释块（这些注释是函数的正确性规约），并迫使 Agent 消耗大量 Token 去论证注释的必要性或将其删除。 请打开 oh-my-openagent 配置文件（通常位于 ~/.config/opencode/oh-my-openagent.json），添加 disabled_hooks：

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

快速开始

uv run python main.py <proj_dir> [--resume] [--all-bugs] [--domain-knowledge FILE ...] [--bug-validator FILE] [--submodule PATH [PATH ...]]

参数	描述
proj_dir	待检测代码库的目录路径
--resume	续跑上一次中断的运行，而非从头开始
--resume-from WORKSPACE	从归档恢复并续跑，同时保留所选归档和当前运行；需重复原分析选项
--incremental INTENT_FILE	以增量模式运行，参数值为描述本次修改目标的意图文件路径。
--all-bugs	在发现不匹配后继续推理并报告每个候选 Bug。完整和增量模式会逐个验证。
--domain-knowledge FILE [FILE ...]	将额外的 Markdown 领域知识文件复制到本次运行中，并提供给 setup、规约生成和 Bug 验证 Agent。别名：--knowledge；可重复传入。
--bug-validator FILE	使用自定义 Markdown 提示词执行 Bug 验证，替代内置的 md/bug_validator.md。
--isolate	针对项目的隔离 git worktree 快照运行，而非直接在项目目录上运行。
--submodule PATH [PATH ...]	只处理 proj_dir 中一个或多个子目录下的源代码。
--extra-edge FILE	从 JSON 文件或目录向静态调用图补充 caller 到 callee 的边。
--only-spec	只生成行为规约，跳过推理与 Bug 验证阶段。不能与 --incremental 一起使用。
--estimate	不调用 LLM，仅扫描范围并输出基于历史数据的时间、LLM 调用次数、Token 与费用预估。
--plugin NAME	加载 plugins/NAME/ 下的 Pipeline 插件。
--list-plugin	列出有效的 Pipeline 插件并退出。

Pipeline 插件

FM-Agent 插件可以通过受信任的 Python Hook 跳过、替换或修改六个 Pipeline Stage。所有 Hook 使用统一签名：

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

插件目录结构、JSON 配置、执行模式、生命周期和信任边界参见 Pipeline 插件。

proj_dir 必须是一个 git 仓库。

运行前预估

在消耗任何模型 Token 前检查计划分析的代码范围：

uv run python main.py <proj_dir> --estimate
uv run python main.py <proj_dir> --estimate --submodule src/core src/runtime

预检会展示纳入和排除的目录、纳入/排除的源文件数量、通过本地抽取得到的近似函数数量，以及六个分析阶段。当存在已完成的历史运行时，FM-Agent 会按本次函数数量（缺失时退化为文件数量）缩放历史运行的实际耗时、LLM 调用次数、Token 用量和费用，并给出区间。所有预测值都会明确标注为 ESTIMATE（估算）；没有完整历史样本时会显示无法估算，而不会编造数值。

成功运行的摘要会保存在 fm_agent/history.jsonl，并在全新运行归档旧工作目录时继续保留；估算也会读取已完成的归档运行。正常运行会在第一次 LLM 调用前生成 fm_agent/estimate.json，实时 Dashboard 会同时展示该预检和实际用量。

如需在不修改 FM-Agent 内置提示词的情况下提供项目特定领域知识，可传入一个或多个 Markdown 文件：

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

FM-Agent 会将这些文件暂存到 fm_agent/spec_prompts/domain_context/user_knowledge/，并在本次运行中让相关 Agent 读取。也可以通过 FM_AGENT_DOMAIN_KNOWLEDGE 提供使用 os.pathsep 分隔的 Markdown 文件列表。

如需自定义候选 Bug 的测试与确认方式，可通过 --bug-validator 指定 Markdown 文件：

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

该文件会替代内置 md/bug_validator.md 的验证指令。使用自定义 --bug-validator 验证 --all-bugs 候选时，FM-Agent 会规定最终结果 JSON 的写入路径、必需字段及合法取值，以便可靠地读取和校验验证结果，并在 --resume 时安全复用。--bug-validator 的相对路径以启动 FM-Agent 命令时的当前目录为基准，而不是以 proj_dir 为基准。FM-Agent 仍会在每个 Bug 验证提示词中加入当前 Bug ID、目标验证结果，以及通过 --domain-knowledge 提供的领域知识。

使用 --submodule 可以把完整运行或增量运行限制到指定项目子目录：

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 路径必须是 proj_dir 内部目录。该参数可与 --resume、--isolate 和 --incremental 一起使用。

--all-bugs 可用于完整或增量分析：

uv run python main.py <proj_dir> --all-bugs
uv run python main.py <proj_dir> --incremental intent.md --all-bugs

该选项默认关闭。启用后，FM-Agent 会继续检查后续推理检查点，并为每个候选写出一个标准 mismatch 结果。完整和增量模式会分别验证每个候选。

若主结果为 path/to/function.json，all-bugs 候选会写在同一目录下，依次命名为 path/to/function.bug-001.json、bug-002.json 等。主结果通过 bug_count 和 reasoning_complete 记录候选数量及推理是否完整。续跑时，完整的主结果就是 reasoning 阶段的检查点，只补跑尚未产生终态结果的候选验证；若 reasoning 中途停止，则只清理并重跑该函数的中间候选和验证，不影响其他已完成函数。

默认情况下，全新完整分析会先将旧 fm_agent/ 中的分析产物移至 <proj_dir>.fm_agent_runs/<UTC时间戳>_<唯一ID>/，保留报告、trace、规约、验证证据及续跑检查点。当前运行仍位于 <proj_dir>/fm_agent/，CLI 会输出当前路径和归档路径。归档位于项目旁边，避免 CodeGraph 和项目 Agent 扫描旧代码及报告。空工作区或只有 .env_check_memory 的工作区不归档；该文件保存的忽略警告设置留在当前工作区，恢复归档和回写结果时也保留当前设置。环境检查仅在保存用户选择的忽略警告设置时创建工作区。归档失败时停止分析，保留原目录。历史归档不会自动删除，仅在你不再需要时自行显式删除。全新的 --isolate 和 --entry-func 运行也遵循这一规则；它们复制结果回原项目时同样会先保留旧工作区。

归档和结果回写使用同一文件系统内的重命名操作，需要项目的父目录可写，且项目、归档和复制暂存目录位于同一文件系统。如果项目本身是独立挂载点，可能不满足这一条件；操作失败时会保留已有结果。复制暂存目录位于项目旁边的 .<项目名>.fm_agent_publish_*/，强制终止后即使有残留，也不会进入项目的分析范围。

使用 --resume（或环境变量 FM_AGENT_RESUME=1）可保留当前工作区并继续剩余工作。若中断后误启动了新运行，可通过 --resume-from 恢复之前的归档：

uv run python main.py <proj_dir> --resume
uv run python main.py <proj_dir> --resume-from <proj_dir>.fm_agent_runs/<归档ID>
uv run python report.py <proj_dir>.fm_agent_runs/<归档ID>

恢复过程会复制所选归档、归档当前工作区，再从 fm_agent/ 续跑；所选归档仍保留，便于比较。续跑需使用中断时的源代码版本和分析选项，恢复产物不会自动切换或回退源代码。尤其是 all-bugs 工作区必须带 --all-bugs，不兼容的推理模式会被拒绝。--resume-from 不可与 --resume、--incremental 或 --estimate 同时使用。

--resume-from WORKSPACE 支持绝对路径、相对路径和 ~；相对路径以启动命令时的当前目录为基准。

新运行在分析开始前写入 fm_agent/run.json，记录稳定的运行 ID、时间、项目路径、Git HEAD 和是否存在未提交修改；HTML 报告也显示运行 ID 和版本。可以直接打开归档中的 report.html 查看已保存的报告，或用上述命令依据归档证据重新生成（重新生成时的源代码预览取决于源代码是否仍可访问）。没有 run.json 的旧版工作区也可保留和恢复。历史估算会使用已完成的归档运行。增量模式继续在原工作区中更新结果。

使用 --only-spec 可以在生成行为规约后即停止，跳过推理与 Bug 验证阶段。它会为每个函数生成相邻的 .spec.json 和 .info.json 元数据文件，而不在验证上花费时间，适用于只需要规约、或希望先审阅规约再运行完整分析的场景。该参数不能与 --incremental 一起使用，因为增量模式本质上是一个推理/Bug 验证流程。

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

当静态解析无法看到关键调用关系时（例如间接 syscall 分发），可使用 --extra-edge FILE。补充边会同时作用于完整运行和增量运行。JSON 格式如下：

{
  "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 字段规则：

• caller.fqn：单个 caller 的精确 caller FQN，补一条到 callee.fqn 的边。可以为空。
• caller.callsite_names：源码 callsite 函数名。源码中包含这些 callsite 的函数都会作为 caller，补一条到 callee.fqn 的边。可以为空。
  • caller.fqn 和 caller.callsite_names 至少有一个非空。
• callee.fqn：单个 callee 的精确 FQN。
• callee.info_names：可选，用于匹配生成的 .info.json 中指代该 callee 的条目。它只用于 .info.json 匹配和传递调用者期望。

增量模式

增量模式会复用上一次运行的结果，仅重新检测发生变化的部分。它将当前代码与上一次运行记录在 fm_agent/version.log 中的提交进行 diff。每次运行都会把所处理的提交 id 写入该文件，因此后续的 --incremental 运行会自动读取它：

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

如果 fm_agent/version.log 不存在（没有可供比较的历史运行），FM-Agent 会回退为完整运行。

实时监控面板

FM-Agent 自带一个独立的实时 TUI 监控面板（dashboard.py），用于在运行过程中可视化展示：运行前范围与估算、各阶段进度、Token 用量与花费、prompt 缓存命中率，以及 Bug 验证结果。它读取 FM-Agent 写入 fm_agent/ 目录下的 trace 文件，因此可在 main.py 运行期间于另一个终端中启动：

uv run python dashboard.py <proj_dir>

也可以直接在主命令中启用，Dashboard 会自动关联本次运行的工作目录，并在流水线结束时退出：

uv run python main.py <proj_dir> --dashboard

如需在不启动流水线、不调用 LLM 的情况下生成并展示一次运行前估算：

uv run python dashboard.py <proj_dir> --estimate
uv run python dashboard.py <proj_dir> --estimate --submodule src/core src/runtime

参数	描述
proj_dir	与 main.py 相同的代码库目录（监控 <proj_dir>/fm_agent/）。也可直接指向任意包含 trace/ 子目录的工作区目录，例如已归档的运行

按 Ctrl-C 退出监控面板，不会影响正在运行的流水线。

输出说明

FM-Agent 会在代码库目录下创建 fm_agent/ 目录，主要输出内容如下：

Bug 报告（fm_agent/bug_validation/<bug_id>.md）

每个已确认或经过排查的 Bug 都会生成一份 Markdown 报告，包含以下内容：

条目	含义
Specification Claim	函数正确性规约要求满足的后置条件
Actual Behavior	代码实际上满足的后置条件
Code Evidence	导致 Bug 的具体代码语句
Trigger Condition	触发 Bug 的条件
How to Trigger	触发 Bug 的具体步骤
Probe Script	用于触发 Bug 的完整测试脚本
Probe Output	执行测试脚本的输出

fm_agent/bug_validation/ 目录下的 summary.json 文件汇总了所有 Bug 结果，包括报告的 Bug 总数、已确认 Bug 数、未确认 Bug 数。在 --all-bugs 模式下，汇总还会报告待验证候选；缺失、损坏或尚未进入终态的验证结果会显示为 pending，而不会从统计中消失。默认模式的汇总行为保持不变。

交互式报告索引（fm_agent/report.html）

每次完整流水线运行结束后（包括仅生成规约的 --only-spec 模式），会自动生成一个自包含的 report.html 索引页，将 Bug 验证结果与逐函数逻辑验证结果汇总到同一页面。该页面完全由运行产物渲染而成——不调用 LLM、不联网、无额外依赖。

每一行展示报告标题、状态徽章、源文件（可点击跳转到原始源码）、函数名与代码位置。页面支持：

• 搜索：按标题、源文件、函数名搜索
• 筛选：按状态（confirmed_bug / potential_bug）与源文件筛选
• 排序：按状态、源文件或函数名排序
• 展开/折叠：单个报告与全部报告一键展开/折叠，以及重置按钮

页面写入 fm_agent/report.html，用浏览器打开即可浏览。也可随时基于任意已有运行的产物重新生成：uv run python report.py <项目目录>（也可直接传入 fm_agent/ 工作目录或归档的工作区目录）。增量模式（--incremental）不会自动生成该页面，需手动运行上述命令。

日志文件（fm_agent/fm_agent.log）

单一日志文件记录完整的流水线执行过程，包括文件提取进度、推理任务的提交与完成情况、网络错误与重试，以及最终的推理统计摘要。日志级别为 INFO，格式为 %(asctime)s [%(levelname)s] %(message)s。

注意事项

1. FM-Agent 会在代码库目录下创建 fm_agent/ 目录，请确保不存在命名冲突。
2. md/ 目录下的 Markdown 文件提供了引导 Agent 推理过程的通用说明。针对项目特定的上下文（如不变量、协议、编码规则、领域术语），优先使用 --domain-knowledge。对于项目特定的 Bug 验证流程，请使用 --bug-validator，无需直接修改内置提示词；例如，编译器项目的自定义 validator 可以要求 Agent 将输出与 GCC 等参考实现进行对比。
3. 支持的编程语言：Rust、C、C++、Python、Java、Go、CUDA、JavaScript、TypeScript、ArkTS、Erlang。C/C++ 调用图对 Clang 分析成功的函数使用 Clang，其余函数使用 codegraph。Erlang 的函数抽取与调用图需要 ELP；ELP 不可用时会给出警告并跳过 Erlang 文件。

论文引用

如果您使用了 FM-Agent，请引用我们的论文：

@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},
}

联系方式

如有任何问题，欢迎提交 Issue 或发送邮件联系。