MAGS：多智能体自动形式化，为智能体输出提供安全保证

arXiv 论文提出多智能体框架 MAGS，用于为 LLM 生成的程序提供形式化安全保证。它把经人工审核的 API 与安全需求固化，将生成代码翻译为 Dafny 中间表示，借助验证器反馈修复违规，再编译回可执行代码。在 100 个 CUDA kernel、100 个终端脚本和 20 个机械臂任务共 220 个样例中，针对冻结规范产出非平凡安全保证的成功率为 100%。

此前 fuzz 测试、静态分析和 LLM-as-a-Verifier 只能覆盖部分失败路径，难以穷尽边界情况；人工形式化验证又依赖大量手动规范和证明工程。MAGS 把形式化验证变成多智能体可自动执行的流程，使大规模 LLM 生成代码有机会获得机器可检查的安全保证。

机制是把“人类审核后的 API 与安全需求”冻结为验证基准，让生成代码经由 Dafny 这一验证感知中间表示接受机械检查；验证器反馈驱动违规修复，最终把通过验证的程序编译回可执行形态。这样，安全保证不依赖模型自我判断，而依赖可被机械检查的规范。

对研发流程而言，可为代码生成环节加入自动形式化闸门：先冻结接口与关键安全属性，再让生成、验证、修复循环自动运行，减少人工审查负担。对安全敏感场景，可把验证通过作为上线前置条件；但需注意，当自动形式化语义未能完整覆盖目标行为时仍会出现失败。

• 在 CI/CD 中集成 Dafny 验证环节，对安全关键模块设置“验证通过才可合并”的门禁。
• 面向 CUDA kernel、终端脚本和机器人控制三类场景，沉淀可复用的冻结 API 与安全需求模板库。
• 开发验证失败反馈的自动修复服务，按违规类型生成补丁并重新验证。
• 为形式化验证结果提供可审计报告，向客户或监管方展示机器可检查的安全保证。

• MAGS 在 220 个样例上的 100% 成功率能否推广到更大规模、更多编程语言和更复杂的安全属性？
• 独立安全与功能评估的具体指标、基线和测试方法尚未给出，结果可比性待确认。
• 当自动形式化语义未完整覆盖目标行为时，失败率与误判边界分布在哪些任务类型上？
• 冻结规范的人工审核成本、维护成本和生产环境吞吐量尚未披露。