They Owned the Camera Partition—and Still Couldn't Crash the Helicopter

Kathleen Fisher is director of RAND's Cybersecurity Initiative, the former lead of DARPA's High Assurance Cyber Military Systems program, a past director of DARPA's Information Innovation Office, and, as of February, incoming CEO of the UK's Advanced Research and Invention Agency. Byron Cook is a vice president and distinguished scientist at Amazon, where since 2014 he has pushed formal methods into the core of AWS, arguably the world's largest cyber target. Nathan Labenz, host of the Cognitive Revolution, admits he has never felt more outclassed by guests; he still wanted a 101 on the one strategy he keeps hearing can resolve specific vulnerabilities once and for all.

Labenz offers three stories about how AI might change offense: chatbots that lift script kiddies, AlphaGo-style 'move 37' zero-days, and parallelization of work that used to be limited because hackers cannot share freely. Fisher says, sadly, it is all of the above. AI assists at every stage of the kill chain and every expertise level. People who know nothing know more; people who know some know more; experts become more effective; and attackers can work at greater scale and in parallel. Colleagues who are among the best reverse engineers on the planet, she says, are shocked at how well the tools help them, and at how well the tools can go on their own.

Cook agrees and adds the defender's version. For a long time, software security depended on the absence of mechanisms: humans wrote code, did not really know what the programs were doing, and hired a few good people to watch. Agentic tools are pushing the industry from those sociotechnical habits toward formalization. After a security event, a team can write down 'we never want to be in that state again' as a property and show it of the code. Each incident, he says, has a much larger blast radius on future systems than it used to, though he is speaking more to the future than to this week.

Fisher pulls the claim back to the present. Software is riddled with vulnerabilities, and AI will make them easier to exploit for script kiddies, ransomware gangs, nation-states, and runaway agents, subtly or overtly. The same technology can be flipped to make software less vulnerable. Hardware, software, and people are all in play; software is the sweet spot where a positive difference can come relatively quickly. Later she will cite Google's CodeMender, similar work at OpenAI, and the AI Cyber Challenge as evidence that AI plus cyber can already find and fix bugs at speed and scale.

Cook's one-line definition: formal methods are the algorithmic search for proofs. A proof is a finite argument that something is true. You can reason about the infinite in finite time and space if you follow a small, chess-like set of rules society has settled on over two thousand years, modus ponens among them. These days algorithms can search for those arguments, and generative AI is actually very good at helping find a proof that a checker, which only follows the rules, can then accept.

Fisher zooms out: it is a set of mathematical techniques that let a machine check that you did the work properly, and it is not one size fits all. At the easy, weak end, Java's type checker is a formal method. Run the compiler and it proves you will not add an integer to a function; you did not have to know how, only the rules of how types may interact, and you had to avoid casts that break soundness. Type safety is a relatively thin guarantee. JavaScript, Labenz's home turf, still gives you memory safety: what you store as an integer comes back as an integer. C does not. Memory safety, she says, is extremely useful for not getting hacked, and it is a property the language and its interpreter enforce.

At the other end sits interactive theorem proving of full functional correctness. CompCert is a verified C compiler that proves C maps to assembly with the same semantics, each logical step machine-checked, at something like PhD-level effort. In between is a whole range of tools with intermediate properties and intermediate elbow grease. Choosing which property and which level of effort is part of the art. Labenz's ordinary web-developer loop—throw code together, click around, ship—cannot be exhaustive. Type checkers catch rules he would never have thought to test. Parsers, he has noticed while doing homework for the show, are a very common weakness; Fisher agrees that input validation sits beside memory safety and type safety as a door you can actually lock.

Labenz wants to know how a layperson can sleep after a proof: what if there was a mistake in the process? Fisher analogizes to a house. One hundred percent security is the wrong goal; a house no one can ever enter is a house you cannot re-enter if you lose the keys. Right now the industry is closer to doors and windows standing open. The job is to close and lock them, not to invent a fortress. Cook's mental model is an envelope of properties you want to hold: credentials never logged, data at rest encrypted, certain data never leaving a region for sovereignty. You underspecify, then let a programmer or an LLM implement inside that envelope. Proving everything is not the point.

Assumptions go all the way down. Prove a program correct and you typically assume the microprocessor is correct. Prove the microprocessor and you assume the principles of physics. Gravity has held; you believe it will continue; you will not get a mathematical proof of that without still more assumptions. You are only ever raising assurance. Cook's comfort test is the air in the room: theoretically it could all rush into a corner and you would suffocate, and you still live as if it will not. Memory-safe systems with generated parsers and validated inputs make certain attacks much less likely. Attackers may simply go next door.

