MAGS Framework: Multi-Agent Auto-Formalization Provides Safety Guarantees for AI-Generated Code

When AI Writes Code Faster Than Humans Can Review It

Large language model (LLM) programming agents can now generate complex programs at a staggering scale — and this creates an increasingly thorny problem: human reviewers simply cannot keep pace with code generation. When the volume of AI-generated programs grows too large for thorough manual inspection, the risk of safety and security vulnerabilities rises accordingly.

The industry's go-to defenses — fuzz testing, static analysis, and LLM-as-a-Verifier approaches — can catch many defects, but they share a common weakness: they struggle to cover all possible edge cases. That means some potential failure scenarios will always slip through the cracks.

Formal Verification's Old Problem and MAGS's New Approach

Formal verification could, in principle, solve this coverage problem — it provides machine-checkable guarantees against specified properties. The catch is that traditional formal verification carries a steep entry cost: it demands extensive manual specification writing and proof engineering, making large-scale adoption impractical.

The MAGS (Multi-agent Auto-formalization Guarantees Safety) framework, proposed in a paper on arXiv, attempts to combine the rigor of formal verification with the automation capabilities of LLM agents. It is a unified multi-agent framework designed to generate executable programs that simultaneously carry formal safety guarantees.

Dafny as a Verification-Aware Intermediate Representation

The centerpiece of MAGS's design is using Dafny as a "verification-aware intermediate representation." Dafny is a programming language with built-in formal verification capabilities, where safety properties can be mechanically checked. This choice gives the entire pipeline a reliable verification anchor.

The workflow breaks down into several key stages:

• Freezing human-audited specifications: MAGS formalizes and "freezes" human-audited APIs and safety requirements as immutable verification baselines.
• Translation to Dafny: LLM-generated code is translated into a Dafny representation.
• Feedback-driven repair: Feedback from the verifier is used to automatically fix any parts that violate safety properties.
• Compilation back to executable code: Programs that pass verification are compiled back into executable form.

This closed loop of "freeze specs → translate → repair → compile" essentially encodes human safety intent into a fixed constraint framework, then lets agents automatically handle verification and repair within that framework.

---

The core idea behind formal verification is to use mathematical methods to prove that a program satisfies a given specification — not merely "no issues found after testing a few inputs." Typical approaches include Model Checking, Theorem Proving, and program logics such as Hoare Logic. Unlike testing, formal verification provides complete guarantees covering all possible execution paths, which is why it is widely used in safety-critical domains such as aviation, chip design, and cryptographic protocols. However, the practical barrier is extremely high: engineers must manually write specifications in formal languages (such as TLA+, Coq, or Isabelle) and handle numerous auxiliary lemmas during the proof process — an effort that often takes several times longer than writing the program being verified. This is precisely the bottleneck MAGS aims to break through with multi-agent automation: delegating the tedious work of specification writing and proof repair to LLM agents, while concentrating the human judgment needed for safety intent into a one-time "frozen specification" review step.

Dafny, developed by Microsoft Research, is one of the few practical languages that deeply integrates program logic specifications with code syntax. Developers can write preconditions (requires), postconditions (ensures), and loop invariants (invariant) directly alongside function signatures. Dafny's built-in SMT solver (based on Z3) automatically attempts to prove these assertions at compile time. A successful proof means the code mathematically satisfies the specified properties — not merely that it passes test cases. The advantage of choosing Dafny as an intermediate representation is that it has sufficient expressive power to describe complex safety properties while offering automated machine-checking without requiring manually constructed proof scripts. For a pipeline like MAGS that requires frequent "generate → verify → repair" iteration, Dafny's immediate feedback mechanism (pointing to the specific assertion that failed) also gives LLMs actionable location information for automated repair.

---

Experimental Validation Across Three Domains

The research team evaluated MAGS on three substantially different task types: 100 CUDA kernels (GPU parallel computing), 100 terminal scripts, and 20 robotic-arm tasks — 220 samples in total.

The results are impressive: across all 220 samples, MAGS achieved a 100% success rate in generating programs with non-trivial safety guarantees against the frozen specifications. The word "non-trivial" is key here — it means these safety guarantees are not empty formalities but carry real, meaningful constraints.

Independent evaluations of safety and functionality further demonstrated strong performance across all three domains. This cross-domain consistency suggests the framework's methodology has genuine generalizability, rather than being fine-tuned for a single scenario.

Limitations Honestly Presented

To the authors' credit, the work does not shy away from its own boundaries. The evaluation also reveals a class of failure modes: failures occur when the auto-formalized semantics fail to fully capture the intended behavior.

In other words, MAGS can guarantee that "the program satisfies the formalized specification" — but if the formalization process itself does not accurately express what humans actually want, then the guarantee is aimed at the wrong target. This is actually a fundamental philosophical problem in formal verification: specification correctness. Verification can only guarantee what you verify, not that what you verify is what you truly want.

This is a particularly important reminder for teams looking to deploy safety solutions for AI-generated code: auto-formalization reduces the manual burden, but also conceals the critical responsibility of "is the specification accurate" even more deeply.

---

The specification correctness problem has a classic formulation in the formal verification community, often called the "what to verify" challenge — equally important as "how to verify." History offers cautionary lessons: the floating-point division bug in Intel's Pentium chip passed formal verification at the time precisely because the specification itself omitted certain boundary conditions. In the MAGS context, auto-formalization converts natural language or semi-structured requirements into Dafny assertions, and this conversion process can itself introduce semantic drift — the gap between an LLM's interpretation of a requirement and the human's true intent is not always obvious. Therefore, although MAGS achieves a 100% specification satisfaction rate across 220 samples, assessing the system's true safety requires additional scrutiny of whether the auto-formalized specifications themselves are accurate. This points to a future research direction: providing more readable back-explanations of auto-formalized specifications so that human reviewers can verify "what is actually being verified" at lower cost.

---

Implications for the AI Agent Safety Ecosystem

MAGS represents a promising technical direction: as LLM programming agents become increasingly widespread, using formal methods to add a mechanically checkable safety guardrail to their outputs is a compelling proposition. Compared to best-effort approaches like fuzz testing and LLM-based verifiers, formal guarantees offer commitments at the level of certainty.

As AI agents are used to generate increasingly critical system code — from GPU kernels to robotic control systems — an architecture that encodes human-audited specifications as fixed constraints and then automates the verification loop through multi-agent collaboration could become an indispensable part of future AI-assisted development toolchains. Of course, scaling this approach to more complex, real-world engineering scenarios will require further validation.