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

MAGS：多智能体自动形式化保障智能体输出的安全性

LLM coding agents now generate complex programs at a scale that makes thorough human review increasingly difficult, raising the risk of safety and security failures. Common approaches, including fuzz testing, static analysis, and LLM-as-a-Verifier, can detect many failures but struggle to cover all possible edge cases. 大语言模型（LLM）编程智能体目前生成的复杂程序规模巨大，使得全面的人工审查变得愈发困难，从而增加了安全和合规性失效的风险。常见的处理方法，包括模糊测试、静态分析以及“LLM 作为验证者”（LLM-as-a-Verifier），虽然能够检测出许多故障，但在覆盖所有可能的边缘情况时仍显得力不从心。

Formal verification addresses this by providing machine-checkable guarantees over specified properties, but traditionally demands substantial manual specification and proof engineering. We introduce a unified multi-agent framework, MAGS, that generates executable programs with formal safety guarantees, using Dafny as a verification-aware intermediate representation where safety properties can be mechanically checked. 形式化验证通过对特定属性提供机器可检查的保证来解决这一问题，但传统上需要大量的手动规范编写和证明工程。我们引入了一个统一的多智能体框架 MAGS，它能够生成具有形式化安全保证的可执行程序。该框架使用 Dafny 作为具备验证意识的中间表示，从而实现对安全属性的机械化检查。

MAGS formalizes and freezes human-audited APIs and safety requirements, translates generated code into Dafny, repairs violations using verifier feedback, and compiles verified programs back into executable code. MAGS 对经人工审计的 API 和安全需求进行形式化并锁定，将生成的代码转换为 Dafny，利用验证器的反馈修复违规行为，并将验证后的程序编译回可执行代码。

We evaluate MAGS on 100 CUDA kernels, 100 terminal scripts, and 20 robotic-arm tasks. Across all 220 examples, it achieves a 100% success rate in producing programs with non-trivial safety guarantees against frozen specifications. Independent safety and functional evaluations further show strong performance across all three domains, while revealing failures when the auto-formalized semantics do not fully capture the target behavior. 我们在 100 个 CUDA 内核、100 个终端脚本和 20 个机械臂任务上对 MAGS 进行了评估。在全部 220 个示例中，它在针对锁定规范生成具有非平凡安全保证的程序方面实现了 100% 的成功率。独立的安全性与功能性评估进一步显示了其在上述三个领域中的强劲表现，同时也揭示了当自动形式化的语义无法完全捕捉目标行为时所产生的失效情况。