CompCert's remaining assumptions, as far as they recall, are about the underlying hardware: the x86 or ARM instruction set is taken as given, with a model of the ISA rather than a proof of the ISA itself. Early versions also assumed a parser that turned out to be wrong and was later fixed. The original was sequential, aimed at single-threaded avionics. Calls into the operating system and other third-party APIs need assumptions about what those APIs do. The useful trick is demonic non-determinism: you write a formula that means 'I do not know what this returns,' and non-determinism is already paid for in the tool. You refine those assumptions as you learn more. There is always another layer.

Proofs are not one shape. Some tools, using predicate abstraction and counterexample-guided refinement, run fully automatically and discover proofs of API-usage properties. Amazon's open-source TLS stack, s2n, used across the company, has an automatic proof of the handshake: SAT plus discovery of inductive invariants, helped by the fact that cryptographic loops are usually simple and not over complex data structures. At the other extreme, AWS has announced Isolation Engine, a new hypervisor headed for the Graviton 5 stack, with properties proved in Isabelle. Cook's mental model of that team is about a one-to-one ratio of engineers to formal-methods experts, and roughly one-to-one proof scaffolding to code.

How do low-level lemmas add up to 'the software does what it is supposed to do'? Fisher's exhibit is seL4, a separation kernel proved fully functionally correct by a team in Australia. The headline property: you can configure compartments so that code in one cannot interfere with another. About 10,000 lines of C came with about 100,000 lines of Isabelle. That effort was worth it because the kernel is a reusable building block. HACMS, the DARPA program Fisher ran from 2011 to 2016, used seL4 on Boeing's Unmanned Little Bird to partition the helicopter. Analysis said the camera partition was not important to flight or to talking to the ground station. Mission control talked to the ground; the flight computer actually flew the aircraft.

The team modeled the architecture in AADL, wrote the ground-station protocol as a grammar rather than by hand, and proved system-wide properties: the only path from the ground to the mission-control computer had to be authenticated and encrypted. Parser tools, encryption tools, and seL4 isolation combined. Then came the red team. Phase one hit the unmodified platforms; Boeing engineers were surprised that six weeks of knowledge was enough to get in, while nobody was surprised about the quadcopter. Phase two attacked on the ground. Phase three attacked in flight with two test pilots aboard, trying not just to crash a partition but to crash the helicopter. The pilots survived and could not tell they were flying the high-assurance build. The camera partition kept dying—the red team could fork-bomb its own box—and the rest of the system restarted it. Flight operations were untouched.

The red team had followed the program the whole way, so ignorance was not the excuse. DARPA later took the similarly hardened quadcopter to DEF CON's aerospace village; years afterward, no one got in. The techniques, Fisher says, pass the test of time. Hardware attack is still probably possible; the software path is badly blocked. Labenz asks how many nines 'proven' meant before the bird went up. The flight, she thinks, was mostly demonstration: the people writing the program were willing to risk the pilots' lives, and everyone in the program already believed it would be fine, because of the proof plus all the surrounding reasoning. Someone could still throw a rock at the rotors. Helicopters are not very stable. Software risk, in that setup, had fallen below other risks. Cook's metaphor: even a magical oracle that answers any question 100 percent still faces an infinite set of questions. You might have asked 5,000 and missed the 5,001st that reveals something you do not like.

Cook joined Amazon in 2014. Customers loved the flexibility of the policy language and of virtual networks; they did not love not knowing whether they had gotten the configuration right. The first customer-facing tools were IAM Access Analyzer, VPC Reachability Analyzer, S3 Block Public Access, plus pieces in Inspector and Config rules. Internally the team picked places that had to be right: cryptography, virtualization, storage durability, identity. Proofs of two systems start to touch and blur into a system with proved parts.

The policy interpreter is the example that makes the connections visible. On every AWS API call, the system gathers policies for the principal and the resource, hands them to the interpreter, and gets allow or deny. That code is invoked more than a billion times per second and is now proved correct. Correctness here has a precise meaning: it is relative to the semantics of the policy language defined for IAM Access Analyzer. First they defined the semantics, then they gave customers tools to reason about their own policies, then customers asked how they knew the interpreter matched those semantics, so they went and proved it. The same pattern shows up in virtualization and elsewhere.

After the 2022 holiday, boards wanted a generative-AI story, and customer questions shifted from chatbot correctness toward multi-agent systems. Under the hood, many of the same techniques apply. An FMLA policy is a lot like an S3 bucket policy. Reasoning about a multi-agent composition looks a lot like reasoning about microservices to show that S3 offers strong consistency rather than eventual consistency. Generative AI can be asked to find a program and a proof at the same time, so proofs can be checked as code is synthesized. The hard part, Cook and Fisher agree, has always been figuring out what you want to prove. Automated Reasoning Checks, Bedrock Guardrails, and Amazon's specification-driven Kiro IDE are aimed at iterating on that specification until you are proving what you think you are proving.

