FM-Agent：通过基于 LLM 的霍尔风格推理将形式化方法扩展至大型系统

针对大语言模型生成的大规模系统代码难以自动验证的问题，本文提出 FM-Agent 框架。该框架利用 LLM 采用自顶向下范式，根据调用者期望自动生成函数级自然语言规范，克服了传统霍尔逻辑需人工编写形式化规范的瓶颈。通过将霍尔风格推理泛化以支持自然语言规范，并自动生成测试用例触发潜在缺陷，FM-Agent 实现了对含十余万行代码系统的自动化组合推理。实验表明，该系统能在两天内发现 522 个未被察觉的严重漏洞。