MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs

MAGS 先冻结人工审计的 API 和安全要求，再把代理代码翻译到 Dafny，循环利用形式验证反馈修复，最后编译回可执行程序。100 个 CUDA 内核、100 个终端脚本和 20 个机械臂任务全部产出带非平凡安全保证的程序，但独立测试也指出：若自动形式化的语义没有覆盖目标行为，证明只保证了错误的规格。它展示的是“把证明工程变成多代理流水线”，不是免除规格设计的万能验证器。