POSTCONDBENCH: Benchmarking Correctness and Completeness in Formal Postcondition Inference

Formal postconditions are precise specifications that characterize program behavior and are essential for debugging, testing, and verification. However, writing them manually requires significant expertise. Recent work has turned to large language models (LLMs) to automatically generate postconditions from code and natural-language artifacts. But evaluating these generated postconditions has been a bottleneck—existing benchmarks focus heavily on correctness and rely on surface-form matching or small synthetic datasets.

To address this, researchers from academia introduced POSTCONDBENCH, a benchmark of 420 real-world Python and Java tasks from 121 open-source projects. Each task includes expert-constructed ground-truth postcondition sets. The benchmark provides a runnable execution environment and operationalizes completeness through defect discrimination: a postcondition set is more complete if it's violated by more defective implementations while remaining satisfied on correct runs. Testing five state-of-the-art LLMs revealed a significant gap between correctness and completeness, with repository-level dependencies and method complexity widening that gap. The work highlights the challenge of generating truly robust and useful formal specifications.