Breaking software bottlenecks
What if flawless software could be developed easily, quickly, and at scale?
Our civilization and future increasingly depend on software, and understanding the potential for future software development is critical to understanding prospects for the world as a whole. As usual, AI will play a pivotal role.
Exploiting expanded physical capabilities — general implementation capacity — will require a corresponding expansion in our ability to create software. While it's tempting to assume that advanced AI will simply develop whatever we need, this is simplistic. How can we specify what the software should do? How can we ensure that AI-developed software performs as intended, without vulnerabilities, and with sufficient reliability for critical applications, even in the face of sophisticated cyberattacks? Answering these questions requires a closer examination of how AI capabilities align with key challenges in software development.
Today, software development is often a bottleneck: It's a slow, expensive process that frequently yields unreliable or insecure products that don’t align with actual needs. Post-delivery, the difficulty of modifying and debugging software hinders adaptation to new requirements. Achieving security against human hackers — let alone AI — seems improbable. Redesigning flawed infrastructure appears out of reach.
Projecting these problems into the future blocks serious consideration of possibilities for swift deployment of complex, novel, critical systems. This, in turn, blocks consideration of crucial options (both military and economic) that could promote better alignment among competing actors.
Let's explore the possibilities by breaking down the software implementation problem into components that align with emerging AI capabilities.
Scaling speed, quantity, and quality
The most obvious application of AI in software development is to have AI write the code. We're already seeing AI-powered assistants for programmers, which can quickly and cheaply generate code that is untrustworthy, yet can boost programmer productivity. (And Claude Sonnet 3.5 has generated a fresh wave of excitement.)
Paths forward in automating software development may include AI models that surpass human capabilities in writing, critiquing, testing, and debugging code. This unitary, generalist AI approach may seem dated, however; a more realistic path would rely on frameworks that orchestrate AI workflows, using different models (or different prompting, knowledge, or fine-tuning) for specific tasks.
To unpack this further, the natural approach would rely on a large, generalist language model (LLM), trained on both code and discussions of software functionality, capable of understanding human intent, asking clarifying questions, and providing effective prompts to downstream models fine-tuned for tasks in code development. Picture an iterative process with progress reports, unit tests, stringent quality checks, and feedback loops that incorporate user input. Most of the intermediate results would be produced by AI, for AI.
This role architecture outlines an implementation workflow spanning design, development, production, deployment, and adaptation (though “production” may simply mean downloading). In systems combining code and hardware, physical and software implementation workflows would intertwine.
The problem, however, is that human-level software is inadequate, because human-written software is often buggy, vulnerable, or even malicious (consider supply chain attacks). Just automating standard development workflows wouldn’t guarantee reliability and trustworthiness. This calls for something more.
Applying formal methods at scale
Formal methods are mathematically rigorous techniques used to specify, develop, and verify software, ensuring it performs correctly.1 They provide software products paired with machine-checkable proofs of correctness, which can eliminate bugs and guarantee reliability — provided that the specifications themselves are correct and the hardware meets its own specifications, which is a topic in itself.2
Formal methods have been applied to develop systems as complex as compilers and operating systems, but their adoption has been limited by the scarcity of expertise and the cost of manual proof development. Current efforts focus on improving automated theorem-provers and incorporating them into development environments.3
Advanced AI systems are on a path toward automatically generating and verifying code from high-level specifications, augmenting and gradually replacing human effort. Note that there is a hard-edged criterion for success: the code corresponds to the proof by construction, and the proof must be accepted by the proof-checker (a simple, deterministic algorithm).
Because success has precise criteria, learning to code using formal methods can be formulated as a reinforcement learning task (like winning a game of Go) with unlimited backtracking. Poor choices along the way don't cause errors; they merely increase search costs, which decrease as strategies improve. Meanwhile, successful code-and-proof pairs provide gold-standard data for training better models.
And because proof-checkers are small and simple, there’s no need to trust opaque software or the AI systems themselves.
Breaking the Specification Bottleneck
A major challenge in applying formal methods is the bottleneck in developing accurate specifications. However, some tasks are already well-specified, others can be addressed by learning from data, and AI tools can help improve and accelerate the specification process for the rest.
Satisfying universal preferences
Some properties are universally desirable. At the most general level, a computational process should run as instructed by its code without crashing, hanging, or suffering from intrusions that tamper with its execution or data. Formal methods can guarantee these properties in software, provided that the hardware itself operates as intended — executing instructions correctly, storing and fetching data from uncorrupted devices — and without physical interference. Building software on foundations that adhere to the object capability (ocap) model can provide many of these guarantees automatically, inherited from properties inherent in a formally-verified ocap language or operating system.4
Other universal preferences are application-specific. For example, user data should be handled in compliance with regulations (HIPAA, GDPR), and within the constraints set by hardware, databases should satisfy the ACID properties (atomicity, consistency, isolation, and durability). Effects on the world should also satisfy universal preferences: Flight control software should never command an aircraft to crash.
Human burden: Approximately nil
Reimplementing existing systems
With sufficient implementation capacity, AI can be used to replace existing software stacks from bottom to top, providing upgrades that maintain or improve external functionality. This approach can circumvent the ugly task of formalizing and implementing bug-compatibility with existing software components. Instead, formal methods can be used to build from the bottom of the stack, starting with defined processor operations and ultimately supporting interactions with human users and their tools. The goal is to describe and formalize behaviors that satisfy functional requirements, which may be as flexible as the expectations of human users faced with a new software release.
Users generally welcome moderate changes that improve software alignment with universal preferences, such as reliability, efficiency, and smooth scrolling. However, refining software behavior is a slippery slope; as external behaviors are improved, the task may overlap with specifying new functionality.
Human burden: Typically small and informal
Specifying new functionality
In developing new functionality, AI can help humans make informed choices and formalize specifications that accurately reflect these choices. AI can work with users to explore requirements while considering universal or obvious, yet unmentioned, preferences. AI assistants can highlight potential unintended consequences of choices and help humans explore tradeoffs.
Through discussions, diagrams, and simulated behaviors, interactive, multimodal systems can synthesize the concerns and insights of multiple people and AI systems. This approach avoids assigning humans the impossible task of writing (or even comprehending) masses of opaque, formal specifications. Humans can consult various AI models for summaries, evaluations, critiques, and suggested alternatives while proposing hypotheticals and asking probing questions about potentially problematic behaviors. When tests can be sandboxed or stakes are low, users can test code and provide feedback in a rapid iteration cycle. However, when stakes are high — such as in failure-critical control systems for aircraft or data collection and processing for security applications — developing and judging specifications will call for deliberative processes that are formal in a human, institutional sense (an aspect of the AI Agency model for applying powerful AI capabilities to consequential tasks).
Human burden: Exploring and choosing options assisted by AI
Informal AI in formal frameworks
Developing AI systems that meet formal specifications for behavior — and even real-world consequences of that behavior — has been identified as a challenging but important research objective. Even limited applications of verified code, though not a substitute, can provide leverage on problems of AI control by constraining AI-component interactions and outputs.
Consider the problem of implementing a secure repository of that includes sensitive personal information with strict, verifiable constraints on disclosure. How could unverified AI be applied to this information while preserving privacy guarantees? An AI system could be allowed to explore the repository freely to search for clues that suggest threats, yet would be able to act only by passing specific evidence to a reporting mechanism that itself verifiably adheres to privacy-protecting regulations.
In compound AI systems, multiple models perform tasks orchestrated by conventional software frameworks with verifiable properties. Formal methods can ensure constraints on flows of information between AI systems, and limits on the retention of information by the AI systems themselves. Ocap foundations implemented at the OS kernel level (see seL4) are available today and can do much of the work.
Credible realism and the future of software
Recognizing the potential for AI to transform software development (scope, speed, quantity, and quality) is crucial realistic views of the future. Imagining that the future will resemble the present, with software development remaining a slow, error-prone process, would be a profound failure of imagination. It would constrain our thinking about what is possible and limit our ability to plan for and shape the future.
The strategy of “credible realism” calls for exploring credible possibilities that have consequences aligned with realistic prospects. In the case of software implementation capacity, credible realism calls for focusing on several considerations:
Continued advances in applying large language models to coding
The existence and implications of formal methods in software development
The prospects for AI-enabled scaling of formal methods
That formal methods can make AI-generated code absolutely trustworthy
Crucially, all of the above points can be discussed as potentially long-term prospects, without arguing for fast or slow timelines. Setting timelines aside, each of these considerations is either credible or simply factual. Together, they give reason to explore potential futures in which novel, verifiably correct software is applied to problems ranging from AI safety to mutual trust among state actors.
Formal methods are used to co-develop code and proofs, not to attempt to prove theorems about arbitrary code.
Hardware, considered as a system of elementary digital devices (logic gates, memory cells, etc.), can also be verified using formal methods. However, elementary digital devices must be analyzed using physics, including phenomena like charge leakage and exploits like rowhammer. The proof conditions for the physical level of analysis then include correct manufacturing — which, with today's fabrication methods and supply chains, leaves a non-trivial attack surface.
Assurance at this ultimate, physical level is a matter for other sociotechnical means until atomically precise mass fabrication (APMF) technologies collapse supply chains to single facilities and enable verification at the level of discrete molecular processes and atomically precise products. Assurance through conventional monitoring and controls in semiconductor fabrication is credible but challenging and a matter of degree. Because assurance through verified APMF processes is realistic (though not yet credible), policy analysis that explores the implications of assurance by conventional means (whether these are practical or not) will lead to realistic conclusions.
Recent papers on AI applications to formal software verification include “Clover: Closed-Loop Verifiable Code Generation” and “Leveraging Large Language Models for Automated Proof Synthesis in Rust”, and to theorem proving in general, “A Survey on Deep Learning for Theorem Proving”.
The object-capability (ocap) security model is a formally defined model of computation that constrains interactions between computational entities, ensuring that information and control flow only through explicitly granted channels while enabling dynamic changes in channel topology. The ocap model can be implemented at the level of languages, operating systems, and cryptographic protocols, and systems built on these foundations inherit ocap guarantees. The seL4 OS kernel, formally verified at the level of machine instructions, implements the ocap model across OS processes. In a correctly configured seL4-based system, the kernel guarantees integrity and availability by ensuring that processes interact only through explicitly granted capabilities. (The seL4 kernel also ensures inter-process confidentiality, provided that the processor allows no timing attacks.)