2 papers
cs.AI2026
Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs
Gabriel Poesia, Simon Henniger, Tzu-Han Hsu +2
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…
cs.SE2024
dafny-annotator: AI-Assisted Verification of Dafny Programs
Gabriel Poesia, Chloe Loughridge, Nada Amin
Formal verification has the potential to drastically reduce software bugs, but its high additional cost has hindered large-scale adoption. While Dafny presents a promise to signifi…