AI Engineer Code 2025
Vision: Zero Bugs
Read the talk
Vision: Zero Bugs
High-assurance engineering already offers ways to prevent software defects. Coding agents could make those practices affordable far beyond aerospace and other critical systems.
From a talk by Johann Schleier-Smith
Before you start: Familiarity with functions, arrays, loops, and basic type checking is helpful; no prior formal-verification experience is required.
What would zero bugs change?
What would it mean for software to have literally zero bugs? Most people already experience something close to that impression: their phone camera, news, social media, and banking apps usually work. Engineers see the machinery behind that apparent reliability—on-call pagers, cloud outages, and the constant possibility of errors entering critical applications.
The disconnect becomes visible when an ordinary transaction goes wrong. Johann Schleier-Smith took his seven-year-old son to mini golf, where reservations were required and only one slot remained. He scanned the QR code and completed the booking process, only to be told someone else had taken the reservation. His son handled the disappointment remarkably well. About ten minutes later, a message revealed that the reservation had actually gone to them. They could play after all—but the software had already put them through an unnecessary emotional rollercoaster.
Schleier-Smith works at Temporal Technologies, which provides durable execution for applications running in the cloud. The connection is reliability and giving engineers time back for innovation; the zero-bugs vision extends beyond Temporal's current products. For product-specific material, he points to Cornelia Davis's Sunday workshop and Samuel Colvin's session on building agents with Temporal and Pydantic.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Three reasons to doubt the goal
The first objection is practical: perhaps existing reliability is good enough. Incidents happen, people recover, and an imperfect world can tolerate some imperfect software. Many systems already achieve strong reliability where it matters most. Eliminating every remaining defect may not improve people's lives enough to justify the effort.
The second objection is technical. Systems contain millions of lines of code, and agents can increase that volume rapidly. More fundamentally, a bug is a mismatch between behavior and an end user's expectations. The user does not care whether the cause was an ambiguous product specification or a missing null check. Control systems introduce another boundary: a self-driving vehicle may encounter physical conditions its designers never modeled. Verification also has theoretical limits, including problems that become computationally intractable.
The third objection is economic. A competitor that spends less on quality may ship sooner and win the market. A minor defect with an easy workaround may cost more to eliminate than it costs users to tolerate. Schleier-Smith adds a more cynical possibility: some businesses may benefit from selling support for buggy software. Taken together, these objections make zero bugs sound like a goal that loses to complexity, competition, and incentives.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Engineering software as a certified component
Aerospace provides a reason to take the goal seriously. The Airbus A320's control software, developed in the 1980s, is Schleier-Smith's first example of exceptional reliability. He describes its safety record as having no serious incidents attributed to software as of the talk. That broad historical assertion is his characterization; the more actionable lesson is the combination of safeguards used to pursue reliability.
The A320 approach he describes combines several forms of assurance:
- N-version programming: Different processors, operating systems, and implementation teams reduce dependence on a single implementation. His processor examples are Intel x86 and Motorola.
- Specification-based design: Extensive documentation supports analysis and provable statements about behavior across different scenarios.
- Independent verification: The people checking the implementation are separate from the people writing it.
- Defensive programming: Allocate memory statically rather than at runtime, and handle errors simply and explicitly instead of relying on sophisticated exception handling.
- Static analysis and verification: Examine the implementation for properties that should hold before it runs.
These techniques support a zero-defect-tolerance mindset: software is an engineered, certified component with a specification, much like a turbine fan blade.
The unit of reliability is still the whole aircraft. Software assurance must fit into protection against the many other things that can go wrong. Decades of experience with mission-critical mechanical systems offer lessons for software precisely because those disciplines treat reliability as a system property.
That makes quality through process relevant to agentic coding. Planning and requirements are familiar; external certification by a regulator or government may be less so. Integration testing is especially important when software must interact with physical equipment, a concern that grows as more software acts on the world. Feedback must improve each stage and the interfaces between stages. For an agent, such a process supplies structure for staying aligned with the intended behavior.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
High assurance can use different architectures
The Shuttle figures Schleier-Smith cites match Charles Fishman's 1996–1997 reporting in They Write the Right Stuff: one reported error in each of three 420,000-line versions, and 17 errors across eleven versions. These are the latest versions at that reporting period, not the final releases of the Shuttle program. Schleier-Smith also says that Shuttle losses were not caused by software.
Schleier-Smith estimates that the Shuttle figures represent roughly 1,000 times fewer bugs per line than typical commercial software. Curiosity supplies a different lesson: a costly mission with little opportunity for intervention on Mars still needs exceptional reliability, but its architecture need not duplicate the A320 approach. In his account, the rover's software, developed in the 2000s, used identical redundant systems and a commercial off-the-shelf real-time operating system rather than diverse implementations and a custom operating system.
Chemical plants, automobiles, medical systems, nuclear power, and security systems offer further sources of high-assurance practice. The shared objective is dependable behavior under consequential conditions; the engineering choices can evolve with the application and available components.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Make the program easier to reason about
The foundations of reliable software are also the foundations of ordinary software development. High-level languages emerged in the 1950s and 1960s, and assembly became less common as an application programming language through the 1980s. Machines increasingly generated machine code for other machines. Schleier-Smith attributes a roughly 5–10× productivity gain to the historical move to high-level languages.
The mechanism is abstraction. A programmer can work with data structures meaningful to the problem instead of manipulating memory locations directly. Preserve essential complexity and remove implementation complexity: the program must still express the business or physical problem, but it need not continually expose registers, memory layout, memory access, or machine-specific performance details. Structured programming supplies the corresponding abstraction for control flow.
Edsger Dijkstra's advocacy in the 1960s, followed by broader adoption in the 1970s, helped establish sequence, selection, and iteration as the basic building blocks of programs. Statements execute in order; if/else selects a branch; loops repeat work. Compared with arbitrary GOTO jumps through a flowchart, these structures support compositional reasoning: understand a piece, then understand how it combines with the surrounding pieces.
Structured programming does not make spaghetti code impossible. Schleier-Smith's invitation to try reading older Fortran is a reminder of how different unrestricted control flow can feel. The gain comes from hierarchical decomposition, which lets a programmer focus on one part at a time. That is just as useful when an LLM generates the code.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Libraries still matter when code is cheap
David Parnas's work on modularity in the 1970s extends the same idea to system structure. Modularity is associated with object-oriented programming, but libraries provide it without requiring objects. A module gives a human reviewer, an LLM, or a formal verification tool a smaller unit to understand. Schleier-Smith describes the intended benefit as replacing exponential verification complexity with sub-exponential, potentially linear work through local reasoning. Achieving that benefit depends on being able to reason about the module boundaries and their composition.
Why, then, should an LLM generate a high-level language instead of machine code? Context remains scarce. An LLM may have a larger explicit context window than a person's working memory, while people carry substantial compressed background knowledge. Both still benefit from representations that concentrate attention on the relevant problem.
Cheap generation does not remove the case for libraries. Having an agent rewrite a library for one application may save little once that new implementation must be tested and verified. Trusted, separately validated components let the application inherit useful work instead of repeatedly rebuilding its assurance. Temporal's durable execution is Schleier-Smith's example: it moves responsibility for aspects of cloud reliability into a separate component, reducing what application code must handle itself.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Prove an array search before running it
Dafny brings specifications and proofs into the programming language itself, and can generate code for targets including JavaScript, Python, and C#. Its verifier uses theorem-proving machinery to establish that an implementation satisfies its stated properties. The demonstration starts with an index-of method: search an array for a number and return an index. The stated conditions include a nonempty array and a result that is either -1 for absence or an index below the array's length.
A compact Dafny implementation of that search makes the contract concrete. requires constrains the input; ensures describes the result; loop invariants record what remains true as the search advances.
dafny
method IndexOf(a: array<int>, target: int) returns (r: int)
requires a.Length > 0
ensures -1 <= r < a.Length
ensures r >= 0 ==> a[r] == target
ensures r == -1 ==> forall k :: 0 <= k < a.Length ==> a[k] != target
{
var i := 0;
while i < a.Length
invariant 0 <= i <= a.Length
invariant forall k :: 0 <= k < i ==> a[k] != target
decreases a.Length - i
{
if a[i] == target {
return i;
}
i := i + 1;
}
return -1;
}
For a teaching input of [4, 9, 2] and target 9, the search passes over 4 and returns index 1. The prefix invariant explains why returning -1 after exhausting the array is valid: every earlier element has already been shown unequal to the target. The decreases clause supplies a termination measure.
The recorded sequence then exercises the verification boundary:
- Run the Dafny verifier on the search implementation.
- Generate and exercise a Python program using the functionality; verification occurs before execution in the demonstrated workflow.
- Introduce a small algorithm change that creates a bug.
- Try again and receive a verifier error.
Generating a Python library makes the verified component usable from an ordinary application. The intentional mutation shows how a failed proof obligation can stop a defective implementation before that workflow runs it.
Verification is only as good as the specification. The illustrative contract above requires a matching index, but does not explicitly require the first matching index. That distinction matters if callers expect first-occurrence behavior. A proof establishes the properties that were written down; an omitted user requirement remains an opportunity for a bug.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
From verified components to verification tools
Formal methods already support deployed systems. The seL4 microkernel is a verified operating-system kernel used in embedded and security-critical settings. Its guarantees concern the kernel and particular properties under explicit assumptions, including hardware and boot-related assumptions; they do not automatically verify every application in a deployed system. CompCert provides a compiler example: its central assurance is that compilation preserves the behavior specified by the source C program. Schleier-Smith points to security-critical and aviation applications.
Project Everest applies formal methods to cryptographic and communication components, including libraries deployed to protect internet traffic. Microprocessor design has also used formal verification for decades, driven by the high cost of incorrect hardware. These examples put verification at reusable boundaries—kernels, compilers, cryptography, and processors—where an assurance investment can benefit many downstream systems.
Schleier-Smith reports benchmark success rising from roughly 30% to nearly 100%, with runtime falling by at least 50× over roughly two decades. The talk does not identify the benchmark suite, solver versions, hardware, or task distribution, so those figures describe the progress he presents rather than a general performance guarantee. The broader mechanism is that benchmarks concentrate research effort on shared, measurable problems.
The techniques differ in what they check and how closely a proof is tied to an implementation:
| Technique | Relationship to the program |
|---|---|
| Type systems and static verification | Check properties without running the program |
| Dafny and SPARK | Couple specifications and proofs closely to code |
| Coq and Lean | Support theorem proving; implementation correspondence needs attention |
| Model checking | Proves properties of a finite-state model |
Ordinary type checking is already a basic form of static verification, and richer checks can build on it. With separately expressed proofs, the crucial obligation is showing that the proved object corresponds to the code actually used. Theorem proving can reason beyond the finite-state formulation described here for model checking.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Apply assurance where the agent struggles
These practices can be useful on a specific troublesome piece of agent-generated code without imposing an aerospace process on an entire codebase. Start with detailed specifications, typed languages, and modular implementations. Then ask the model for explicit risk analysis and safety cases: what could go wrong, and what in the implementation mitigates each failure? This is qualitative reasoning, distinct from a mathematical proof, but it makes assumptions and failure handling available for inspection.
Independent verification suggests a practical division of labor. Use separate prompts for implementation and testing; for greater diversity, use different foundation-model providers for the two tasks. Add formal proofs around critical sections where the properties can be stated precisely. Keep the application small by relying on libraries that can be developed, tested, and validated separately. Each intervention reduces the amount of unchecked reasoning concentrated in one generated implementation.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
When the prompt itself becomes the program
Andrej Karpathy's Software 3.0 framing treats prompts as programs. An LLM might answer directly, generate code, run a loop with tools, or combine those behaviors. In that setting, the behavior being assured includes the model's own responses, not just a conventional program it emitted. Schleier-Smith argues that nondeterminism and an enormous state space prevent the verification techniques discussed so far from carrying over directly to this form of software.
The same flexibility creates a possible new form of resilience. LLMs can interpret ambiguity and respond to inputs that were not anticipated explicitly. An architecture might use agents throughout, or invoke an LLM only after a specific error condition arises. Such a system could potentially recover from cases that a rigid implementation cannot handle. That is an architectural opportunity to investigate, rather than a demonstrated guarantee of recovery.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
The cost is mostly outside the returned code
A small generated game makes the economics concrete. Schleier-Smith spent about two minutes prompting and excluded his own time from the cost calculation. The model was GPT-5-Codex. He reports 600,000 input tokens, 3.5 million cached input tokens, 48,000 reasoning tokens, and 28,000 returned tokens for the game.
Schleier-Smith reports about $2 to generate the game, with visible returned tokens accounting for about 15% of the total cost, excluding his time. The remainder went toward repeated inputs as the agent tested its work and toward reasoning. Here, “returned” distinguishes visible output from reasoning; in API billing, reasoning tokens also count as output tokens. The useful comparison with human development is that typing the final code occupies only a small portion of the work required to build the software.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Can cheap generation pay for expensive assurance?
Schleier-Smith's cost comparison starts with high-assurance development and works down toward cheaper conventional development. These are his illustrative estimates, not a normalized comparison of projects with equivalent requirements:
| Development category | Cited cost per line |
|---|---|
| Shuttle software, 1990 estimate | About $1,000 |
| Same estimate in 2025 dollars | About $2,500 |
| Some security high-assurance software | Up to $3,000 |
| Typical production software, without AI | $10–$100 |
| Low-cost contractors, without AI | $1–$10 |
The large premium buys more than writing code: high-assurance development includes the work needed to establish confidence in its behavior.
Agentic generation spans cheap models producing code with little iteration through expensive models doing substantially more work. Excluding people costs, Schleier-Smith estimates agentic generation to be at least 1,000×, and probably about 10,000×, cheaper than typical software development. He places the high-assurance premium over typical software at about 100×. These rough ratios motivate the economic argument: generation savings might be large enough to fund much more assurance work.
Schleier-Smith extrapolates that agent-produced high-assurance software could become 100× cheaper than typical software is produced today. This is a forecast from the cost ratios, not a measured result from an assurance-oriented agent. Its premise is that agents can apply the expensive verification, process, and testing practices while retaining enough of their generation-cost advantage.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Fewer defects could unlock adoption
The zero-bugs vision depends on directing agents toward assurance, not merely asking them to produce more code. Schleier-Smith characterizes reliability as a solved problem in aerospace and other critical industries, and proposes agents organized around formal methods, extensive processes, and adversarial testing. The intended result is a proliferation of experiences in which users simply do not encounter defects.
This also addresses a reason developers resist coding agents: repairing the generated implementation may take longer than writing it correctly themselves. Lower defect rates can change the adoption calculation. If agents routinely produce fewer defects than human-written code, Schleier-Smith expects adoption to accelerate sharply. The assurance knowledge already exists; the opportunity is to make applying it economically routine.
The closing image is resilience with a sense of humor. Ziggy, Temporal's mascot, is a tardigrade—a member of the phylum Tardigrada, not an insect and therefore not a bug. Tardigrades can survive extraordinary conditions, including exposure to space; Schleier-Smith says Temporal took Ziggy to space earlier that year. He closes by returning to durable execution as a reliable foundation for modern software and inviting people interested in these ideas to explore working together.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Resources
From the talk
Installation options and documentation for the programming and verification language used in the array-search demonstration.
An overview of the kernel's mathematical guarantees and the assumptions on which they depend.
Verified communication and cryptography components, their proof techniques, deployment examples and source projects.
Model capabilities and token pricing for the coding model named in the game's cost example.
Further reading
- They Write the Right StuffArticle
Charles Fishman's December 1996/January 1997 reporting on the Shuttle software team's defect counts and engineering practices.
- Reasoning-token accountingDocumentation
Explains how reasoning tokens consume context and contribute to billed output usage.
Read the complete timestamped transcript
- 0:00
Please join me in envisioning a world where software has zero bugs. Not just a few bugs, but actually literally zero bugs. Okay, okay. Just bear with me now. So for most people, let's just say people who aren't software engineers, bugs are actually just not a very big part of their life, period.
- 0:24
Most of the apps that we use on our phones, our social media, our news, that stuff pretty much works most of the time. The camera works most of the time.
- 0:33
Any of those most popular apps, banking, they work really well most of the time. So bugs are really not top of mind for most people.
- 0:45
Now, anybody who makes software is very familiar with a different world, a world of constant stress about the possibility of software errors creeping into critical applications, on-call, uh, responses to pagers, cloud provider outages.
- 1:09
The list goes on and on. So there's a disconnect between what most people are experiencing every day in the world and the reality of making software. Now, I will say that even for those of us who are not engineers, the perils of broken software do crop up from
- 1:34
time to time. Just yesterday, I took my [REDACTED:age] son to the mini golf place, and there was just one reservation left. Reservations were required. And I dutifully whipped out my smartphone,
- 1:53
snapped the QR code, went through the process to grab the last reservation spot, only to be told that it had been grabbed by somebody else.
- 2:08
Well, I gotta say, I was very proud of my son because most kids, most of the time, would have probably melted, and he actually didn't. He handled it great.
- 2:17
And then can you imagine my surprise when I checked my messages about ten minutes later to find out that, in fact, that last reservation slot had gone to us.
- 2:32
So we were thrilled. That rollercoaster journey still reinforces the fact that bugs are real in the world, and they have real impact on real people every day, even if it is just a momentary emotional swing for a [REDACTED:age].
- 2:48
I'm Johann Schleier-Smith, and today I'm going to be talking to you about a vision of zero bugs. Now, I work at Temporal Technologies. Temporal makes software for durable execution.
- 3:00
It makes software that deploys to the cloud do what it's supposed to do. But this talk is not going to be about Temporal. There are several other talks at the AI Engineer Summit that do talk about Temporal.
- 3:14
My colleague Cornelia Davis will be doing a workshop on Sunday. In addition, Samuel Colvin from Pydantic will be talking about building agents that combine Temporal with Pydantic. The push to build reliable software and the vision of giving engineers time back for innovation is tightly aligned with our products at Temporal.
- 3:39
However, everything in this presentation is going to be outside of the scope of our current products. Let's return to the vision of zero bugs.
- 3:49
There are quite a few objections, really reasonable objections, to this vision. So let's talk through them. First of all, as we've started out saying, incidents happen. Incidents happen whether it's because of cloud outages or problems with orders.
- 4:08
They happen, and generally speaking, we pick ourselves up and get through them. More broadly, the world is imperfect, and so a few software bugs here and there might be okay.
- 4:19
And in fact, we already are solving for reliability pretty well in many of the situations where it matters. So maybe software is good enough. Maybe we don't need to push towards a z- vision of zero bugs.
- 4:35
Here's another objection. You could give perhaps good reasons, good theoretical reasons even, why eliminating all of the bugs is just simply impossible, why it's a preposterous idea. So you could say there are millions of lines of code.
- 4:50
The code is just too big. We have too much code. As we know, as agents generate more and more code, that exacerbates the problem, and it's all just simply too complicated.
- 5:02
Furthermore, if we look at the definition of a bug, it seems that the specifications unavoidably have some degree of ambiguity. I would say that it's a bug whenever the way the program works does not match the end user's expectations.
- 5:20
They don't care whether it was a problem with the product specification or whether the programmer forgot to check for a null. It just doesn't matter, right? And furthermore, unexpected things happen in the real world.
- 5:33
If we think about control systems, for example, if there is some aspect of the world that hasn't been modeled correctly, you could see this frequently, for example, in the fears around the capabilities of self-driving vehicles, then that, you could say, just simply can't be handled.
- 5:54
It's hopeless. Furthermore, we're gonna talk about some of the powerful techniques in software verification, but we also know and we can prove theoretically that those have limits. There are problems that are computationally intractable in some cases.
- 6:11
Reason number three is economics. If you have competitors who don't care much about software quality and who will win in the marketplace if you spend time on it, then that reliable software may never see the light of day.
- 6:25
Also, you might just say that the ROI just simply isn't there for fixing every single bug. Some of them maybe are just not so bad. Maybe they have easy workarounds.
- 6:36
And finally, perhaps cynically, some people think that there are companies that are okay with shipping buggy software because it helps them sell support.
- 6:49
In this vision, this cynical and sad vision of the world, the bugs win,
- 6:56
and we'll never have bug-free software, not even close.
- 7:01
Now, I contend that there is hope. And if we look, there are practices,
- 7:11
a whole slew of techniques that really allow very reliable software. Let's look at this example, which is the Airbus A320. The control software for this airplane was developed in the 1980s and has been held up as a showcase for reliability.
- 7:35
There are, in fact, to this date, no serious incidents with Airbus A320 aircraft that have been attributed to problems with the software.
- 7:47
So what is their approach? There are a bunch of ideas here that are really pretty neat. So one of them is N-version programming. So the most critical elements of the Airbus control system were actually built with different processors, say one from x86 from Intel, one Motorola
- 8:11
processor, different operating systems on that, separate teams writing the software, providing a tremendous level of redundancy against unexpected issues. They also use something called specification-based design. Tremendous amounts of documentation, but also documentation that could be analyzed in order to understand and make provable
- 8:36
guarantees about the behavior of the system and what the software would do under a whole variety of scenarios. They use independent verification teams, where the people writing the code and the people checking to make sure that the code had the desired behavior were completely separate teams.
- 8:54
They also used a slew of defensive programming techniques. So for example, not allocating any memory at runtime. That's all done statically. Not having sophisticated exception handling, just keeping it really simple, very explicit in the code, how any error conditions are handled.
- 9:12
And finally, static analysis and verification. We'll talk about those techniques more in just a few minutes. So the mindset here is also really important. The Airbus engineering team had this idea of zero defect tolerance, of thinking of software as a certified component that was engineered to meet a certain specification, just like a turbine fan blade might be.
- 9:37
And they also had a system-level approach to reliability, because when you think about it, with an airplane, there are all sorts of things that could go wrong that need to be protected against.
- 9:48
It stands to reason that the decades of experience engineering mission-critical mechanical systems crossed over into the software development process, and there's a lot that we can learn from that.
- 10:04
So core to the A320 was quality through process. Now, I know for folks who are banging out code, process is oftentimes the last thing that they wanna think about.
- 10:17
But as we're thinking about how agentic coding works, thinking about how we keep agents on the rails and doing what we want them to do, process really is something that we do want to think about.
- 10:28
There are quite a few steps to the quality process. Many of these are familiar to people who are writing software today, say, planning and requirements, but there are also some others that are a little bit different, like certification by an external agency, maybe a regulator or the government.
- 10:47
The integration testing becomes particularly important for an airplane where that software needs to interact with the physical system. And as we look ahead and think about where things are going in terms of the software that we are going to have in the future, that's interfacing more and more with the physical world.
- 11:06
So this is something that is probably going to come back.
- 11:09
And 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.
- 11:23
The aerospace industry is particularly rich in these examples of super, super reliable software being built. So the space shuttle is one, and, and really it's quite stunning. So in the last three versions of that software, four hundred and twenty thousand lines of code in each of those, and the result of that after sort of inspecting was, was
- 11:44
one error per version. Sadly, some of the space shuttles have been lost, but space shuttles have never been lost to software problems. Over the last 11 versions, there were a total of 17 errors.
- 11:58
And so this is probably a thousand times fewer bugs, um, per line of code than is typical in commercial software. Another aerospace example is the Curiosity rover. With a mission that costs millions and with very little ability to intervene once the system is on Mars, it was critical to have a high level of reliability.
- 12:23
Now, that said, this software, developed in the 2000s, did take a bit of a different approach that sh-- really shows the evolution of reliable systems. So for example, while redundant systems were used, they're actually identical systems and a commercial off-the-shelf real-time operating system was used rather than a custom operating system.
- 12:44
Now, aerospace isn't the only industry where high assurance software, high quality software, software with effectively zero bugs, has been critical. So whether it's in the chemical industry or the automotive industry, medical software, nuclear power industry, or security systems, each of these provides us with an opportunity to learn something.
- 13:11
Let's take a moment to shift gears a little bit. Let's look at the advances in computer science that really set the foundation for how reliable software is built today.
- 13:23
And in fact, as we look at these, we'll find that they really are the foundation for really all software that's built today.
- 13:33
The biggest of these is high-level languages. Here we go back to the 1950s, 1960s and from that period
- 13:44
where people were mostly writing with assembly language up through the 1980s when really assembly language more or less went out of favor as a language that people would use.
- 13:57
It was a l- language that, that was replaced by machine code generated by machines for machines. There was about a five to 10X productivity gain. [lip smack]
- 14:09
And the core idea with high-level languages is around abstraction. It's around data abstraction so that instead of poking at memory locations, you work with data structures that have some relevance in the problem domain, and it's about structured programming, which we'll talk about in a minute.
- 14:32
At the end of the day though, what is sort of a unifying concept here is preserving the essential complexity, which is those aspects of the problem that are directly relevant to whatever it is that the software is supposed to do.
- 14:50
And removing as much as possible from the code those aspects of the problem that have something to do with the implementation, that have something to do with the machine underlying that runs the code, like what its registers are or how you lay out or access the memory, or even many aspects of the performance of that machine.
- 15:11
Structured programming as espoused by Edsger Dijkstra was one of the really big advances coming in the 1960s and being broadly accepted in the 1970s. Today, programmers can be excused for having forgotten about the debates about whether GOTO statements were a useful programming tool or
- 15:36
something that should be avoided at all costs. Our programming language that we use today clearly don't have GOTO statements.
- 15:45
What is structured programming all about? It's really quite simple. You have a set of basic control structures. So these are things like sequences, statements that come one after the other, um, selection, if-then-else, iteration, concepts that are completely familiar to any programmer today.
- 16:01
But what's really important about structured programming versus what came before, where people were modeling applications in terms of flow charts and having these non-structured concepts like GOTOs where you could really jump around throughout a program, was enabling this sort of compositional reasoning and eliminating spaghetti code in many cases.
- 16:23
You could still write spaghetti code, of course, with structured programs, but if you look at Fortran code and if you try to understand that, go for it, it's a fun time, you'll find that, uh, it's, uh, really very different.
- 16:34
So this hierarchical decomposition of programs, it really mitigates complexity. It allows programmers to focus on one piece of the code at a time. When you have LLMs generating the code, this is just as valuable as it was for the programmers who were writing code decades ago.
- 16:53
Another key idea that traces back to the 1970s is David Parnas's push to think about software systems in terms of modules. What does modularity mean?
- 17:09
It's perhaps best known in the context of object-oriented programming, but it applies in a whole bunch of situations.
- 17:16
It's perhaps best known as an aspect of object-oriented programming, but you can have modularity without object-oriented programming. Libraries are one of the obvious examples. And so when we think about verifying a program, when we think about making sure that that program does what it's supposed to do, whether we're verifying it as a person or as an LLM
- 17:38
or using some sort of formal verification technique, modularity is a massive boost. As you chain modules together, you get a sub-exponential scaling, perhaps even a linear scaling rather than an exponential scaling where you can apply local reasoning at every level. [lip smack]
- 17:57
And the upshot of that is that you have manageable complexity regardless of the size of the system. You take that spaghetti and you turn it into something that is very nicely organized.
- 18:09
I wanna take a moment here to reflect on why LLMs are not simply generating machine code rather than high-level language code. It's certainly a reasonable question, and I think that the reasons that applied to human programmers decades ago are just as applicable to LLMs today.
- 18:28
So for one thing, we know that context is limited. The context for an LLM, the context window might be a lot larger than what a human is able to hold in their head.
- 18:39
It depends a little bit on how you count that context. Certainly, we have a lot of awareness of background facts that we've sort of compressed into our brain. Um, but, uh, uh, context is definitely a scarce resource for LLMs, just like attention and ability to reason, perhaps call it working memory, is a scarce resource for people.
- 19:04
The argument for libraries is as strong today as it ever was. So while you could make the argument, "Oh, why don't we just let the AI generate all the code for the libraries since it's fast and cheap, maybe we can customize it to the needs of our specific application,"
- 19:21
getting that code properly tested, properly verified is going to be a huge challenge. And so we really want the ability to use reliable, trusted components and modules to build our systems.
- 19:36
On that note, I do need to put in a little pitch for Temporal. What Temporal allows you to do is it allows you to abstract away the reliability of your software in the cloud.
- 19:48
It provides durable execution, which means that it's shipping that reliability problem to a separate piece of code that's outside of your application that your application doesn't need to worry about.
- 19:59
Let's now go ahead and dive in on the fun part, which is formal methods, and I wanna shoot straight to a few demos. Now, in these demos, I'm going to be using the Dafny language.
- 20:11
What Dafny allows you to do is it allows you to use a custom programming language that generates output to a whole variety of other languages, whether it's JavaScript, Python, um, or C#, you name it.
- 20:25
What Dafny allows you to do is it allows you to put proofs in line with your code,
- 20:32
allowing theorem-proving software to come along and verify that that code does exactly what you said you want it to do. Okay, so I have a program here that is written in the Dafny language, and it has one function.
- 20:49
It's called a method here, and it does something very simple. So it does index up. So what it's going to do is it's going to search an array to find the index of a particular number.
- 20:59
And I can write a number of assertions about this. The array length is greater than zero. The number returned in that result is either negative one if it's not found or the, uh, some number that is less than the length of the array, and so forth.
- 21:18
What I can now do is I can just go ahead, and I can run the Dafny verifier on that program.
- 21:27
Great. No bugs. Let's go ahead and generate a Python program that exercises this functionality, and we can see that the program first verifies before it runs.
- 21:43
So I know that all of those assertions that are proven about the program have been checked before that program runs. This is an extremely powerful technique. Because it spits out a Python library, it's something that can be integrated into your code.
- 22:00
Now, suppose I come over here and I make a small change to the algorithm, which is to say I've introduced a bug.
- 22:09
If I now go back and I try to run that again, the verifier steps in and throws an error, and we are saved from seeing that bug.
- 22:23
All right, let's return to the presentation here. So one thing to keep in mind is that verification is only as good as the specification. If I leave out anything that needs to be checked, that creates an opportunity for bugs.
- 22:34
So I wanna emphasize that in the last few decades, formal methods have become commercially relevant on a really impressive scale. For example, the SeL4 microkernel is a fully verified operating system.
- 22:50
It's a simple operating system typically used for embedded systems and security critical applications, but it is an operating system. The CompCert C compiler, again, often used in security critical applications as well as in the aviation industry.
- 23:06
That is a fully verified compiler. That is to say that formal methods have been used to ensure that the code that that compiler emits given a C program does exactly what that C program is supposed to do.
- 23:22
Project Everest works on libraries for cryptography, including libraries that are widely deployed today protecting internet traffic. And really impressively in the microprocessor space now for several decades, formal methods have been used to ensure the correctness of those designs.
- 23:43
There has been just a huge motivation to make sure that these systems are performing as expected. And one of the things that's really, really cool is that there has been just tremendous progress in terms of the size and speed with which verification can be performed over the last sort of 20 plus years.
- 24:06
And this really coincides with the rise of benchmarks. Benchmarks can have a tremendous role in shaping an industry. It gives folks something to focus on. And so we can see that success rates for the benchmarks have gone from the 30%-ish range up to nearly 100%, while at the same time the runtime on those benchmarks has
- 24:31
gone down by a factor of 50 or more. So there are a handful of verification tools that you can use today, and I want to break them down in a few different categories.
- 24:40
So static verification is probably that which you are most familiar with. I'm starting from the bottom here. If you are using type systems, that is a simple form of static verification, but there are ways to attach more checks to the type system.
- 24:57
Jumping up to the top, we just saw Daphne run Spark. It is another example of tight coupling between those theorems and the code. And then there are other systems that are also well known, Coq and Lean, for example, that provide theorem proving separate from the code.
- 25:16
The problem there, while those tools are super, super powerful, is that you do need to make sure that what the code does and what you have written in terms of the proof are the same thing.
- 25:29
Model checking deals with finite state machines and proving properties about those finite state machines. Theorem proving, on the other hand, doesn't have that limitation because it is able to take advantage of more powerful reasoning techniques,
- 25:46
automated reasoning techniques. All right, let's get to the good stuff, agentic coding. Now, I wanted to give you a set of really practical things
- 26:05
that you can try in your day-to-day work to see what sorts of benefits you can get. These are probably not things that you're going to apply across the code base, but when you're struggling to get the agent to do what you want it to do on a very specific piece of code, these could all be pretty valuable.
- 26:23
So some of these are things that we are probably reasonably well-versed with, so detailed specifications, using type languages, doing modular code. These are all sort of things that we pretty much do anyway.
- 26:36
But some things that we might not do are interacting with the LLM and asking it to do explicit risk analysis, asking it to write safety cases, which are statements about things that could go wrong and how that thing that could go wrong is being mitigated in the code.
- 26:56
So this is separate from formal methods. This is sort of a, um, more qualitative reasoning, which is something that we know that LLMs can do. Another inspiration that you can take is from the design of high assurance systems where they have separate teams do the coding and the verification.
- 27:17
That means that you can have separate prompts to the LLM for testing versus for
- 27:27
writing the code in the first place. And if you want to take that to another level, you can use multiple model providers. So you can use one foundation model for the tests and one foundation model to write the code.
- 27:38
You can bring in those formal methods techniques to give proofs around sections of critical code. And lastly, this is sort of the timeless advice, keeping your code small, outsourcing those things that can be to libraries which can be separately tested, validated, developed, and now your code doesn't need to worry
- 28:03
about it. All right, let's talk for a minute about Software 3.0. So this is the idea promoted by Andrej Karpathy that prompts can really function as programs, that what we're doing today is we are programming through AI, through LLMs.
- 28:28
And it's a new world of coding, whether that means that the LLM directly solves whatever problem you need solved or whether it generates code or perhaps loops and uses tools or any combination thereof in order to get to whatever behavior you want for the system.
- 28:46
This opens up a tremendous need for new assurance techniques, right? Because LLMs are fundamentally non-deterministic and because the state space is absolutely huge, all of the verification techniques that we have discussed have basically no bearing on this form of software.
- 29:10
That said, it's not all gloom and doom, and I am really excited by the idea that despite having new and different failure modes, there are also potentially new forms of resilience.
- 29:25
LLMs can respond to unanticipated inputs. They have that ability to deal with ambiguity, and you can imagine lots of architectures, whether they are pure agentic architectures as we often have today, to ones that maybe invoke LLMs once certain error conditions are encountered, that are actually getting ahead of
- 29:50
and protecting the world from all kinds of software faults and perhaps doing it in really simple and interesting ways. So I think this is just a tremendously interesting idea.
- 30:01
All right, let's get to cost. This is one of the big topics. So what does agentic code cost? I vibe coded up this very simple game. I spent about two minutes prompting.
- 30:17
We can set that aside. I'm going to not count my time towards the cost. GPT-5 Codex, it's co- creating 600,000 input tokens And it has three point five million cached input tokens, forty-eight thousand reasoning tokens, and then is returning twenty-eight thousand tokens.
- 30:34
The cost to generate this game was about two dollars. And the thing that's interesting here is that the cost to generate the output tokens
- 30:44
is only about fifteen percent of the overall cost, the rest of which is going into the repeated use of input tokens as tests are being run and the reasoning tokens as well.
- 30:59
As it-- with human written code, the amount of time that you spend actually writing the code is a small fraction of the overall time that's spent to build the software.
- 31:13
All right, so let's bring it down, and let's look at the cost of code. So for high assurance code, if we look at something like the space shuttle or the Airbus example, the numbers there, if you take nineteen ninety from the space shuttle, it was about a thousand dollars per line of code.
- 31:29
If you translate that into twenty twenty-five dollars, it's probably more like twenty-five hundred dollars. And in some cases, so for example, for security, high assurance software numbers as high as three thousand dollars per line of code have been quoted.
- 31:43
For typical software development, it's more like ten to a hundred dollars for real production software, but nothing that is developed with the high assurance techniques. And in some cases, so for example, for security, high assurance software numbers as high as three thousand dollars per line of code have been quoted.
- 32:03
If you have low-cost contractors, you may be able to bring that number down as low as one to ten dollars. This is all without considering any AI or agentic codegen.
- 32:15
For the agentic coding, I've put a pretty broad range that includes just cheap models spitting out code. It could probably go even lower than this if they're not iterating on it very much, up to more expensive models that are working harder to generate that code.
- 32:36
Regardless of how you slice the numbers, you're looking at a factor of at least a thousand, probably about ten thousand. If you set aside the cost of the people involved in the agentic coding, if you just look at that agentic coding piece, that code is being generated far more cheaply than typical software.
- 32:59
And this is interesting because the gap between the cost of high assurance code and typical software is only about a hundred X.
- 33:10
So if we extrapolate, we could conclude that agentic coding has the potential to produce high assurance software one hundred times more cheaply than typical software is produced today.
- 33:34
That leads us to the vision of zero bugs.
- 33:38
Software reliability is a solved problem. It's solved in aerospace, it's solved in other critical industries.
- 33:46
And with the deployment of agents geared towards achieving high assurance code, whether that's because they're using formal methods, because they have extensive processes, because they're using adversarial testing, the list goes on and on.
- 33:59
We can believe that agents will make high assurance code one hundred times cheaper. And that in this context, we will see a proliferation of bug-free experiences. I also want to emphasize that this push towards a vision of zero bugs serves to address many of the limitations that agentic coding have today, notably around the quality
- 34:24
of the software that's written. When developers choose not to use the agentic coding tools that are at their disposal, the reason for doing so typically is that it's just going to take them more time to fix the bugs in that software than it would to take them to write the software correctly in the first place.
- 34:42
As soon as we can get to the point where agentic coding is routinely generating software that has fewer defects than software written by humans, we can expect absolute takeoff in its adoption.
- 34:59
We know how to do that. We've known how to do that for decades.
- 35:07
Before we close, I want to emphasize that tardigrades are not bugs.
- 35:15
This is Ziggy. Ziggy is Temporal's mascot, and Ziggy belongs to the phylum Tardigrada,
- 35:25
not an insect. Tardigrades are some of the most resilient animals in the world. They have even been known to survive in outer space. And earlier this year, we actually took Ziggy to space just to prove that point.
- 35:43
We are having a lot of fun here at Temporal building durable execution as the reliable foundation for modern software. If anything that we discussed here today resonates with you, please reach out.
- 35:56
We'd love to chat and explore how to work together in any possible way.