- Author
- Brown PLT blog
- Published
- 9 June 2026
- Kind
- Research group blog post, describing a tool and paper
- Original
- blog.brownplt.org/2026/06/09/pick.html
- Subject
- Checkable specs for coding agents
- Themes
- Taste and judgment, Saying it exactly
What it is
This post describes PICK, a tool for getting formal specifications from vague intent. A model proposes several candidates. PICK shows concrete cases where they disagree, and the user votes on each. Candidates that conflict with the votes drop out.
What it says
- Human checks must be meaningful and moderate, or people will simply confirm.
- Verification only informs when program and property are written independently.
- More models give faster agreement, not necessarily more redundancy, because they share training data.
- A date regex shows the idea: rejecting 13/01/2025 commits you to month-first dates.
- Ending with no survivors is useful, because it shows the model failed your intent.
- Better models will not make user intent more articulate, the authors argue.
What evidence it gives
The post says experiments show it works very well, and cites an ECOOP 2026 paper. It gives no numbers itself, and this page has not checked the paper. PICK exists for regular expressions, temporal logic and access control.
Interests and limits
The authors built the tool. It needs formal languages where the difference between candidates can be expressed and sampled. That excludes specs written as ordinary prose.
Connections
These links are this wiki's own reading, not claims the sources make.
- Harmony Explained on Hacker News. PICK assumes some truth lives only in the person asked. The harmony thread keeps arriving there too. So PICK's method might suit tuning. Generate candidates, find where they differ, and let ears vote.
- You can't unit test for taste. Tryggvason says a route's best stops have no ground truth to test against. PICK starts from that situation. It finds inputs that separate candidates, then asks a person. Tryggvason's per-route parameters might be tuned the same way.