Automated Reasoning Checks promise to shrink hallucinations and deliver up to 99 percent verification accuracy. The starting point can be a natural-language policy written with no software in mind, such as the Family and Medical Leave Act, that someone now wants an AI to apply to leave requests. Under the hood the product asks a generative model to translate the PDF into temporal logic, SMT, Lean, or similar. That immediately raises the objection: you just used generative AI to formalize, and the whole point was to catch generative AI's hallucinations.

The reply is an old pairing. Walk the structure of the formula, compute representative corner cases, and show a non-expert what answers the logic will actually give. If they dislike an answer, they say why in natural language and the translation runs again. That is how the field has always worked: a formal-methods person sits with a domain expert in biology, operating systems, airspace, or railway switching, looks at examples, hears 'you did not understand the assumption,' bakes it in, and iterates until they cannot find more problems. After lock-in, user questions are mapped back to the formal model and proved or disproved. Multiple independent translations are checked for equivalence by a theorem prover; agreement is why the number is 99 percent rather than 100. Disagreement triggers active listening: one translation said first class, the other said coach, so ask the user or query a database.

The spec remains, by far, the hardest part, even though reasoning about programs is undecidable or NP-complete. Cook has spent a lot of his career on shuttle buses between buildings trying to get teams to agree they got it right. 'All data at rest is encrypted' sounds plausible until you ask what encryption is. A serial-box gadget from the street? Probably not—so how do you define it? What is rest? Data sitting on a table? Digital storage? Packets flying around a network, using latency so they never hit a disk? If that counts as rest, the property you thought you were proving probably does not hold. Three or four refinements later you have APIs and media named, and that was the simple case.

When a proof fails, cognitive bias takes over. Put a suspected bug on the board in front of three engineers: one will say it is a bug, two will say it is not, because 'the environment will never look like that.' The only way to ground the argument is often an exploit that shows the path. Some tools spit out the crazy triggering input; others just say the proof did not go through and leave you guessing. In the academic monastery, you then celebrate. In the cloud, the code changes constantly, so the proof has to live in CI/CD and be repaired. Sometimes irrelevant edits let proofs update automatically. Sometimes, because the problems are undecidable, the solver goes to lunch: renaming a variable can perturb a hash table so that a three-second query never returns, or takes 400. That operational pain is part of why the generative-AI world is interesting.

Formal methods spent the 1970s and 1980s in decline, Cook notes, proposed as far back as Turing's 'Checking a Large Routine' and then kept alive in universities, the 'monasteries.' What changed was automation. SAT solvers took over hard combinatorial work and helped make HACMS and Amazon's program practical. Fisher, speaking with her former DARPA I2O hat on, thinks large language models turn that automation up to eleven because so much of formal methods is language. The languages are sparse, with little public training data, but the field can generate its own data and know it is correct by feeding it to checkers. That flywheel, plus a high-quality benchmark so frontier labs compete on code security and not just on writing code, is how you get models that emit memory-safe, type-safe, input-validated programs. The models will not care unless the scoreboard does.

Cook lays out a four-rung hierarchy. With no loops or recursion, only conditionals, 'could this launch the rockets?' is NP-complete, essentially SAT. Progress there has been stunning: competition winners on fixed hardware, then distributed solvers such as Mallob that share lemmas across a network, a scaling law he compares to transformers. That is why AWS can reason about policies and VPC networks in under 20 seconds. Add loops, care only that an assertion never fails, and you are in undecidable territory: you must find an inductive invariant. Add 'eventually' or termination and you also need a ranking function, plus combinatorial reasoning. Add concurrency and you need rely-guarantee environment abstractions so you prove one thread at a time.

Tools for the first rung are already strong. For the upper rungs, the reliable method was often to hire a PhD and chain them to a desk. Generative AI changes the search: ask it for an inductive invariant, a ranking function, rely-guarantee constraints, then reduce the rest to combinatorial checking, which is good. Run combinations in parallel on the cloud and keep the answer you like. The invariants and ranking functions the models find, he says, are pretty great. Getting a proof through has always required rare insight, so you are on the verge of a move-37 every time one lands. Amazon teams that invested in proof scaffolding are now pairing programmers with generative tools and using that scaffolding as semantic guardrails so they can deploy without rolling back as often.

