DigiNews

Summary

This article surveys the PICK workflow, a human-in-the-loop approach to using large language models for generating and validating formal specifications across domains like regular expressions, linear temporal logic, and ABAC. It argues that relying solely on models can misrepresent user intent, and that concrete, user-classified evidence (witness strings) helps ensure correct and maintainable specifications, with broader implications for AI-assisted software design and verification.