Barista turns Javadoc into compile-time typestate checks
At the 41st IEEE/ACM Automated Software Engineering conference in Munich, researchers presented Barista a system that extracts protocol rules from Java documentation and converts them into LiquidJava specifications. The goal is to let the compiler catch protocol violations such as using a closed socket or sending data without connecting first.
Rules hiding in plain sight
Java classes carry implicit rules in their Javadoc comments. The java.net.Socket class documents seven states in prose: unconnected, bound, connected, inputshutdown, outputshutdown, bothshutdown and closed. Programmers are expected to follow these transitions — connect before sending, never reuse a closed stream — but these rules rarely appear in formal specifications. Barista reads the documentation and writes the annotations that let LiquidJava enforce them.
From prose to state machine
The paper's running example uses java.net.Socket. Barista models the seven states as a state machine and generates the LiquidJava annotations that represent valid transitions. Annotated interfaces describe which calls are allowed from each state. For instance, bind can only be called in the unconnected state, and connect moves from unconnected or bound to connected. Calls that violate the protocol become compile-time errors.
Agentic workflow builds the specification
Figure 1 of the paper shows the agentic workflow. Each step is an agent with a tool that checks its output, and the agent loops on that feedback until the check passes. The system is built with Claude Code and the Claude Agent SDK using Sonnet 4.6. The checks are MCP tools, and typestate and LiquidJava guides are provided as skills. This iterative process ensures the generated specifications pass expert validation.
Evaluation against expert specifications
Barista was compared against specifications written by two experts for 29 JDK classes. Every run was checked against expert test suites totaling 3,262 test files. Precision measures how often a flagged violation is real: 87% of the time. Recall measures how many expert violations are caught: about two thirds. When the system errs, it errs on the permissive side.
Speed and cost
Generating a specification takes 7.3 minutes and costs $2.20 per class. Writing one by hand takes about 31 minutes. This makes Barista substantially faster for teams that need to cover many classes.
What each component contributes
An ablation study compares three variants. The baseline uses documentation alone. Adding a state machine step improves precision. The full Barista pipeline includes tests and achieves the best results.
| Variant | Precision | Recall | F1 |
|--------------|-----------|--------|------|
| Baseline | 69.1% | 50.7% | 58.5%|
| State machine only | 85.2% | 47.3% | 60.9%|
| Barista (full) | 87.0% | 68.3% | 76.5%|
Where quality still drops
F1 score decreases as protocols become more complex. Simple protocols score 88% F1, moderate ones 72%, and complex ones 54%. When researchers traced each divergence from the expert specification, most turned out to be modeling gaps in the pipeline rather than missing information. The most common gap — 78% of cases — is transitions that depend on an argument's value, which a plain state machine cannot express.
Information and modeling gaps
The remaining 22% of divergences come from information gaps. These are cases where the Javadoc does not contain enough detail for the agent to reconstruct the full protocol. The benchmark uses 35 JDK 17 classes drawn from Beckman et al.'s study of object protocols in Java. Those classes range from 5 to 89 public methods. Expert specifications, tests and annotation guidelines are in the replication package, and each class links to its Javadoc.
Usability assessment
Researchers rated one run per class and asked whether a developer could start from the generated specification. The answer was yes, but the quality of that starting point varies with protocol complexity.
Barista demonstrates that LLMs can synthesize useful typestate specifications from natural-language documentation. While complex protocols still challenge the system, the baseline already captures a significant portion of implicit rules, and the full pipeline brings precision and recall to levels that make compiler-enforced protocol checking practical for many real-world Java classes.