A large test suite should make developers feel safer changing software. Gabriela Moreira, CEO of Quint, has recently experienced something quite different: a new codebase grew from roughly 200 tests to 800 with the help of AI, yet she found herself trusting the suite less and manually verifying behavior more. Gabriela and Robby unpack the difference between having tests and understanding what those tests actually protect, including why she has a particular appreciation for regression tests that preserve the history of real problems.
That question of understanding leads into Gabriela's work on Quint, an open-source executable specification language influenced by TLA+. Gabriela explains how developers can model behaviors and explore edge cases before those scenarios reach production. Rather than treating formal methods as something reserved for banks and safety-critical systems, she makes the case for using specifications more broadly to reason about concurrency, state changes, multiple users, and other situations where software can behave in more ways than a developer can comfortably keep in their head.
The conversation also digs into the relationship between specifications and existing test suites. Gabriela describes model-based testing, trace validation, and the challenge of keeping a specification synchronized with the code that actually runs in production. She also shares a Kubernetes example involving the OpenHands team, where modeling a race condition with Quint showed that a proposed fix would still fail in another scenario. The team could explore another solution before waiting for the intermittent production problem to return.
As AI takes over more implementation and debugging work, Gabriela argues that developers need to strengthen their judgment about how software should behave. She pushes back on workflows where humans are expected to fully describe a solution in a giant Markdown document before handing it to an agent. For Gabriela, some of the useful and enjoyable parts of programming come from experimentation: trying something, seeing what happens, changing your understanding, and trying again. If agents increasingly handle the mechanical work, preserving that ability to explore, evaluate, and make decisions may matter more than simply producing more code.
Topics & Timestamps
- [00:00:53] What Makes Software Maintainable? Gabriela starts with trustworthy tests and explains why confidence comes from understanding both the tests and the behavior they protect.
- [00:03:06] When Hundreds of Tests Still Aren't Reassuring: Gabriela describes a new AI-assisted codebase that quickly grew from around 200 tests to 800, while her confidence in the suite declined.
- [00:06:00] What Is Quint? Gabriela introduces Quint as an executable specification language and explains how it can be used to model and verify software behavior.
- [00:08:29] Where Formal Specifications Fit in Everyday Development: Robby asks whether these techniques apply to ordinary web applications, leading to examples involving multiple users, state changes, and edge cases.
- [00:12:23] Why Build Another Specification Language? Gabriela explains Quint's relationship to TLA+ and why her team wanted to make formal specification more approachable for working programmers.
- [00:16:15] Who Is Quint Actually For? Gabriela makes the case that reasoning about software behavior isn't limited to developers working on distributed systems or critical infrastructure.
- [00:18:11] AI Lowers the Barrier to Formal Methods: Gabriela explains how coding agents have changed the cost of learning and writing formal specifications.
- [00:20:52] Keeping Specifications and Code in Sync: Gabriela walks through model-based testing, trace validation, and the maintenance problems that arise when specifications drift away from implementation.
- [00:25:00] Who Decides What "Correct" Means? Robby and Gabriela explore the difference between obvious correctness properties and product behaviors that require human context and judgment.
- [00:31:58] Bridging Academia and Everyday Software Development: Gabriela discusses the divide between programming-language research and industry, and why she wants formal methods to become more accessible.
- [00:35:22] Catching a Kubernetes Fix Before Shipping It: Gabriela shares how the OpenHands team modeled an intermittent Kubernetes problem and discovered that their first proposed fix wouldn't actually solve every scenario.
- [00:40:00] What Should We Still Delegate to Humans? The conversation turns to AI development workflows and why Gabriela doesn't want programming to become writing exhaustive instructions for agents.
- [00:45:25] Human Judgment as a Software Engineering Skill: Gabriela argues that developers who can judge how software should behave may become more valuable as AI takes over more implementation work.
- [00:47:06] A Small Formal Methods Homework Assignment: Gabriela suggests starting with something familiar, finding the state machine hiding inside it, and modeling it with Quint.
- [00:50:47] Recommended Reading: Gabriela recommends The Name of the Wind by Patrick Rothfuss.
Thanks to Our Sponsor!
Your test coverage says 90%, but that might be misleading. Undercover CI looks at your Ruby pull requests and shows you which parts of your changes weren't tested- not just overall coverage, but what changed and what got missed, down to the method level. Visit undercover-ci.com and use code MAINTAINABLE for 15% off your first billing cycle. Free for public repos. Private repos with unlimited users also available.
