FM-Agent

FM-Agent 是一个基于大语言模型（LLM）实现霍尔风格组合式形式化推理的自动化框架，用于对大规模软件系统（如十余万行代码的C编译器）进行可扩展的形式化验证。其核心功能包括代码结构提取、模块化契约推导、跨函数/文件的Hoare三元组推理链构建，以及自动生成触发潜在缺陷的测试用例；技术上采用多LLM协同调度（通过OpenRouter）、支持细粒度配置与并发推理，并依赖强推理能力模型（如Claude Opus/Sonnet）保障结论可靠性。适用于需要在工业级代码库中开展轻量级、自动化形式化分析与缺陷定位的研究与开发场景。