Identifying What the Solver Needs: LLMs and the Missing Proof Hints in SMT Verification

SMT-based verifiers such as Dafny and Verus require programmers to provide proof annotations that the solver cannot derive on its own. Many of these annotations encode non-trivial proof steps, such as complex loop invariants or inductive arguments. Others appear redundant: ad-hoc assertions that follow from the surrounding context and yet cannot be removed. We investigate what kind of proof gaps these assertions fill, and study their impact on LLM-based verification. We present a mechanism-level study of assertions. Across four corpora of machine and human annotated programs in Dafny and Verus, we identify every assertion whose removal breaks verification and classify them by finding a minimal intervention that restores the proof. We find 320 such essential assertions in Dafny and 462 in Verus. Two mechanisms dominate the types of gaps they fill: \emph{axiomatization gaps}, where the SMT-LIB encoding leaves a needed identity unstated, and \emph{instantiation gaps}, where a quantified fact is available but never triggered. We evaluate four open-weight LLMs on the task of recovering these assertions. Without knowing where the missing assertion belongs, no model repairs more than 10\% of Dafny tasks and one reaches 23\% on Verus. Given the missing assertion location, the three larger models repair 32--52\%. The results suggest that models recognize syntactic patterns of assertions from training data but do not reconstruct the internal verifier reasoning that would identify the missing hint. Our work leaves as an open question how to better integrate SMT solver capabilities into LLM-based verification pipelines.