Vision: Zero Bugs — Johann Schleier-Smith, Temporal

The Vision of Zero-Bug Software

While the idea of software with zero bugs may seem preposterous, it’s a vision worth exploring. For most end-users, software in daily life—from banking apps to social media—is reliable enough that bugs are not a primary concern. However, for software engineers, the reality is a world of constant stress over potential errors, on-call alerts, and outages. This talk bridges that gap, arguing that we are on the verge of making near-perfect software an economic and practical reality.

Objections to the Zero-Bug Vision

There are several reasonable objections to achieving bug-free software:

1. It’s Good Enough: The world is imperfect, incidents happen, and we manage to get through them. For many applications, current reliability standards are sufficient.
2. It’s Impossible: Codebases are too large and complex, specifications are inherently ambiguous, and the real world presents unexpected scenarios (e.g., for self-driving cars). Furthermore, formal verification techniques have known theoretical and computational limits.
3. The Economics Don’t Work: Competitors who prioritize speed over quality may win in the marketplace. The ROI for fixing every single bug isn’t always there, and some business models may even benefit from selling support for buggy software.

Despite these objections, there is substantial evidence that this level of quality is achievable.

A Solved Problem: Lessons from High-Assurance Systems

The aerospace industry, in particular, has demonstrated that building extraordinarily reliable software is possible.

• Airbus A320: The control software for this aircraft, developed in the 1980s, has no serious incidents attributed to software failures. The engineering team adopted a “zero defect tolerance” mindset, treating software as a certified component. Key techniques included:

  • N-version Programming: Critical components were built by separate teams using different processors (e.g., Intel and Motorola) and different operating systems for redundancy.
  • Specification-Based Design: Extensive documentation that could be formally analyzed to provide provable guarantees about the system’s behavior.
  • Independent Verification: The teams writing the code were completely separate from the teams verifying its behavior.
  • Defensive Programming: Techniques like static memory allocation and simplified exception handling to reduce runtime surprises.
  • Static Analysis and Verification: Rigorous automated checks on the code.

• NASA Space Shuttle: This program achieved stunning reliability, with one analysis showing only one error per 420,000 lines of code across its last three versions. Over 11 versions, only 17 total errors were found. No Space Shuttle was ever lost due to a software problem.

• Curiosity Rover: A more modern example from the 2000s, this project showed an evolution by using identical redundant systems and a commercial off-the-shelf real-time operating system, while still achieving the necessary reliability for a mission to Mars.

Foundational Principles for Reliable Software

The ability to build such systems rests on decades of computer science innovation focused on managing complexity.

• High-Level Languages: The move from assembly to high-level languages yielded a 5-10x productivity gain by introducing abstraction. This allows developers to preserve the essential complexity of the problem domain while removing the accidental complexity related to the machine’s implementation details (e.g., memory layout, registers).
• Structured Programming: Championed by Edsger Dijkstra, this paradigm eliminated goto statements in favor of compositional control structures like sequences, selections (if/then/else), and iterations. This enables hierarchical decomposition and local reasoning, turning “spaghetti code” into manageable, understandable programs.
• Modularity: David Parnas’s work on modules allows systems to be broken down into discrete units with clear interfaces (e.g., libraries, objects). This changes the scaling of verification from exponential to sub-exponential or even linear, making it possible to manage the complexity of massive systems.

These principles are just as relevant for LLMs as they were for humans. LLMs use high-level languages because of context window limitations and the immense value of using trusted, pre-verified libraries.

The Power of Formal Methods

Formal methods provide mathematical proof that software adheres to its specification.

A demonstration using the Dafny language showcased this power. Dafny is a programming language that integrates specifications and proofs directly into the code. A verifier can then automatically prove that the implementation meets its specification before generating executable code in languages like Python or C#. The demo showed how the verifier could instantly catch a bug introduced into a simple array search algorithm, preventing the faulty code from ever running.

Formal methods have seen significant commercial success and progress:

• Real-World Use: They are used in the fully verified seL4 microkernel, the CompCert C compiler, Project Everest (for cryptographic libraries), and extensively in microprocessor design.
• Performance Gains: Over the last 20 years, driven by benchmarks, the success rate of verification tools has climbed from ~30% to nearly 100%, while runtimes have decreased by a factor of 50 or more.

Bridging the Gap with Agentic Coding

Agentic coding can leverage these high-assurance principles to overcome its own limitations regarding code quality. Here are practical techniques:

• Provide agents with highly detailed specifications and use typed languages.
• Ask the LLM to perform explicit risk analysis and write safety cases that reason about what could go wrong and how the code mitigates it.
• Emulate independent verification by using separate prompts, or even different foundation models, for generating code versus generating tests.
• Incorporate formal methods like Dafny for critical sections of the code.
• Keep the generated code small and outsource complexity to reliable, well-tested libraries.

The New Economics of Software Development

The primary barrier to widespread adoption of high-assurance techniques has always been cost. Agentic coding fundamentally changes this equation.

A cost-per-line-of-code comparison reveals the opportunity:

• High-Assurance Code (e.g., Space Shuttle): ~$2,500
• Typical Production Code: $10 - $100
• Agentic Code: $0.01 - $1.00

The cost of high-assurance software is roughly 100x that of typical software. However, agentic coding is at least 1,000x cheaper than typical human-written software. This implies that agentic coding has the potential to produce high-assurance software at a cost 100 times cheaper than typical software is produced today.

Conclusion: The Proliferation of Bug-Free Experiences

Software reliability is a solved problem; it has just been too expensive to apply broadly. Agents can make formal methods, extensive process, and adversarial testing economically viable for everyone.

This directly addresses the biggest weakness of agentic coding: the quality and reliability of the output. The reason many developers still write code manually is that it’s often faster than debugging AI-generated code. Once agents can routinely generate software with fewer defects than humans—by applying the very techniques discussed here—their adoption will see an absolute takeoff, ushering in an era of bug-free experiences.

• Tags:
• Software Engineering
• Feature
• Agentic Coding
• Formal Methods
• Software Reliability
• High-Assurance Systems
• Dafny