Researchers have developed a multi-agent workflow that translates safety requirements for generated software into properties a formal verifier can check. MAGS uses Dafny, a programming and proof language, as an intermediate representation between AI-written code and the final executable program.
Human-reviewed interfaces and safety requirements are fixed first. Agents then translate a proposed implementation into Dafny, submit it to the verifier and use the resulting errors to repair violations. Only code that satisfies the specified properties is compiled back into an executable form. Unlike fuzz testing or an AI reviewer, formal verification can cover all executions represented by the mathematical specification rather than a sample of test cases.
The researchers evaluated MAGS on 100 CUDA kernels, 100 terminal scripts and 20 robotic-arm tasks. They report that all 220 examples produced programs with nontrivial, machine-checkable safety guarantees. That does not prove the programs are safe in every real-world sense: a verifier guarantees only the properties encoded in the specification, and mistakes or omissions in those requirements remain possible. Performance on a bounded benchmark also may not transfer to large production systems. The result nevertheless suggests a practical role for AI agents in reducing the manual proof engineering that has kept formal methods out of many ordinary development workflows.