This week, we are presenting the Barista paper at ASE'2026, and by 'we', I mean Catarina Gamboa, who is leading this work.
When trying to adopt LiquidJava, 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, Frama-C's ACML and Java Modeling Language.
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.
@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.