5 citations · 8 across the 4 of their papers we have counts for
5 papers
claimcheck: Measuring and Improving Specification Faithfulness
Martin Amster, One An, Holly Baker +3
Formal verification proves that a program satisfies its specification, but says nothing about whether the specification captures what the author meant. As LLMs increasingly write b…
Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler
Simon Henniger, Stephen Chong, Nada Amin
Programmers write formal specifications, and LLMs implement them, proving that each implementation matches its spec. Taken to its extreme, this makes specification languages the ne…
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…
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…
DafnyBench: A Benchmark for Formal Software Verification
Chloe Loughridge, Qinyi Sun, Seth Ahrenbach +7
We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such a…