Laurel: Unblocking Automated Verification with Large Language Models

Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala +2

Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of as…