A Mere Formality

Ray and John have a  conversation with Annie Vella in this episode about why formal verification, a discipline she first encountered more than twenty years ago, is suddenly becoming increasingly relevant in the age of AI-assisted software development.

With a background spanning mathematics, computer science, software engineering, DevOps, and large-scale banking systems, Annie Vella first studied formal methods at university in the early 2000s. At the time, proving software correct mathematically was intellectually rewarding but difficult, expensive, and rarely practical in everyday software development. Today, better tooling and the rapid rise of AI-generated code are changing that equation.

We explore a growing problem in software engineering: AI can generate code dramatically faster, but that simply moves the bottleneck downstream. If humans remain responsible for reviewing every generated line, the promised productivity gains become difficult to realize. Formal verification offers another possibility. Rather than manually inspecting everything an AI produces, can we mathematically verify the properties that actually matter?

That leads us into the importance of specifications. Annie discusses the renewed interest in spec-driven development, the difference between lengthy natural-language requirements and genuinely formal specifications, and how tools such as Dafny, Verus, Lean, SMT solvers, and emerging AI-assisted approaches could make rigorous verification more accessible to everyday engineers.

However, verifying AI-generated code is only part of the challenge. Agentic systems introduce an even deeper problem: agents can dynamically make decisions, invoke tools, generate code, and take actions at runtime. Annie offers a deceptively simple example that an agent instructed to delete duplicate files could technically satisfy that requirement by deleting every file. Correctness therefore depends not only on verifying an outcome, but on precisely defining what the system is and is not allowed to do.

We also examine what this could mean for highly regulated environments such as banking. Formal methods may provide a way to define critical invariants, constrain dangerous agent behavior, and even help modernize legacy systems by formally capturing essential properties before replacing decades-old implementations.

Ultimately, our conversation comes back to something deeper than tooling. Building trustworthy AI-enabled systems requires engineers to become better at defining what they actually mean by “correct.” Formal verification forces that clarity. As AI makes generating software increasingly cheap, the ability to specify, verify, and reason about what that software should do may become one of the most valuable engineering skills of all.

Show Notes:
Birgitta Böckeler and Laura Tacho on Spec Driven Development
https://www.thoughtworks.com/insights/podcasts/technology-podcasts/what-is-spec-driven-development

Developing provably correct Rust code with Verus
https://www.amazon.science/blog/developing-provably-correct-rust-code-with-verus

Dafny
https://dafny.org/

LemmaScript
https://lemmascript.org/

Guardians of the Agents: Formal verification of AI workflows by Erik Meijer
https://dl.acm.org/doi/10.1145/3777544

Fermat's Last Theorem, Xena project commentary on Anthropic's proof
https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/

Easy Approach to Requirements Syntax (EARS)
https://en.wikipedia.org/wiki/Easy_Approach_to_Requirements_Syntax

https://kiro.dev/blog/deep-spec-analysis/

https://www.amazon.science/blog/developing-provably-correct-rust-code-with-verus

https://cdn.amazon.science/bb/40/22ac44f84f6d8eb625ac9666a00f/formally-verified-cloud-scale-authorization.pdf

https://midspiral.com

https://dl.acm.org/doi/pdf/10.1145/3815784

https://dl.acm.org/doi/10.1145/3777544

https://kiro.dev/docs/specs/feature-specs/

https://dl.acm.org/doi/abs/10.1145/3815784

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.

In this episode of the Profound Podcast, I sit down with Ray Myers, a tech lead in chaos engineering at Indeed.com with a rich background in software engineering across multiple prominent companies. We delve into the fascinating intersection of artificial intelligence and software development, exploring how AI can both augment and challenge the conventional workflows in programming as well as his thoughts on Devin.

Ray discusses his journey into AI, spurred by the developments in generative AI technologies like GPT-4. His insights draw from a traditional AI education but are deeply influenced by the rapid advancements in the field, particularly in areas like natural language processing and code generation. Ray shares his perspective on how AI is reshaping software development, pointing out both the potential benefits and pitfalls.

Ray provides a nuanced view on the recent buzz around Devin AI, addressing its marketed capabilities versus its actual functionality. He discusses the initial excitement in the tech community about Devin's potential to automate coding tasks and the subsequent realization of its limitations. Ray emphasizes the importance of understanding what AI tools genuinely offer versus the hype often propagated by marketing efforts, stressing that these tools should be seen as augmentations to a developer's capabilities, not replacements.

Ray's LinkedIn can be found below:
https://www.linkedin.com/in/cadrlife/

In this episode of the Attention is All You Need Podcast, I talk with Reza Rassool, a  big-shot in the realms of digital transformation and AI innovation. Our discussion navigates through the intricate landscape of artificial intelligence and its implications on personal identity and data ownership.

Rassool's journey from pioneering video editing technologies to spearheading advancements in digital rights management, including his significant role in the creation of technologies sold to Google, sets the stage for an exploration of AI's current trajectory. With an illustrious career that has seamlessly blended physics, video and audio manipulation, and AI, Rassool offers unique insights into the computational and ethical challenges facing today's digital world.

The conversation pivots to Rassool's recent endeavors, particularly his founding of Kwaai, a non-profit initiative aimed at democratizing AI through open source collaboration and personal AI ownership. This venture represents a critical countermeasure against the monopolization of AI by a handful of corporations, advocating for a model where individuals control their digital personas and intellectual properties. Rassool eloquently argues for a future where AI serves as an empowering tool for individuals, rather than a mechanism for further concentration of wealth and power.

Amidst our discussion, Rassool also touches upon the significance of physics-informed approaches to AI, advocating for a shift from data-heavy models to those grounded in the fundamental laws of physics, potentially revolutionizing AI's efficiency and application.

This episode not only sheds light on Rassool's visionary pursuits but also ignites a crucial dialogue on the ethical dimensions of AI, urging us to reconsider our relationship with technology and its role in shaping our future.

You can find Reza Rassool's LinkedIn below:
https://www.linkedin.com/in/rezarassool/

In this episode of Profound,  I talk with Dr. Khai Minh Pham, whose unique approach to artificial intelligence challenges conventional paradigms and opens new frontiers in AI research and application. Dr. Pham, with his extensive background in both medicine and artificial intelligence, shares his journey towards creating a distinctive AI framework that prioritizes knowledge over data, steering clear of the traditional data-centric methodologies that dominate the field.

Dr. Pham recounts his early realization of the limitations inherent in human cognitive processes and how this propelled him to explore AI as a means to augment human memory and decision-making capabilities. 

Central to this episode is Dr. Pham's critique of the prevailing AI models that rely heavily on data processing and pattern recognition. He introduces his concept of "macro connectionist AI," a system that mimics human reasoning more closely by forming high-level knowledge representations rather than merely processing data inputs. This approach, according to Dr. Pham, not only enhances AI's problem-solving capabilities but also significantly reduces the computational resources required, challenging the current industry trend towards increasingly complex and energy-intensive AI systems.

you can find Dr. Pham's LinkedIn below:
https://www.linkedin.com/in/khai-minh-pham/