In this inaugural episode, John Willis and Ray Myers sit down to launch A Mere Formality, a new conversation exploring formal methods, software verification, and the search for certainty in an increasingly AI-driven world. Ray introduces formal methods as a family of techniques for applying mathematical rigor to software, an area he believes is poised for renewed importance as AI coding agents become more autonomous.
First, John and Ray trace the path that brought them to this topic, from the rise of generative AI and coding agents to growing concerns about uncertainty, evaluation, containment, and risk. If an AI agent can not only generate code but also make decisions and take actions, how do we establish confidence that the resulting systems will behave as intended? Their discussion positions formal methods as a potential bridge between the nondeterministic nature of AI and the deterministic assurances required in consequential software systems.
Then, Ray breaks down the distinction between formal methods, formal specification, and formal verification, explaining how specifications can allow teams to reason rigorously about a system's design before, or alongside, its implementation. They explore tools such as TLA+, Quint, and Lean, including how formal specifications can uncover race conditions and unexpected behaviors in distributed systems that conventional prose or Markdown specifications may miss.
The conversation also looks at the history of formal methods in high-consequence environments, from aerospace and medical systems to cloud providers such as Amazon. John draws a parallel with technologies like cloud computing and containers: capabilities once reserved for technology giants can eventually become accessible to everyone. Could formal verification be approaching its own “Docker moment,” where previously specialized techniques become practical for mainstream software development?
Finally, John and Ray examine the relationship between AI and mathematical proof. Rather than viewing AI as a replacement for rigor, they discuss the potential power of combining LLMs with theorem provers such as Lean, using AI to explore solutions while formal systems provide a mechanism for checking them. That combination could become increasingly important as organizations deploy autonomous agents in high-consequence environments such as banking and financial services.
The episode sets the direction for A Mere Formality: exploring how formal methods can move beyond their academic and specialized roots to help us build, evaluate, and trust the next generation of software. As AI accelerates our ability to create code, the bigger question may be how we create certainty at the same speed.
