MAGS: Machine-checked guarantees on specified safety properties in AI code (arxiv.org)

A new framework named MAGS, or Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs, has been introduced to address the safety and security challenges posed by the rapidly growing complexity of programs generated by large language model (LLM) coding agents. With traditional methods like fuzz testing and static analysis often failing to cover all possible edge cases, MAGS offers a solution by providing machine-checkable safety guarantees through formal verification. This framework employs Dafny, a verification-aware intermediate representation, allowing for the formal specification, verification, and execution of generated code while providing immediate feedback on safety violations. The significance of MAGS lies in its ability to automate the rigorous process of formal verification, previously hampered by extensive manual work. In evaluations involving 220 programs across diverse domains—including CUDA kernels and robotic-arm tasks—MAGS achieved a perfect success rate in ensuring safety properties, underscoring its potential to enhance the integrity of AI-generated software. Additionally, independent safety assessments revealed both strong performance and the potential for failures when semantics did not fully encapsulate intended behavior, indicating areas for further refinement while establishing a robust foundation for safer AI outputs.