It works better, an Amazon blog post argues, if documentation, threat models, and ops plans sit with the code, so the model sees the human-level story as well as the repository. For proof search, humans read old proofs and pull an invariant out of a hat; people like John Harrison have read them all. You can pass prior proofs and Lean-trained models already know some of that literature. Labenz restates the flywheel: proofs are hard to find and easy to check; run the models a lot, fold successes back into training, then use proof capacity as a reward on coding. Cook notes it is easier to auto-formalize 'all data at rest is encrypted' than the FMLA. Asked whether GPT-6, Gemini 4, Nova, and open-weight models should be superhuman at writing secure code the first time, he says yes, it is already heading there: open math problems were proved the week before. Fisher adds the missing half: you still need incentives to produce good code, stop producing bad code, and replace the bad code already in critical infrastructure. DARPA's TRACTOR program aims to translate C into idiomatic Rust. One of the easiest formal jobs, Cook says, is proving two programs equivalent, because then you already have a spec.

Labenz wants a timeline for a society-wide rewrite of sixty years of software before attackers use the same models on critical infrastructure. Fisher says motivation, not technology, is the bottleneck. The AI Cyber Challenge, CodeMender, OpenAI's similar work, and the conversation so far all suggest that AI-enabled generation can rewrite to a higher standard in the relatively short term, and that this is the worst the tools will ever be. Attacks will keep rising. The sentence 'cyber attacks of increasing severity' has been true for twenty years, she notes, and society has sat like a frog in warming water. Y2K was a rare mobilization that actually fixed the two-digit dates. The tools will be there when people get serious. She does not know when that is.

Cook watches the commercial marketplace: how much people will put up with, and how much they will pay. He chooses machines and phones by security reputation, pays a premium, and advises others to do the same. Inside Amazon, threat models differ by team; the barrier to using formal tools is dropping, so teams that previously would not are starting to. Kiro's differentiator is specification-driven development. AgentCore Policy, announced the week of the recording at re:Invent, uses Cedar as a formal envelope around what an agent may and may not do. Agentic AI, he says, is a way of saying we are doing declarative programming again. He is no less worried than he was ten years ago, but he is fairly optimistic that products people flock to will drive the flywheel.

If society stopped writing new software and did the great rewrite, could AI bug-finders become unnecessary? Fisher likes belt and suspenders: it does not hurt to keep poking. You could get to a place where the pokers rarely find anything, and where hardware and people, not software, are the source of almost all remaining holes. Labenz lights up at the containment implication: maybe self-exfiltration risk can be taken off the table. Cook pours cold water. Every safety technology lets us push harder; people drive faster because cars are safer. He once saw a company keep drivers in user space, then move them into the kernel because some games were slower, losing the protection. Video drivers skipped error checks, including failed memory allocation, to stay fast on the common path. Markets navigate availability, features, performance, and security; they do not go all in on security. Fisher agrees one hundred percent, and still says that if you were focused on sandboxing a super-aggressive AI, formal methods would help. That frontier—virtualization, sandboxing, policies for AI—was the meeting she had been in before the call.

For AI engineers shipping business systems, Automated Reasoning Checks are a way to tell stakeholders that FMLA-like policies can be implemented with a stated confidence. Today's wheels are often greased by going slightly off policy for a long-tenured employee. Cook's Portland, Oregon example makes the sociotechnical status quo concrete. To put an accessory dwelling unit in the backyard you file with the city, hire an architect who knows Portland, Oregon rather than Portland, Maine, and hope they maximized setbacks and height rules you cannot check. Hallucinating models cannot yet let you ask the zoning code at 2 a.m. and start digging. The last mile is correctness. Automated reasoning is not creative; it defines the envelope of true and untrue answers with logic, lets the language model be as creative as it wants, then maps the output back and proves or disproves it.

Open, licensed, or city-provided rule sets could be conjoined. Citizens could argue that a particular axiom makes a rule unfair, propose a change, save past chats, and replay them to see which answers would shift. Not all axioms are equal: some are first-class, some are second-class 'avoid if you can,' and the last can be 'what does Steve say?' That is an explicit fudge, a get-out-of-jail card written as logic rather than buried in a prompt. Labenz wonders about a right to appeal to a human, which Europe is exploring. Cook notes people already vote with their feet across countries. Fisher adds the double edge: human judgment sometimes adds needed flexibility and sometimes adds bias that torches the process. The big societal challenge, Cook says, is learning how hard it is to figure out what truth is.

His closing frame is neurosymbolic AI: automated reasoning and statistical methods, long siloed in different conferences, blurring back together in a way envisioned in the early 1950s. The magic is at the intersection, a peanut-butter-and-chocolate moment with a multiplicative effect. Fisher uses the same metaphor. Formal methods give guarantees but are rigid and hard to use; AI is flexible and easy but often untrustworthy. Put them together and you get strengths of both. DARPA I2O has programs exploring different combinations; the craft is which mix, in which circumstance. Labenz calls it one of the few strategies he has heard that can really work, in the sense of closing specific critical vulnerabilities for good.