Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification

Xu Xu, Xin Li, Xingwei Qu +2

We introduce DafnyCOMP, a benchmark for evaluating large language models (LLMs) on compositional specification generation in Dafny. Unlike prior benchmarks that focus on single-fun…