MAGS Uses Multi-Agent Formalization to Guarantee Safety for Agentic Code

Summary

LLM coding agents can generate programs at a scale that makes complete human review difficult, while fuzzing, static analysis, and LLM-based verification may miss edge cases. The paper introduces MAGS, a multi-agent framework for producing executable programs with machine-checkable safety guarantees. It freezes human-audited APIs and safety requirements, translates generated code into Dafny, uses verifier feedback to repair violations, and compiles verified code back to executable form. MAGS was evaluated on 100 CUDA kernels, 100 terminal scripts, and 20 robotic-arm tasks. It succeeded on all 220 examples under the frozen specifications, with independent safety and functional evaluations also showing strong results across the three domains. The authors nevertheless report failures when the auto-formalized semantics do not fully represent the intended target behavior, so the guarantees depend on the adequacy of the specifications.