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

arXiv: https://arxiv.org/abs/2609.19391 · HTML: https://mlsanity.com/paper/2609.19391/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 11 of its 25 references that are in the map.
- First posted on arXiv 16 Sep 2026.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)

## Builds on (most cited first, 11 of 11)

- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Large Language Models Cannot Self-Correct Reasoning Yet](https://mlsanity.com/paper/2310.01798/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [VLABench: A Large-Scale Benchmark for Language-Conditioned Robotics Manipulation with Long-Horizon Reasoning Tasks](https://mlsanity.com/paper/2412.18194/) (2024)
- [A Large-Scale Survey on the Usability of AI Programming Assistants: Successes and Challenges](https://mlsanity.com/paper/2303.17125/) (2023)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation](https://mlsanity.com/paper/2510.05156/) (2025)
- [BaxBench: Can LLMs Generate Correct and Secure Backends?](https://mlsanity.com/paper/2502.11844/) (2025)
- [Densing Law of LLMs](https://mlsanity.com/paper/2412.04315/) (2024)
- [ProofWright: Towards Agentic Formal Verification of CUDA](https://mlsanity.com/paper/2511.12294/) (2025)

## Abstract (arXiv)

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.