Gabriela Moreira, CEO of Quint at Informal Systems – Interview Series

Gabriela Moreira, CEO of Quint at Informal Systems, is a research engineer specializing in programming languages and formal methods, with a strong focus on building tools that make complex system verification more accessible to engineers. She leads the development of Quint, a modern executable specification language based on TLA+, where she continues to maintain and evolve the language and its tooling. Her work spans formal verification, static analysis, and developer tooling, and she has also contributed to academia by teaching formal methods, reflecting a blend of practical engineering and theoretical depth.

Quint, developed and maintained at Informal Systems, is a modern specification language designed to model, test, and verify complex systems such as distributed networks, blockchains, and databases. Built on the foundations of the Temporal Logic of Actions (TLA), Quint introduces a more developer-friendly syntax, along with advanced tooling like type checking, simulation, and model checking, allowing engineers to detect system failures before deployment. The platform emphasizes executable specifications, enabling developers to not only describe system behavior but actively test and explore it, bridging the gap between theoretical correctness and real-world implementation.

Going back to the beginning, what first sparked your interest in programming, and how did you eventually find your way into formal methods and distributed systems?

I was an avid gamer with a bad computer, and I realized I enjoyed fixing the problems and making it work. I signed up for computer science and was drawn to theory and compilers. 

In 2015, I was presented with programming contests. In those, you usually get a few examples of input and expected output, and you write code that solves the problem and works for those examples. However, after you submit it for evaluation, the code is actually tested with many more examples beyond the ones they show you. That realization that code might work for the scenarios I see or think of, but still fail in cases I haven’t considered, made programming into a kind of challenge I fell in love with.

Working in the industry, I was quickly drawn to distributed systems, where we had to consider different orderings messages could arrive in, different failure modes, and a whole world of hidden behaviors. In 2018, a colleague introduced me to a formal specification language called TLA+. I was hooked. I immediately started building tools around TLA+ and have been working in this space ever since.

You have built your career around formal methods and programming languages, from your early work on tooling based on Temporal Logic of Actions (TLA+) to leading the development of Quint at Informal Systems. What motivated you to focus on making formal verification more accessible, and how has that vision shaped Quint’s design?

TLA+ is too good not to be used extensively in the industry. I was still quite junior when I learned about it, and I’d join these calls with my work colleagues to try to come up with solutions together, and I was constantly finding scenarios where our solutions would fail. However, I was always the last line of defense against those scenarios in most cases. I figured there had to be a better, less costly, more valuable way to solve these scenarios. Thus, the idea of using formal methods to create specs before implementing code was created. So I started my academic journey towards it, which led me to Informal Systems and Quint.

Quint was not originally conceived as a product. We built it out of necessity at Informal Systems. We were writing TLA+ specifications for systems we needed to trust more than we did, but that didn’t expand beyond a very small group of people as the syntax was too scary with too many math symbols, and the tooling didn’t meet people’s basic expectations. We’d show colleagues and external collaborators: “look at this amazing thing I did”, but they couldn’t read it, and didn’t have time to learn a new tool.

The design choices in Quint follow directly from that experience. The language is easy to read and remember. The first thing we built was a VSCode extension that highlights errors as you type. It has types and distinct modes to separate layers explicitly. It has a REPL so you can explore interactively, and a simulator so you can get quick feedback and iterate. It exports traces to a standardized JSON format that is easy for machines to parse. These were things programmers already expect from their tools and that we needed ourselves. The verification underneath is the same logic as TLA+.

I’m obsessed with making formal methods more accessible, and shipping tools is exciting, but the real impact is only felt if engineering teams actually use them. There’s still a delta between what the tools can do and how useful they feel to developers, and I’m working to close that gap.

For readers unfamiliar with it, how would you explain what Quint is and why a new specification language was needed alongside existing tools like TLA+?

Most specifications are documentation. You write down what the system should do, and you check them by reading them. The problem is that documentation is wrong in ways you cannot mechanically detect: undefined names, ambiguous behavior, implicit assumptions. You usually find out during implementation, or in production.

A Quint spec is something you execute. You model the system as a state machine, define the properties it should satisfy, and run or verify the model. If there is a violation, you get a counterexample showing exactly the sequence of steps that triggers it. That changes when and how cheaply you catch a design flaw.

TLA+ could always do this. Quint makes it practical for engineers who are not already specialists in temporal logic.

Quint is designed to bridge the gap between formal methods and everyday software engineering. What were the biggest usability barriers you aimed to eliminate compared to traditional approaches?

Honestly, the biggest usability barrier was the syntax. That’s why we started with the syntax. After addressing that, we could focus more on other factors. Quint’s type and effect system came to flag as many errors as possible before even starting the regular verification process, and people valued that a lot. It led us to write more high-quality specifications that even more people could read. We integrated it all in editors, and offered the basic functionality all developers have the right to expect.

The biggest impact after that was our simulator. It started as just a way to offer people first feedback on the behavior of their system, as a developer wants to be able to, somehow, run the code after they write it. It then turned out to be extremely valuable as a way to get confidence on specifications that are too big for verification to handle, since the expertise of adapting a specification to make it feasible for verification should not be taken for granted. Our simulator made confidence more accessible and we have been using it extensively in many projects.

My biggest pain point with TLA+ syntax was how frequently I mixed my backslashes and regular slashes, and you need to type those a lot. I like Quint’s syntax much better, but what really makes it impossible to go back for me is all the tooling.

