Quint and Verifying AI Generated Code

Gabriela Moreira started her bachelor's in computer science more than ten years ago, and at the time she was buried in compiler work, programming languages, and type systems. Then someone showed her TLA+, a formal specification language, and her reaction split in two directions at once. She could see it solving real problems in the distributed systems and databases she handled at her industry job, but she could not picture a single teammate ever agreeing to touch it.

"Oh, this thing would be super useful in my job, but also, the syntax is so mathematical and so scary, I doubt anyone on my team would like to use this."

That gap, between a tool she loved and a syntax nobody else wanted, is most of the reason Quint exists.

From Compilers to Formal Methods

Moreira fell for formal methods on the spot, then went looking for a way to make them less painful to adopt. She did a master's focused on tooling around formal verification, and she taught formal methods at university for a year and a half.

Her path crossed Quint's at the TLA+ conference, where she met Informal Systems, the group building the Cosmos blockchain and doing heavy work in TLA+. They were already building the same kind of tooling she was. She joined, and Quint started there. As she put it, her origin story has a lot of intersection with Quint's origin story.

When she explains formal methods to people who have never heard the term, she starts somewhere familiar: type checking. Running a compiler against type definitions and watching it complain about a mismatch is already formal verification, since it checks correctness properties. From there the field branches into proof assistants like Lean, Rocq (formerly Coq), and Isabelle, where a property is proven to hold for every possible case, and into the lighter-weight world of model checking, where the computer does the proving. Quint and TLA+ both sit in that second camp. An engineer builds a model as a state machine, with an initial state and a set of transitions, states a property, and the tool either confirms it holds in all cases or hands back a counter-example, an exact sequence of states that produces the bug.

Why Web3 Is the Best Use Case

Moreira is precise about why blockchain turned out to be fertile ground for formal verification, and she lays it out in three parts. The first is that shipped code is hard to patch. She compares it to software written for a rocket or an airplane, where mistakes cannot be fixed once the thing is in the air. The second is incentive: when money sits directly inside the contract, an exploit pays out instantly, which widens the gap between attacker and defender and forces more effort into making code correct. The third is simply where the work was. When she was starting out, the advice from research groups was blunt: if the goal was to do formal methods in industry, the path led to blockchain, or to one of the rare jobs at NASA or an aerospace company.

She is candid that she came in knowing almost nothing about blockchain, and says she still does not know a lot, though events have given her more context since.

What AI Cannot Decide Is Correct

The sharpest part of the conversation is Moreira's view of where AI stops being useful. She grants that AI can produce code that does not crash, code without null pointer exceptions, code without certain authorization holes. Other tools already check for crashes, underflows, and overflows, and she points to those as important. But behavior is a different problem.

"But how much can actually AI know what correct means for your application?"

Her answer is that it cannot, because correctness is a judgment call that belongs to the people building the product. The person who decides a user should be allowed to do one thing and forbidden from another is the engineer, sometimes the business person beside the engineer, not the model. Quint's role, she says, is to surface those decisions and pin them down. It is not going to make code correct on its own, even with AI in the loop. Instead it asks what behavior is actually desired, records the answer, and then checks the application against it. The specifications are formal, but Moreira keeps stressing that they are also executable. A developer can press run on a spec, watch one path play out, and notice when something happened that should not have.

For developers who already write unit and integration tests, she frames Quint as a complement rather than a replacement. There is an open source library called quint-connect that links a spec to real code and generates test scenarios, including very specific ones, like a path where two users hold the same item in their cart at checkout. She also sees a role at code review, against what she calls cognitive debt or comprehension debt, the problem of reviewing code nobody on the team wrote. If no one on the team really wrote the code in the ordinary sense, who is supposed to understand it well enough to approve it? Her stance there is direct: reading code is not a permanent solution, because human brains are not wired to read code well, so something more abstract and executable is more tangible to reason about. The third entry point, and the one she calls the holy grail, is design, writing the spec before the code, the same argument Leslie Lamport made when he asked why anyone would construct a building without drawing a blueprint first.

Spinning Out and Building Quint Studio

In April, Quint spun out of Informal Systems into its own company, and Moreira ties that move directly to AI. Language models turned out to be good at writing specs, including translating from a language like Rust into Quint, which lowers the cost of getting started and widens the audience Quint Co. can reach. There is also a repository called quint-llm-kit with commands and examples, and official skills for tools like Claude Code are being polished for release soon.

The larger bet is a product called Quint Studio, described as a command center for everything behavior-oriented, currently behind a waitlist with betas planned. Moreira's motivation for all of it is plain:

"My life's goal is just to get this in the hands of like more software engineers, making sure that we can trust software more."