Technology
AI Is Making Formal Methods Practical for Every Software Engineer
As AI models grow capable of generating formal specifications, the once-esoteric practice of verifying system behavior is becoming accessible to mainstream developers—but defining correctness remains uniquely human work.
InfoQ
Formal methods—the mathematically rigorous practice of specifying and verifying system behavior—have long remained confined to specialized domains. Now, as generative AI makes it easy to auto-generate formal specifications, the field is poised to reach mainstream engineers building complex, distributed systems.
In a conversation with Shane Hastie of the InfoQ Engineering Culture Podcast, Gabriela Moreira, CEO of the newly spun-out Quint specification language, described how AI is dismantling the historically high barrier to entry. Rather than requiring years of mathematical training, engineers can now describe their system in plain language, ask an AI to generate a formal specification in Quint or TLA+, and immediately run it to explore system behavior.
From Theory to Practical Problem-Solving#
Formal methods address a concrete challenge that all software engineers face: reasoning about the countless edge cases and race conditions that emerge in distributed and concurrent systems. While simple, synchronous systems are often straightforward to test, complex systems involving message delays, lock scheduling, and asynchronous events are notoriously difficult to reason about through conventional testing alone.
Rather than framing formal methods as an obligation to learn, Moreira reframes it as a solution to problems developers already have. When a system's behavior depends on unpredictable sequences of events—whether from OS scheduling, network delays, or user actions—formal methods provide the tools to define, explore, and verify those behaviors systematically.
Model-Based Testing Bridges Specifications and Code#
The most practical application for developers is model-based testing, which directly connects formal specifications to real implementations. Engineers extract behaviors from their formal model and replay them against actual code, catching divergence early.
The major historical obstacle to this workflow was the need to write "glue code" or harness code—tedious boilerplate that maps abstract model behavior to concrete implementation calls. Every change to either the model or code required painful maintenance.
AI changes this entirely. Quint Connect, an open-source library for Rust (with community implementations emerging for TypeScript, Zig, and Go), uses AI-friendly interfaces that make generating and maintaining this integration code straightforward. The library essentially provides guardrails that allow AI to fill in the glue code without guessing or inventing logic.
