Efficient Formally Verified Code Generation via Specification Quality Estimates

Large language models have become a ubiquitous element of software development workflows, but the code they generate may diverge from user intent or contain bugs. Formal verification has shown promise for addressing the correctness gap: instead of simply generating executable code, an LLM-based agent is tasked with producing a specification, an implementation, and a formal language proof of correctness. Generating the artifacts required for formal verification, though, is difficult: synthesized specifications are often incorrect, and generating implementations and proofs is computationally expensive. In this paper, we ask whether variation in specifications can be harnessed to improve agents' performance on verified code generation tasks. We first find that the downstream cost of implementation and proof generation can be accurately predicted given a specification as input. We then show that these cost estimates are useful: they can guide a verified code generation agent in selecting a specification that reduces the downstream cost of implementation and proof writing without diverging from user intent. We realize our approach as a tool, SPEQUEST, and find that it makes implementation and proof generation more than $3\times$ faster on a standard benchmark set.