- Author
- Yueyang Feng and Ilya Sergey
- Published
- 18 May 2026
- Kind
- Research blog post, with benchmark results
- Original
- proofsandintuitions.net/2026/05/18/property-based-testing-specifications/
- Subject
- Checkable specs for coding agents
- Themes
- Checking the work
What it is
Feng and Sergey ask how to tell whether a formal specification is right. They split the question into three checks that random testing can refute. The post works in Lean, using its Plausible testing library.
What it says
- Admissibility asks whether the spec claims to handle the test input.
- Soundness asks whether the spec accepts the intended output.
- Uniqueness asks whether the spec rejects every other output.
- Mutating the intended output beats random sampling, because bad outputs tend to resemble good ones.
- Output variables should always have constrained domains, as one example bug shows.
What evidence it gives
Across 188 VERINA and 104 CLEVER problems, the method flagged 13 and 18 underspecified specs. That is about 10% of those tested. The authors say both benchmark teams acknowledged the findings.
Interests and limits
Testing can refute a spec but cannot prove it right. Only 104 CLEVER specs converted cleanly, so the rest went untested. The benchmarks cover Lean programs, so the 10% may not carry to other settings. This page draws on the post's method and main results.
Connections
These links are this wiki's own reading, not claims the sources make.
- The components of agent memory. A wrong spec and a wrong note fail alike, because later work trusts them. Feng and Sergey test specs with counterexamples. Martin tests notes against transcripts. Each checks the layer everything else relies on.