智能体写代码的规模已经超出了人能审的范围。模糊测试、静态分析、LLM 当审查员，这些手段能抓到很多问题，但都是抽样式的——抓不到所有边角。形式化验证本可以给出机器可查的硬保证，问题是它传统上要求大量的人工规格书写与证明工程，贵到一般团队用不起。arXiv 2609.19391 提出的 MAGS，试图用多智能体把这道工序自动化。
流水线分四步：先把人工审计过的 API 与安全属性形式化并冻结，作为机器可查的判据；智能体生成的程序被翻译成验证感知语言 Dafny 作为中间表示；证明检查器标记违例，反馈驱动修复，循环到通过；末了把带证明的代码编译回可执行形式。人只出现在规格冻结那一环——这是刻意的设计：把人的判断压缩到责任最清晰的位置。
220 个真实任务的答卷
评测选了三个差异极大的域：100 个 CUDA 内核、100 个终端脚本、20 个机械臂任务。220 个例子里，MAGS 全部产出了对冻结规格具备非平凡安全保证的程序，达成率 100%。独立的第三方安全与功能评测进一步确认了三个域上的表现——这比「自己出的题自己全对」有说服力得多。
但论文没有回避软肋。独立评测同时暴露了失效模式：当自动形式化的语义没有吃准目标行为时，程序依然会错，而且错在数学看不见的地方。MAGS 保证的是「代码符合人写下的规格」，规格本身有没有写全，机器不背书。用论文自己的定位说，这是一条可靠的安全带，不是自动驾驶。
和抽样式检测怎么分工
需要说明的是，MAGS 不是来取代模糊测试与静态分析的。三者的分工其实很清楚：模糊测试便宜、适合扫运行时的崩溃面；静态分析快、适合抓已知模式的缺陷；形式化验证贵但完备，适合兜住安全关键属性。MAGS 的贡献是把第三类成本压到一个可接受的位置，让「给关键属性上数学证明」从奢侈品变成流程选项。
另一个现实约束是规格的质量：冻结的人工审计规格是整条流水线的地基，规格写偏了，后面的百分百达成率只是精确地满足了错误的目标。所以引入这条流水线的团队，真正的投入点不在跑验证，而在规格评审——这恰好是把人力用在了机器最不擅长的地方，方向是对的。
为什么值得编排层关注
这项工作对智能体赛道有两层意义。技术层面，它示范了多智能体分工的一种严肃用法：不是把一个任务切碎了分给几个模型聊天，而是让生成、翻译、修复各司其职，中间用形式化工具做硬校验——协作的价值被一个机器可查的判据锚定了，不再依赖主观评分。
产业层面，随着编码智能体进入金融、工业控制这类出错代价高昂的场景，「生成的代码带不带可验证保证」会从加分项变成准入项。MAGS 路线把形式化验证的成本从「养一个证明工程师团队」降到「冻结一份规格 + 跑一条流水线」，中间的落差正是未来一两年的工程机会。目前官方及行业暂未披露更多细节，后续将持续跟进迭代动态。