MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs
MAGS uses multi-agent auto-formalization with Dafny to generate code with machine-checked safety guarantees, achieving 100% success across 220 tasks.
MAGS is a unified multi-agent framework that formalizes and freezes human-audited APIs and safety requirements, translates generated code into Dafny as a verification-aware intermediate representation, repairs violations using verifier feedback, and compiles verified programs back into executable code. Across 220 examples, including 100 CUDA kernels, 100 terminal scripts, and 20 robotic-arm tasks, it achieved a 100% success rate producing programs with non-trivial formal safety guarantees. Independent safety and functional evaluations showed strong performance, while revealing failures when auto-formalized semantics do not fully capture the target behavior.
- Multi-agent pipeline freezes human-audited APIs and safety requirements before code generation.
- Uses Dafny as verification-aware intermediate representation with mechanically checked safety properties.
- 100% success across 220 examples: 100 CUDA kernels, 100 terminal scripts, 20 robotic-arm tasks.
- Verifier feedback repairs violations; verified programs compile back into executable code.
Full article183 words · extracted from arxiv.org · click to collapse
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. 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 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. 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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.19391