One of Quint’s strengths is its ability to model and test distributed systems before deployment. How does this change the way engineers should think about building systems like blockchains or real time infrastructure?

The biggest shift is moving validation earlier. Leslie Lamport, creator of TLA+, compares writing specs before code to drawing blueprints before construction work. Even if you already built something without a blueprint, it is still a good idea to write one now and use it to inform your further changes.

In the software industry, we use markdown files and whiteboards. Maybe you can compare that to try to textually describe a building. It works, but would you know if the wall sizes add up? Quint offers a way to describe systems where you can be as high-level as you want, and get insights about its behavior and correctness.

Quint builds on the foundations of TLA+, which is widely used to describe distributed systems. How did you balance maintaining that theoretical rigor while making the language more developer friendly?

The key decision was to restrict Quint to a fragment of TLA (the logic behind TLA+) rather than expose everything the logic allows. TLA is very expressive, and some of that expressiveness includes operators that are not supported by any tools, and allows combinations that people understand and use wrongly, making things really hard to debug. We made a deliberate choice: stick with what most realistic specs actually need, and avoid what has potential for confusion.

The type system and effect system add constraints, but constraints that are useful. They prevent a whole class of spec errors that are not fun when found after the verification is already running. Types are almost entirely inferred and effects are hidden from the users, so this adds value with no friction.

Before I learned about TLA+’s existence, I was doing research work in type systems, which means that Quint’s type checker was probably my favorite component to write. I remember drinking a Paçoca-flavored coffee in my first few months at Informal while reviewing some type system paper and thinking “my life is amazing”. 

Making the language good to use while still keeping correspondence with TLA+ (as Quint specs can be transpiled into TLA+) was a programming language exercise, and discussions with the team were the most helpful resource, followed by feedback from early users. There are still improvements we want to make, and it might be my favorite part of the job.

You have also worked on static analysis and type systems. How have those experiences influenced Quint’s type checking, tooling, and overall developer experience?

The biggest lesson I learned in that world is that not all languages are the same. You’ll hear people saying that it’s just a matter of learning a new syntax, all the same concepts still apply, so all languages are equal and it’s just a matter of taste. That is not true. The field of programming languages has great researchers that do amazing work to advance this field, and that is not only to make a language look prettier or more to their liking.

Functional programming was introduced to me very early, I learned Haskell at the same time I learned C (my first programming language), and I’m very grateful for that. This is the foundation that helps me see that isolating state mutations and non-determinism to a thin layer in Quint, and having all complexity in pure functions objectively helps in many factors, and it is not only a matter of taste. I don’t think building Quint would have been productive if matters of taste were up to discussion too often.

Teaching formal methods as a lecturer gives you a unique perspective. What are the most common misconceptions engineers have about formal verification today?

Well, I was teaching undergraduate students that were just getting started in the industry. The vast majority of them never heard of formal methods or formal verification before, so no misconceptions! The curriculum was made in such a way that most of them also didn’t learn about distributed systems, and about half of them would be learning about threads in the same semester. I used to tell them I felt like I was teaching them what an umbrella is good for before they had experienced any rain!

I was more motivated to teach them how formal methods and formally specifying a system can help us reason about solutions and find edge cases than to make them think they should formally verify every software they ever write. My final assignment was a tabletop RPG setup where different orders that players could take and different setups had to be taken into account, trying to mimic the difficulties we face in distributed systems as much as I could. It succeeded in being hard enough that they had to use the tools to find edge cases and improve their solutions for beating the monsters in the end. Hopefully, when they face a similar situation at work one day, they will remember me. Some of them already did.

There is growing interest in combining AI with software development. Do you see a role for AI in helping developers write, validate, or even generate formal specifications using tools like Quint?

A significant one, and it is already happening. Computer Science is bigger than writing code, and AI opens the door to completely new ways of using formal methods. LLMs are good at writing Quint specs from natural language descriptions of a system and even existing code. The Quint LLM Kit has Claude Code agents that take an English description of a protocol and produce a Quint spec you can run and check immediately.

At the same time, Quint also helps developers trust code written with AI. I strongly believe that confidence needs to come from understanding, not some magical checkmarks. Working on a Quint specification that drives and checks the implementation code means developers can still own and understand the behaviors of the system, addressing the cognitive debt that AI usage can create and providing more assertive ways of validating the generated code.

We leverage LLMs as language tools that write Quint precise definitions from the natural language intent, and then give the Quint tools to AI so it can accomplish things that it can’t reliably do on its own, like finding edge cases.

Looking ahead, what needs to happen for formal methods to move from niche adoption into a standard part of the software development lifecycle?

For a while now, I know the two high-level things Quint needs for more adoption: lower cost and higher value. I think this applies to a lot of other things too. Formal methods just got a big boost in both those things, with AI tremendously reducing the cost of writing formal specifications and also creating the environment of lack of trust and understanding where formal methods can be the most impactful and valuable.

With AI changing what our profession is, at least to some degree, I hope this change is toward higher-level design choices and behavior correctness, making formal methods an everyday tool; and not toward us not understanding any code or systems anymore and spending all our time reviewing AI-generated code without any toolset to help us reason about it.

Thank you for the insightful interview; readers interested in learning more about this executable specification language for modeling and verifying complex systems, including its tooling and how to get started, can explore Quint.