Barista: Synthesizing Typestate Specifications with LLM Agents

Abstract

Object-oriented classes encode implicit protocols that clients must follow, such as connecting a socket before sending data or opening a stream before reading. Mainstream programming languages like Java cannot validate the correct use of these protocols, but more advanced type systems, such as typestate systems, can detect these violations at compile time. However, these systems require a formalization of these implicit protocols. To overcome this limitation, we propose to extract object protocols from documentation using a combination of LLMs and test generation. We developed Barista, an agentic workflow that transforms class documentation into verifiable LiquidJava specifications through DFA-guided protocol extraction, test synthesis, and verification-driven refinement. We evaluated our approach on 35 Java classes with expert-written ground truth, achieving 87.0% precision and 68.3% recall, with 75% of specifications usable directly or with minor edits. Barista bootstraps these specifications for well-documented libraries, reducing the manual annotation burden and enabling compile-time protocol safety without specialized expertise.