MAGS tests formal safety checks for code written by agents

MAGS puts formal verification between AI-generated code and an executable program. The authors describe the multi-agent framework in an arXiv preprint submitted on 16 September; it has not been peer reviewed.

The process starts with human-audited interfaces and safety requirements, which are then fixed. Generated code is translated into Dafny, a language designed to support verification. Feedback from the verifier guides repairs before verified programs are compiled back into executable code.

A proof is only as useful as its specification

The authors tested 100 CUDA kernels, 100 terminal scripts and 20 robotic-arm tasks. They report that all 220 examples produced programs with non-trivial safety guarantees against the fixed specifications.

That result is narrower than saying every program behaved correctly. Separate safety and functional evaluations found failures when the automatically formalised description did not fully capture the intended behaviour.

For developers, the useful distinction is between checking a program against explicit rules and checking whether those rules describe the real task. MAGS automates parts of the proof process, but its design still depends on human scrutiny of the requirements being proved.