Compositional Annotation Synthesis for Program Verification with LLMs

Formal verification can establish that LLM-generated code satisfies its specification, but constructing proof annotations remains costly. With interacting functions, locally provable annotations may fail to compose: a callee's guarantee may omit facts its callers need, or a generated requirement may exceed what its callers establish. Verifier feedback identifies failures but does not by itself determine how dependent annotations should change together. We present CoVeri, which combines bottom-up symbolic reasoning over implementations and current summaries with top-down analysis that traces failed obligations to candidate interfaces. These analyses guide the LLM to strengthen guarantees, relax generated requirements, and jointly revise dependent contracts while preserving fixed specifications. Across three LLM backbones, CoVeri outperforms all evaluated baselines on DafnyComp, VeriEquivBench, and SWE-Dafny. On DafnyComp, it matches the strongest baseline while using a smaller backbone. Ablations support the complementary benefits of bidirectional guidance and joint revision.