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

arXiv:2609.19391v1 Announce Type: new Abstract: 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.

MAGS provides machine-checkable guarantees for safety properties, reducing risk of failures.

The MAGS system provides a reliable, automated method for generating software with formal safety guarantees, addressing risks of undetected failures in complex AI-generated programs. This enhances software safety and security, benefitting human users and society by reducing potential harm from faulty AI-coded systems. Limitations remain where semantics are incomplete.

This is a genuine technical safety advance for AI-generated code, addressing a real and growing risk as coding agents scale beyond human review capacity. The implication is modestly positive but bounded by the paper's own caveat that formalized specs can miss intended behavior, and it is an unreviewed preprint tested on limited benchmarks.

The framework successfully generates complex programs with formal safety guarantees, achieving a 100% success rate on 220 examples. This capability significantly mitigates safety and security risks associated with autonomous AI code generation, improving reliability in critical applications. The limitation to frozen specifications and occasional semantic capture failures are noted but do not negate the core safety benefit.

SOURCE     arXiv cs.AI (tier 1)
   ↓
DOCUMENT   aac933c0-44ea-456e-9955-a9d7e7e2b498
           https://arxiv.org/abs/2609.19391
   ↓
EVIDENCE   2 extracted excerpts
   ↓
MODEL RUN  4 runs, methodology 1.0.1
   ↓
SCORE      -21  (Adverse)
   ↓
CONFIDENCE 78%