AI says you’re right, formal methods say you’re wrong

Summary of AI says you’re right, formal methods say you’re wrong

by The Stack Overflow Podcast

28m•October 16, 2026
Listen to Episode

Overview of The Stack Overflow Podcast

In this episode, Ryan Donovan speaks with Gabriela Moreira, CEO at Quint, about formal verification for agentic coding and why tools like TLA+ and Quint are becoming more relevant in the age of AI-assisted development. The conversation covers how formal methods help teams specify software behavior precisely, catch logic bugs earlier, and validate that implementations match intended behavior—especially in distributed systems, infrastructure, and agentic workflows.

Key Topics Discussed

How Gabriela got into software

  • Started in computer science in 2015, inspired by:
    • customizing Tumblr themes
    • troubleshooting a slow gaming computer
  • Became especially interested in:
    • discrete math
    • graph theory
    • compilers
    • computer theory
    • formal methods
  • Discovered TLA+ near the end of her degree and kept working with it from there.

Why formal methods feel intimidating

  • Formal methods often get a reputation for being:
    • strict
    • academic
    • hard to use
  • Gabriela argues the reputation is partly due to how they’re presented:
    • too abstract
    • not clearly tied to real engineering pain points
  • In practice, she says they are useful for everyday development when applied well.

What TLA+ Is and Why It Matters

TLA+ as a formal specification language

  • TLA+ is used to describe what software should and should not do.
  • Its key property is no ambiguity:
    • each statement has a precise mathematical meaning
  • It is especially suited to:
    • algorithms
    • distributed systems
    • protocols

Leslie Lamport’s motivation

  • TLA+ was created by Leslie Lamport, who wanted a more precise way to write distributed systems ideas after noticing imprecision in his own papers.
  • The language later gained tooling, including the TLC model checker, which verifies specifications.

Model checking vs. code verification

  • TLA+ usually checks the specification, not the final production code directly.
  • Gabriela notes that verifying full codebases is much harder because real code has a much larger scope.
  • The strength of TLA+ is that it can check most of what’s written in the language because it’s designed for that purpose.

Where Formal Specifications Fit in Development

Ideal workflow: spec first, implementation second

  • The classic use case is:
    1. write the formal specification
    2. verify behavior and properties
    3. implement the software
  • Gabriela compares it to drawing a blueprint before building a house.
  • This approach helps catch design flaws before they become expensive code bugs.

Specs are also useful after code exists

  • Formal specs are not only for greenfield work.
  • They can also:
    • expose design issues in existing systems
    • help evaluate possible fixes before changing code
    • reveal edge cases not obvious in implementation

Quint: Making TLA+ More Accessible

What Quint is

  • Quint is a more approachable syntax and tooling layer on top of TLA+.
  • It keeps the same formal foundation but is designed to be easier for engineers to read and write.
  • The goal is to lower the barrier to adoption for industry teams.

Why accessibility matters

  • Gabriela emphasizes that engineers think in terms like:
    • AND
    • OR
    • behaviors and state changes
  • They do not want to fight symbolic syntax if they can avoid it.
  • Quint makes formal methods feel more familiar and practical.

AI, Formal Methods, and “Spec-Driven Development”

AI can help with specs—but also creates new risks

  • Gabriela notes that AI can now help write formal proofs and specifications.
  • But the bigger risk is delegating the specification itself to AI without understanding it.
  • Her concern: if you don’t know what you specified, then what exactly have you proven?

The danger of vague spec-writing

  • She criticizes AI-driven “spec-driven development” approaches that rely on:
    • markdown
    • prompts
    • loose natural-language descriptions
  • Her view:
    • markdown is still imprecise
    • specs must be executable and checkable
    • a spec should not just be a larger prompt

Why execution matters

  • One reason programming is satisfying is that you can:
    • write something
    • execute it
    • observe results
    • refine it
  • Gabriela wants formal specs to preserve that interactive loop:
    • write
    • run
    • inspect
    • adjust

Real-World Example: Catching a Bug Before Production

OpenHands/Kubernetes example

  • Gabriela describes a case involving OpenHands and a Kubernetes deployment bug.
  • The issue was a race condition causing repeated alerts.
  • A fix was attempted, but Quint showed the fix was insufficient.
  • Later, the actual problem appeared in production exactly as the spec predicted.
  • The team iterated until Quint verified a fix that eliminated the issue.

Main lesson

  • Formal tools are especially valuable because they can say:
    • “this is wrong”
    • “this behavior is not allowed”
  • Gabriela jokes that AI assistants often say “you’re absolutely right,” while formal methods are more useful because they point out what is broken.

Behaviors, Not Just Code

Core idea: specify behaviors

  • Gabriela repeatedly returns to the idea that software should be understood as a set of possible behaviors.
  • A behavior is a sequence of states or steps, such as:
    • deposit
    • withdraw
    • transfer
  • Formal specs describe which behaviors are allowed and which are not.

Why this helps with AI development

  • As AI generates more of the code, the important question becomes:
    • Does the system behave correctly?
  • Focusing on behaviors helps teams reason about:
    • core logic
    • protocols
    • invariants
  • It also avoids getting bogged down in unimportant implementation details.

How Formal Specs Help Find Bugs

Bugs become more visible

  • A specification can make implicit assumptions explicit.
  • Example:
    • “No negative balances”
    • “Every if-statement must define an else branch”
  • By forcing precision, specs reveal edge cases that may be easy to miss in code.

Spec-writing can uncover issues without model checking

  • Gabriela says her team often found bugs simply by writing the spec, before running any tool.
  • This happened during security audit work:
    • the act of formalizing the behavior exposed gaps and inconsistencies
  • That’s one reason she values formal methods even before automated verification kicks in.

Where Quint Fits in the SDLC

Design phase

  • Best place to use formal specs:
    • during solution design
    • before implementation
  • Useful for validating architecture and protocol decisions early.

Testing and validation

  • Formal specs can also support testing by checking that code matches the model.
  • Two approaches discussed:
    • Model-based testing: replay behaviors from the spec against real code
    • Trace validation: validate production logs or test traces against the spec

Quint Studio

  • Quint’s product, Quint Studio, aims to make this behavior-centric workflow easier.
  • It can:
    • analyze test traces
    • suggest missing tests
    • help bridge the gap between specifications and production behavior
  • Quint is also open source and can transpile to TLA+.

Main Takeaways

  • Formal methods are becoming more relevant in the AI era because code generation increases the need for precise behavioral specs.
  • The real value of TLA+ and Quint is not just proving things, but making software behavior explicit and checkable.
  • Gabriela’s central thesis is that teams should think in terms of behaviors, not just code.
  • AI can help write specs and proofs, but humans still need to ensure the specification reflects actual intent.
  • Formal methods are no longer just for safety-critical systems—they’re increasingly useful for everyday engineering, especially when correctness and complex behavior matter.

Mentioned Tools and Technologies

  • TLA+
  • Quint
  • TLC model checker
  • Lean
  • Coq
  • Isabelle
  • Agda
  • Alloy
  • OpenHands
  • Kubernetes
  • AWS

Closing Notes

Gabriela’s pitch is that formal methods should feel less like a niche academic exercise and more like a practical way to build reliable software in an AI-heavy world. Her goal with Quint is to make formal specification more accessible, more executable, and more centered on real system behavior.