Aerospace software has achieved extremely low defect rates through specifications, independent verification, redundancy, defensive programming, and disciplined processes.
2
Agentic coding needs stronger assurance methods because generated code is cheap, nondeterministic, and difficult to verify by inspecting output alone.
3
If agents can produce high-assurance software at a fraction of today's cost, zero-bug experiences could become practical in more applications.
Summary
Johann Schleier-Smith argues that software with zero bugs is difficult but possible in systems built with high-assurance engineering practices. He uses Airbus A320 and Space Shuttle software to explain how specifications, independent verification, static analysis, redundancy, simple designs, and carefully managed processes produce extremely reliable systems. He then traces related ideas through high-level languages, structured programming, modularity, libraries, and formal methods. A live Dafny example shows a verifier rejecting a deliberately introduced bug before the generated Python code runs. These methods have limits, especially when specifications are incomplete and when software includes nondeterministic LLM behavior. Schleier-Smith's practical advice for agentic coding includes detailed specifications, explicit risk analysis, safety cases, separate prompts or models for coding and testing, formal proofs for critical sections, and small modules built on trusted libraries. He estimates that agentic coding could reduce the cost of high-assurance software enough to make it broadly usable.
Zero bugs is already possible in high-assurance systems
Schleier-Smith says the Airbus A320 control software, developed in the 1980s, has had no serious incidents attributed to software problems. Its process combined diverse processors and operating systems, separate software teams, detailed specifications, independent verification, defensive programming, static memory allocation, and simple error handling. The Space Shuttle provides another example. Each of its last three software versions contained 420,000 lines of code and one error after inspection. Across 11 versions, there were 17 errors, and no Shuttle was lost because of a software problem. These results came from expensive engineering practices rather than ordinary commercial development.
Aerospace reliability comes from process as well as code
The A320 team treated software as a certified component that had to meet a specification, with zero defect tolerance. Schleier-Smith connects this approach to decades of experience in mission-critical mechanical engineering. The process included planning, requirements, integration testing with physical systems, external certification, and feedback between each stage. He argues that this matters for agentic coding because agents need to stay within a process that defines what they should produce and how their work will be checked. As software increasingly interacts with physical systems, integration testing becomes more important.
Abstraction and structure reduce the amount of complexity programmers must handle
High-level languages replaced much assembly-language work with machine-generated code and brought a reported 5x to 10x productivity gain. Their central idea is abstraction: programmers work with data structures relevant to the problem instead of machine memory locations. Structured programming then organized code around sequence, selection, and iteration, which enabled compositional reasoning and reduced the effects of spaghetti code. Schleier-Smith says hierarchical decomposition lets both programmers and language models focus on one part of a program at a time. Modularity adds another layer of control by allowing local reasoning as modules are combined.
Modularity helps people, LLMs, and formal verification tools check software without reasoning about the entire system at once. Schleier-Smith says composing modules can produce subexponential, perhaps even linear, scaling instead of exponential growth. Libraries are an important example because they can be tested and verified separately. He also argues that LLMs should generate high-level code rather than machine code because their context is limited, much like human working memory. Re-generating every library for each application would create a large testing and verification burden, so reliable components remain useful for agentic systems.
Formal verification can reject a bug before generated code runs
In a demonstration, Schleier-Smith uses the Dafny language to write a function that searches an array for a number. He adds assertions about the array length and the permitted return value, then runs the verifier. Dafny generates a Python library only after the assertions have been checked. When he changes the algorithm to introduce a bug, the verifier throws an error instead of allowing the faulty program to run. He also stresses that verification depends on the specification. If an important behavior is left out of the specification, the verifier cannot protect against that missing requirement.
Schleier-Smith names several examples of formal methods used beyond small research programs. The seL4 microkernel is a fully verified operating system used for embedded and security-critical applications. The CompCert C compiler has been verified so that the compiled result matches the intended C program behavior. Project Everest develops verified cryptographic libraries that protect internet traffic, and formal methods have been used for decades to check microprocessor designs. He says verification benchmark success rates have risen from roughly 30 percent to nearly 100 percent while benchmark runtimes have fallen by a factor of 50 or more.
Agentic coding needs separate checks for code, risks, and failures
For day-to-day agentic coding, Schleier-Smith recommends detailed specifications, typed languages, modular code, and small codebases. He adds practices that many developers may not use routinely: ask the LLM for explicit risk analysis and safety cases, which describe what could go wrong and how the code mitigates it. Separate teams in high-assurance engineering inspire separate prompts for writing code and testing it. Developers can also use different model providers for those tasks, apply formal proofs to critical sections, and move reusable behavior into libraries that are tested and validated separately.
Agentic coding changes both assurance problems and software costs
Schleier-Smith says software 3.0 treats prompts as programs, with LLMs directly solving tasks, generating code, using tools, or combining these behaviors. Because LLMs are nondeterministic and have a very large state space, existing verification methods do not directly cover this form of software. He also sees a possible benefit: LLMs can respond to unexpected inputs and may be used as fallback components when error conditions appear. In his coding example, a simple game cost about $2 to generate, with most of the cost coming from repeated input tokens and reasoning rather than output tokens. He compares this with much higher historical costs for high-assurance code and concludes that agents could eventually make it far cheaper.
"The key thing too is that there's a feedback process in refining each of these processes and making sure that it interfaces well with the steps that come before and after."10:59
Who should watch
You are using coding agents and need practical ways to check their output before it reaches production.
You build software that interacts with physical systems or handles failures where ordinary testing is not enough.
You want a concise history of structured programming, modularity, formal verification, and their relevance to LLM-generated code.
