Coins: Evaluating LLM Formal Specifications by Instantiating Them on Trusted Test Cases Instead of Proving Equivalence

arXiv 2608.13077·medium signalXBlueskyLinkedInCopy link

Existing evaluations of LLM-generated formal specifications require verifying implementation conformance or proving semantic equivalence between specs — both formidably hard, and both conflate proof difficulty with specification quality. Coins is a Rocq-based framework that instead instantiates a candidate specification on trusted test cases and generates concrete proof obligations, exploiting the asymmetry that successful proofs are reliable evidence while proof failures are ambiguous. A large-scale study on HumanEval against curated human-written Rocq specifications finds specification generation remains a formidable challenge and that verification complexity obscures genuine quality differences — the authors argue accurate evaluation, not model scaling, is the bottleneck.