Podcast: Formal Methods for Every Engineer in an AI-Powered Future

Gabriela Moreira (guest); host Shane Hastie (InfoQ) · podcast · 2026-07-10 Reader 🖥️

Practical · Mixed — an expository interview that is also argumentative (defending formal methods as a practical, human-essential discipline) and carries two embedded narratives (Moreira's Byzantine-fault-tolerance learning story and the AWS DNS-outage case). — Conversational podcast: claims are stated informally, restated and drawn out through Shane Hastie's questions. Almost all propositions are Moreira's; Shane contributes one load-bearing framing move (spec-code drift is an age-old problem). Moreira explicitly rejects the framing of formal methods as an academic responsibility in favour of 'a solution to a problem you already have', which fixes the classification as practical.

Structure

Key terms

• Formal methods Formal Methods
  A practical family of techniques (specification, model checking, model-based testing, trace validation) for precisely reasoning about, and checking, the behaviours of complex systems — framed as a solution to an edge-case problem, not an academic obligation.
• Quint Formal Methods
  A new specification language Moreira has built for four years, based on TLA+ but stripped of the parts that were too hard for newcomers — TLA+'s power made accessible; now a spin-out she leads as CEO.
• TLA+ Formal Methods
  A mathematical formal-specification language for defining what a system can do and the properties it should hold; expressive but hard to learn, and the ancestor of Quint.
• Specification / model
  A state machine describing what a system or solution can do; you define initial states, transitions, and properties, then run it to observe behaviours — deliberately more abstract than the code.
• Model checking Formal Methods
  Automatically exploring a specification's state space to find behaviours, verify properties, and surface corner cases — the act of 'running' the spec where most of the value lives.
• Model-based testing (MBT) Formal Methods
  Deriving tests from the model: replaying behaviours from the spec against the real implementation and checking that the resulting states match step-by-step; can use random or targeted (witness) behaviours.
• Glue code / harness code
  The replay code that links a model to an implementation for model-based testing — tedious and annoying to write and maintain, historically the main reason MBT never caught on, and exactly what AI is good at generating.
• Trace validation Formal Methods
  Checking real production execution traces (via logging/instrumentation) against the spec to ask 'is this compliant with what you said?' — the frontier for connecting formal specs to runtime monitoring.
• Witness
  A property you deliberately expect to break in order to witness an interesting or rare behaviour; used to challenge the tools ('the most cornery corner case I can come up with') and to gain confidence that the tools find scenarios at least as well as you can.
• Failure modes
  Explicitly modelled external failures (and the system's response to them) — needed because a system's whole point may be to recover from failure; modelling them reveals 'which ways does your software break' when failures exceed tolerance.
• Reproducible behaviours
  Specific modelled scenarios (like 'process B accesses X while process A holds the lock') written down executably — whiteboard reasoning made concrete without sacrificing abstraction, usable as documentation, in PR descriptions and on CI.
• Corner case / edge case
  The rare event sequences in complex systems that developers are expected to anticipate 'in their heads' but cannot — the core problem formal methods exist to address.

Propositions

• explicitFormal methods are best understood not as an academic discipline or a professional responsibility to fulfil but as a practical solution to a problem engineers already have: reasoning about all the edge cases of complex systems.conf: high
• explicitMost non-trivial systems have enough complexity that different sequences of events lead to different outcomes, and it is infeasible for developers to hold all the possible sequences in their heads.conf: high
• explicitdevelopedIn 2026 the fastest way to start with formal specification is to ask your favourite AI to generate a Quint or TLA+ spec for your system, which collapses the historic barrier of learning a new language, a new tool, and how to think in state machines.conf: high
  supportsSoftware Design in the Agentic Age: Place Your Bets · p9 — That doc claims formal modelling is on the rise because agents lower its barrier (they can create/explain models and use them to verify outputs); this conversation is the concrete embodiment — AI generating Quint/TLA+ specs plus the glue code that verifies against implementations.
  extends ←Transcript for Cursor Team: Future of Programming with AI | Lex Fridman Podcast #447 · p19 — Arvid's 2024 speculative vision (model proposes a formal spec, human reviews it, a reasoning model proves the implementation matches) is an early articulation of what the later piece describes as already-practical: asking an AI to generate a Quint/TLA+ spec as the fastest on-ramp to formal methods.
• explicitThe value of a specification comes from running it — model checking it and generating behaviours — not merely from reading the spec the AI produced.conf: high
• explicitFormal specification operates at a higher, more abstract level than tests, so it can reason about concurrency, scheduling, timing and message-delay scenarios that are hard or impossible to control in ordinary tests.conf: high
• explicitFormal tools can synthesize a scenario for you on demand ('give me a behaviour that reaches this rare state'), whereas conventional testing requires the engineer to enumerate the scenarios manually.conf: high
• explicitModel-based testing keeps a specification and its implementation in sync by replaying behaviours from the model against the real code and checking that the resulting states match step-by-step.conf: high
  supportsSoftware Design in the Agentic Age: Place Your Bets · p11 — Supports 'executable specifications are the strongest bet because non-deterministic agent code is safest when deterministic verification can predictably find faults' — model-based testing is precisely deterministic replay of a spec against the implementation.
  extendsPresentation: AI-First Software Delivery: Balancing Innovation with Proven Practices · p8 — That doc argues tests written after code are brittle because the LLM fits the test to the code, and specs-before-code avoid it. Model-based testing extends this: the tests are derived from a model that is deliberately MORE ABSTRACT than and independent of the implementation, so they cannot be fitted to the code at all.
• explicitThe tedious glue/harness code that links a model to an implementation is the main historical reason model-based testing never became mainstream, and AI removes that barrier because such code is trivial and boring to generate and maintain.conf: high
• explicitA well-designed glue-code library such as Quint Connect doubles as guardrails for AI: it gives interfaces the AI simply fills, so the linking code is generated without the model having to invent anything.conf: high
• explicitThere is no easy correctness 'check mark' to ship on; formal methods yield confidence only in proportion to how much you genuinely understand your system.conf: high
• explicitWriting a formal spec is not by itself sufficient to understand a system; the understanding comes from running it and producing witnesses that reproduce the corner cases.conf: high
• explicitReproducible behaviours turn whiteboard-level reasoning into executable documentation that colleagues can run, put in PR descriptions and check on CI — without sacrificing the abstraction level of the whiteboard.conf: high
• explicitThe model should be more abstract than the code; otherwise you forfeit the power of abstraction and are merely re-reasoning about the code itself.conf: high
• explicitcorroboratedSpecifications abandoned in a repository folder are dangerous, because code drifts away from a correct original design over time and reintroduces bugs the model had ruled out.conf: high
  supports ←Comprehension at AI Speed: Building a Context Store for Evolutionary Architecture · p7 — Independently converges on the same failure mode: a specification left unmaintained in the repository drifts from the implementation and becomes actively misleading rather than merely stale.
• explicitKeeping design and code in sync is an age-old problem in software engineering (present since the COBOL era); spec-code drift is not new.conf: high
• explicitAI is a genuinely new and better solution to the age-old spec-code drift problem because LLMs excel at exactly the boring connective work — generating glue code, instrumentation, and parsing logs to extract and check behaviour against the spec.conf: high
• explicitDefining which system behaviours are correct or incorrect is essential human work that AI cannot take over; it is the part of the profession that has to remain ours.conf: high
  supportsAgents don't know what good looks like. And that's exactly the problem. · p10 — That doc's key shift is controlling OUTCOMES (whether the system behaves correctly) over controlling output; Moreira's 'defining which behaviours are correct is essential human work' names the human faculty behind that shift.
  supportsHave your agent record video demos of its work with shot-scraper video · p8 — Both locate the non-delegable human contribution in judging edge-case behaviour rather than typing code; formal methods are Moreira's precise language for that residual work.
• explicitFormal methods give engineers a precise, executable language that both preserves human understanding of a system even when AI writes the code and lets them assert that AI-generated code is correct.conf: high
  supportsWhat Survived Contact · p1 — Concrete instance of 'rigor migrates upstream into specifications and down into test suites/constraints' — the formal spec is the upstream rigor, model-based testing the downstream test-suite instrumentation.
• implicitAI writing more of the code makes precisely defining correct behaviour more important rather than less, because human understanding must then be preserved in an artifact other than the code itself.conf: medium
  supports13) Tobias K. Torrissen om kodekvalitet, konferanser og AI · p14 — Supports the claim that only ~20% of development is programming while the other 80% (understanding, deciding) remains human — Moreira's version is that defining correctness and understanding the system stay human even as AI writes the code.

Arguments

Narratives

• At Informal Systems, surrounded by PhDs who discussed Byzantine fault tolerance and consensus fluently, Moreira struggled to understand even basic distributed protocols. Writing a formal specification for one algorithm was not enough; only when she ran it and produced witnesses for its corner cases — finally writing one reproducible example for the algorithm's most extreme case — did she feel she truly understood it, an understanding that has stuck.
  → Grounds the claim that understanding comes from running a spec and producing witnesses, not from writing it (p11), and that confidence scales with genuine understanding rather than a check mark (p10).
• In October (last year), AWS suffered a DNS outage. The original design was correct and the initial code was correct; the bug arose because the code diverged from the design over time. As presented at AWS re:Invent, they made their (previously informal) documentation into a formal model and used an AI tool to compare the new model against the code — the AI read both and found a divergence, which they then fixed.
  → Supports both the spec-code-drift danger (p14) and the claim that AI is a new, better solution to the age-old sync problem because it can compare model to code and surface divergence (p16).
• Moreira's own arc: introduced to compilers and type systems during her bachelor's, pointed at TLA+ by a colleague ('I think you will like it'), she fell in love with it, built TLA+ tooling through her master's while working on event-driven distributed systems, was found and hired by Informal Systems at a TLA+ conference, spent four years building Quint (an accessible TLA+), and is now spinning Quint out as CEO.
  → Establishes credibility and motivates the accessibility mission — the conviction that formal methods 'should be used more' and made easy enough for newcomers (frames p1 and p3).

Questions addressed

• ✅ Why should software engineers care about formal methods?
  They already do, implicitly: formal methods are reframed as the solution to an edge-case problem engineers already face, not a responsibility to take on.
• ✅ How is formal methods different from just good test design?
  Formal specs work at a higher abstraction that can reason about concurrency/timing/scheduling tests cannot control, and the tools synthesize scenarios for you instead of requiring manual enumeration.
• ✅ How do I get started and integrate this into my workflow?
  In 2026: ask an AI to generate a first Quint/TLA+ spec, run and refine it, then wire it to the code via model-based testing (AI-generated glue code) and, at the frontier, trace validation against production.
• ✅ What is the relationship between the model and my codebase, and how do you keep them in sync?
  The model is deliberately more abstract than the code; the two are kept in sync by model-based testing (replaying model traces against the code) and by trace validation (checking production traces against the model).
• ✅ What does this mean for our profession if AI is writing the code?
  Defining which behaviours are correct or incorrect remains essential human work AI cannot take; formal methods preserve both understanding/confidence and professional value.
• ⭕ Who verifies that the AI-generated specification and glue code are themselves faithful and correct?
  Left unaddressed: the advice is to proceed 'when you're happy with your specification', but how you gain warranted confidence in an AI-authored spec and its AI-authored glue code — when understanding was the original barrier — is never explained.

Gaps

• incompleteThe spec-verification circularity. The whole 2026 pitch is that AI removes the barrier to WRITING the spec and the glue code. But Moreira also insists there is 'no easy check mark' and that confidence requires 'a lot of understanding'. Judging that an AI-generated spec is a faithful representation of the intended system, and that the 'trivial' AI-generated glue code is correct, still requires exactly the deep understanding that was the original barrier. The talk papers over this with 'when you're happy with your specification' and 'it's very easy for AI to generate the code without inventing anything' — never saying how a newcomer reaches warranted confidence in artifacts they did not author.
  Read next: Read against the corpus's LLM-fidelity material: llm-limitations (silent corruption, non-determinism, over-attribution) and verifiability, plus the finding that AI code which 'works' is not thereby correct or secure (extract-founders-playbook-building-ai-native-startup#p9) and that agents generating lots of software says nothing about whether it is correct (extract-ai-funhouse-mirror-velocity-debt#p3). Also extract-ai-first-software-delivery#p8 on tests fitting the code rather than the intent — the same fidelity risk one level up, at the spec.
• incompleteThe boundary of 'essential human work' is asserted but under-drawn. Moreira says product people can safely leave AI to build software 'when safety and big concerns' are absent, while complex concurrent systems still need technical judgment — but she gives no criteria for classifying which systems warrant formal specification versus which can be left to unspecified AI generation. Without that decision procedure, 'defining correct behaviour is essential human work' cannot be operationalised: a team cannot tell where the line falls for their system.
  Read next: Read alongside risk-tiering / not-all-software-is-equal material — the autonomy-boundary and classification gap in extract-ai-funhouse-mirror-velocity-debt#g4, and the risk-tiering concept — which frame exactly the 'which changes get which rigor' judgment this talk leaves implicit.
• incompleteTrace validation for runtime monitoring is named as the frontier ('we are going to focus on developing infrastructure for that') and simultaneously conceded to be hard and historically infeasible ('you have to orchestrate your code, there's a bunch of challenges'). How you instrument production, faithfully parse logs into behaviours, and orchestrate real code for trace validation at scale is left as future work, so the strongest version of the pitch (specs connected to production behaviour, not just tested behaviour) is promissory rather than demonstrated.
  Read next: Read against the AWS re:Invent case in full detail, and against agent/observability material (agent-observability) on capturing and interpreting production telemetry — the practical substrate trace validation would need.
  closed byGrafana's gcx and MCP Server Reach GA for Telemetry-Driven Agent Development — That gap named production trace validation and orchestrating real code against production behavior as future, largely-infeasible infrastructure work. Grafana's now-GA gcx CLI and MCP server are concrete shipping infrastructure for exactly this: agents querying live traces/metrics/logs, tracing dashboard queries back to the code that generates them, and grounding test/implementation decisions in observed behavior — though this closes the 'infrastructure exists' half of the gap, not the harder 'validate against a formal spec' half, which remains open.

Closes gaps elsewhere

• What Survived Contact · g3 — g3 asks how to build a self-generating oracle for genuinely NEW behaviour, where no running reference implementation exists to reference an expected answer from live. Formal methods supply exactly that: instead of computing the expected answer from a pre-existing running system, the engineer authors an abstract formal model of the intended behaviour and uses model-based testing to replay the model's behaviours against the implementation — the authored model itself becomes the oracle, constructed from understanding before any reference implementation exists. (Note the mechanism difference from the referenced-oracle case: the answer is authored, not referenced live.)

Related documents

• 13) Tobias K. Torrissen om kodekvalitet, konferanser og AI
• Presentation: AI-First Software Delivery: Balancing Innovation with Proven Practices
• What Survived Contact
• Have your agent record video demos of its work with shot-scraper video
• Software Design in the Agentic Age: Place Your Bets
• We've Stopped Arguing About Whether AI Changes Software
  Agentic Engineering Code Was Never the Bottleneck Taste & Judgment Verifiability (as the Quality Bar)
• Comprehension at AI Speed: Building a Context Store for Evolutionary Architecture
  Code Was Never the Bottleneck Evolutionary Architecture & Fitness Functions Verifiability (as the Quality Bar)
• Eight years of wanting, three months of building with AI
  Mental Models & Understanding Software Design Fundamentals Taste & Judgment
• Notes from FOSE Europe
  Agentic Engineering Software Design Fundamentals Taste & Judgment
• The third golden age of software engineering – thanks to AI, with Grady Booch
  Agentic Engineering Code Was Never the Bottleneck Mental Models & Understanding