Nada Amin

Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs

Gabriel Poesia, Simon Henniger, Tzu-Han Hsu, Yilun Du, Nada Amin

The cost of producing code is rapidly diminishing with increasingly capable AI agents, while quality assurance of generated programs has not kept pace. Formal verification provides the strongest possible guarantees, but the ability of AI models to work with verification-aware lan…Read more