多智能体框架 MAGS 把代码生成的验收标准从「能跑通」抬到了「可证明正确」：在 100 个 CUDA 内核、100 个终端脚本与 20 个机械臂任务合计 220 个样例上，它全部产出了针对冻结规范带有非平凡安全保证的程序，成功率 100%。其枢纽是把 Dafny 作为验证感知的中间表示，让模型写出的代码先进入可被机器检查的形态，再由验证器反馈驱动修复。
一、MAGS 要补的缺口：生成规模超过人工审查能力
编码智能体如今能批量产出复杂程序，逐行人工审查反而成了瓶颈，风险被推迟到集成、上线甚至物理执行时才暴露。MAGS 的出发点很直接：与其事后补救，不如让安全成为生成过程的内置约束。
现有检测手段的天花板
模糊测试、静态分析和「让另一个大模型当验证器」是常见三板斧，能抓住不少缺陷，共同问题却是覆盖不完整：模糊测试依赖抽样，静态分析受限于规则，模型验证器本身也没有硬保证。
形式化验证的旧门槛
形式化验证能对指定属性给出机器可检查的保证，强度远超抽样测试。代价是它长期需要人工撰写规范、设计不变式、维护证明工程，难进日常开发流。MAGS 想用多智能体流水线把这份成本摊薄并前置。
二、工作机制：Dafny 作为验证感知的中间表示
先把人工审计过的接口与要求冻结
第一步是把人工审计过的 API 与安全要求形式化并冻结，此后生成、翻译与修复都对照这份规范接受检查。这把人的判断固定在信任链最上游，避免模型边写边解释、自己给自己打分的循环论证。
翻译—验证—修复—回编译的闭环
链路是：智能体生成程序，系统翻译成 Dafny 中间表示；验证器检查安全属性，发现违反就把失败信息反馈给智能体做定向修复；通过后编译回可执行代码。判据不再是抽样用例是否通过，而是属性是否被机械证明。
| 环节 | 常见做法 | MAGS 的做法 |
|---|---|---|
| 需求来源 | 模型自行理解任务 | 人工审计后形式化并冻结 |
| 中间形态 | 直接产出目标代码 | 翻译为 Dafny 中间表示 |
| 验收判据 | 用例通过、人工抽查 | 验证器机械检查属性 |
| 失败处理 | 重新采样、整体重试 | 按验证器反馈定向修复 |
| 最终产物 | 可运行代码 | 带安全保证的可执行代码 |
三、220 个任务、三个领域：结果如何
评测覆盖 GPU 侧的 CUDA 内核、系统侧的终端脚本，以及直接作用于物理世界的机械臂控制，三类合计 220 个样例，跨度从纯计算延伸到物理执行。
| 任务领域 | 样例数量 | 论文报告的结果 |
|---|---|---|
| CUDA 内核 | 100 | 均产出带非平凡安全保证的程序 |
| 终端脚本 | 100 | 均产出带非平凡安全保证的程序 |
| 机械臂任务 | 20 | 均产出带非平凡安全保证的程序 |
| 合计 | 220 | 成功率 100% |
论文给出的结论是：在全部 220 个样例上，MAGS 达成 100% 的成功率，所产程序都带有针对冻结规范的非平凡安全保证；独立的安全性评估与功能性评估在三个领域均有不错表现，同时也暴露出自动形式化语义未完整刻画目标行为时的失败。
四、失败模式：自动形式化抓不住的语义偏差
论文明确指出一类失败：当自动形式化得到的语义没有完整刻画目标行为时，系统仍会出错。这点是形式化方法的固有边界——验证器只能证明程序符合被写下来的规范，无法证明写下来的规范就是人真正想要的。规范本身仍需人工投入，这也解释了 MAGS 为何坚持在入口处冻结人工审计结果。
五、谁该关注，谁不必急着上
受益最直接的是代码出错代价极高的场景：内核中的越界与并发、运维脚本里的破坏性命令、机器人控制中的物理约束，都属于规范可写、后果难承受的类型。反之，若需求天天变、连人都说不清正确行为，先投规范工程并不划算；翻译与多轮修复也会带来额外开销，延迟敏感场景需权衡。
FAQ：关于 MAGS 你最可能关心的 3 个问题
MAGS 和「生成代码再补单元测试」有本质区别吗？
有。单元测试是有限用例抽样，通过只说明这些用例没出问题；MAGS 依赖验证器对安全属性的机械检查，覆盖属性空间而非若干样本。修复依据也不同：前者靠重采样碰运气，后者靠验证器给出的具体违反点定向修改。
为什么中间表示选的是 Dafny？
因为 Dafny 自带规范与验证机制，前置条件、后置条件、循环不变式这类构造可被机械检查。作为中间层还有工程好处：验证能力只需实现一次，就能通过「翻译进去、编译出来」复用到多种目标语言与任务类型。
100% 成功率是不是等于代码绝对安全？
不等于。100% 指 220 个样例都产出了带非平凡安全保证的程序，保证范围严格限于被冻结的规范。规范未覆盖的行为、自动形式化与目标语义的偏差仍是风险来源，理解成「在给定规范内可证明」更准确。
小结
MAGS 的价值不在让模型写出更花哨的代码，而在给智能体的产出装上可检查的信任链：人工审计的规范冻结在最上游，Dafny 中间表示承担机械验证，验证器反馈驱动修复，最后回编译成可执行程序。它把「可证明正确」从论文概念推向可流水线执行的工程流程。对准备把编码智能体放进生产环境的团队来说，规范工程而非提示词工程，可能是下一阶段真正要补的功课。
消息来自 HEX2077 AI资讯日报（2026年9月19日），原始出处 arXiv 2609.19391：MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs