Paper: Barista - Synthesizing Typestate Specifications with LLM Agents

Catarina Gamboa is presenting the Barista paper at ASE 2026, describing an LLM-agent workflow that reads English library documentation to synthesize typestate specifications for Java libraries, including the Java Standard Library. The workflow translates documentation into automata, derives positive and negative method-call sequences from those automata, and iterates on the generated specifications until they validate, targeting the annotation burden faced by tools such as LiquidJava, LiquidHaskell, Frama-C's ACSL and the Java Modeling Language. The paper's co-author writes that LLM advances since the work began mean a skill- or tool-based architecture would likely outperform the original DFA-oriented multi-agent design, and argues the results should be treated as a pre-print or living benchmark.

This week, we are presenting the Barista paper at ASE'2026 https://conf.researchr.org/details/ase-2026/ase-2026-research-track/97/Barista-Synthesizing-Typestate-Specifications-with-LLM-Agents , and by 'we', I mean Catarina Gamboa https://catarinagamboa.github.io , who is leading this work. When trying to adopt LiquidJava https://liquid-java.github.io , an annotation-based language that adds refinements to types, in your Java project, you will have to write the annotations for any library that you use, including the Java Standard Library. This is just a huge amount of work for your simple application. This issue is shared by LiquidHaskell https://ucsd-progsys.github.io/liquidhaskell/ , Frama-C's ACML https://frama-c.com/html/acsl.html and Java Modeling Language https://www.eecs.ucf.edu/~leavens/JML/ . Roughly one year ago, we wanted to explore if we could have LLMs read the documentation English and write the specifications for libraries. We focused on a few examples from the Java Standard Library and, given that one year ago LLMs generated more slop than they do today, we came up with an agentic workflow that combined LLM to translate English to an Automata, and the Automata to specification. And by having the automata, we could create positive and negative examples of method call sequences that we could use to validate the generated specification and iterate until we are satisfied. If you want to learn more about how we come up with the refinements below, you can read the interactive presentation Catarina prepared https://catarinagamboa.github.io/papers/barista/ . @StateSet {"unconnected", "bound", "connected", "inputshutdown", "outputshutdown", "bothshutdown", "closed"} @RefinementAlias "ValidPort int p {p = 0 && p <= 65535}" @ExternalRefinementsFor "java.net.Socket" public interface SocketRefinements { @StateRefinement to = "unconnected this " public void Socket ; @StateRefinement to = "connected this " public void Socket InetAddress address, @Refinement "ValidPort " int port ; @StateRefinement from = "unconnected this ", to = "bound this " public void bind SocketAddress bindpoint ; ... } Presenting this work almost one year after it was conducted feels very strange to me. LLMs have advanced so much in the meantime, that I believe they would be able to get better results without the need for our DFA-oriented architecture. Or probably we would have done a skill-based or tool-based architecture instead of multi-agent. LLMs are now much better at orchestrating the whole process and managing their contextual memory than they were back when we started this. This paper along with most of the accepted papers in SE these two years should probably just be a pre-print, or a living benchmark. The results we present are a product of our time, that would be imperceptible for anyone who wasn't using LLMs to generate code last year, or for the rest of us that forget it easily. I still see value in our approach, though. I am more and more convinced that we need more verified programming, not to avoid bugs, but rather to gain trust in the source code. While before software engineers would gain trust by building it themselves, and eventually by testing it, both of these tasks are so automated that we need other ways of building trust in our systems. That is an open question that I would love to have a complete answer to. Right now, formal methods and dependently-typed languages are a partial answer to that problem. If you're in Münich, please go and see Catarina's talk on Thursday https://conf.researchr.org/details/ase-2026/ase-2026-research-track/97/Barista-Synthesizing-Typestate-Specifications-with-LLM-Agents .