Agentic AI
New Framework Uses Multi-Agent AI to Guarantee Safety in Code Generated by AI Agents
Researchers introduce MAGS, a system that combines code generation with formal verification to produce programs with machine-checkable safety guarantees.
As LLM coding agents now produce increasingly complex software at scale, the challenge of verifying their output for safety and security has become acute. Traditional review approaches—including fuzz testing, static analysis, and using language models as validators—can catch many bugs but typically fail to cover all edge cases comprehensively.
The Verification Problem#
Large-language-model-powered programming agents create code faster than humans can realistically review it, creating new risks around correctness and security. Existing detection methods have inherent blind spots, particularly when handling unexpected inputs or rare conditions. Formal verification offers a theoretically sound alternative, providing mathematically proven guarantees that code meets specified safety properties, but it has historically required substantial manual effort to specify requirements and construct proofs.
Introducing MAGS#
Researchers have proposed MAGS (Multi-agent Auto-formalization Guarantees Safety), a unified framework that automates the formal verification process for agent-generated code. The system works by formalizing human-audited APIs and safety requirements, then translating generated programs into Dafny—a verification-aware programming language where safety properties can be mechanically validated. When the initial translation fails verification, MAGS uses feedback from the verifier to repair violations and eventually compiles the verified program back into executable code.
Evaluation Results#
The team tested MAGS across three distinct domains:
- 100 CUDA kernels (GPU code)
- 100 terminal scripts (command-line utilities)
- 20 robotic-arm tasks (control systems)
Across all 220 examples, MAGS achieved a 100% success rate in generating programs that carry non-trivial safety guarantees against the frozen specifications. Independent assessments of both safety compliance and functional correctness showed strong performance across all three domains, though the evaluation also identified cases where the auto-formalized semantics did not fully capture the intended behavior of the target system.
