The Great Security Update: AI ∧ Formal Methods with Kathleen Fisher of RAND & Byron Cook of AWS

Summary

• AI is lowering the skill floor, raising the expert ceiling, and making cyberattacks massively parallelizable. Kathleen Fisher’s verdict is “sadly, it’s all of the above”: everyone from script kiddies to nation-state adversaries gets better. Byron Cook’s counterweight is that defenders can turn each incident into a formal property, giving failures “tremendously more blast radius” for improving the systems of the future.
• Formal methods provide machine-checkable guarantees about chosen properties, not blanket proof that a system is secure. The practical objective is an operating envelope—credentials are never logged, all data at rest is encrypted, or certain data never leaves a region—not an exhaustive specification of every behavior. There are “assumptions all the way down,” from operating-system APIs to processor models and physics, but the guests argue today’s baseline is so poor that merely closing and locking the doors would transform risk.
• The HACMS helicopter demonstrated that compositional proofs can become credible system-level protection. A roughly 10,000-line SEO4 kernel backed by about 100,000 lines of Isabelle proof separated critical flight functions from a hostile camera partition; during an airborne red-team attack with two pilots aboard, the compromised partition repeatedly crashed and restarted without affecting flight. Similar quadcopter defenses remained unbroken when DARPA later exposed them to DEF CON hackers.
• AWS has already embedded formal reasoning into commercially critical infrastructure rather than treating it as academic assurance theater. IAM Access Analyzer, VPC Reachability Analyzer and related tools let customers reason about configurations, while AWS’s policy interpreter—invoked more than a billion times per second—has been proved correct relative to the formally defined policy semantics. Separate work covers cryptography, virtualization, durability and identity, with proofs increasingly “beginning to touch.”
• Automated Reasoning Checks turn natural-language policies into formal models and use theorem proving to constrain AI outputs. Because the initial translation can itself hallucinate, users inspect generated corner cases and refine the model; at inference time, multiple translations are checked for logical equivalence, supporting the stated “up to 99% verification accuracy,” not 100%. The commercial promise is an unusually strong last-mile guardrail for HR, zoning, compliance and agent workflows.
• Generative AI could invert today’s insecure-code narrative by producing both programs and independently checkable proof artifacts. Models can search for inductive invariants, ranking functions and concurrency abstractions that previously required scarce PhDs, while deterministic tools verify the result. Fisher expects GPT-6, Gemini 4, Nova and open-weight models to become superhuman secure coders if that capability is explicitly rewarded.
• A great software rewrite is becoming technically plausible, but incentives and governance—not raw capability—may determine its timing. AICC, Google’s CodeMender, an OpenAI counterpart and DARPA’s TRACTOR point toward finding, fixing and translating vulnerable legacy code at speed, including C-to-Rust migration with equivalence checks between programs where applicable. Yet safer systems invite more aggressive use—“we drive faster because our cars are safer”—while formalized policies create a second challenge: preserving legitimate exceptions without reintroducing human bias.

Deep dive

1. AI scales every attacker, but failures can compound into better defense

• Fisher’s threat assessment is categorical: “Sadly, it’s all of the above.” AI assists every stage of the cyber kill chain, increases parallelism and makes novices, capable operators and experts more effective. Even world-class reverse engineers she knows are “shocked at how good AI tools are” both as assistants and on their own.

• Today’s vulnerable software therefore faces several simultaneous threats: scaled ransomware and nation-state exploitation, subtle compromise, overt attacks and autonomous agents running amok. Cook sees software as the near-term “sweet spot” for defense, though the complete system also includes fallible hardware and people.

• Cook’s more optimistic framing is a feedback loop: defenders can translate each incident into a property—no credentials logged, all data at rest encrypted, specified data never leaving a region—and prove it against subsequent code. That could give each breach “tremendously more blast radius” for improving the systems of the future, even if it offers limited comfort today.

2. Formal methods range from routine type checks to full correctness proofs

• Cook’s compact definition is “the algorithmic search for proofs.” A proof is “a finite argument of what is true,” allowing people to “reason about the infinite in finite time and finite space” by following a small accepted set of logical rules whose applications a machine can check.

• Fisher casts formal methods as a spectrum of mathematical techniques, with usability traded against richness of guarantee. Java’s type checker proves relatively modest facts—an integer will not accidentally be added to a function—yet ordinary developers receive that assurance without understanding the proof machinery.

• JavaScript’s managed memory supplies another formal-methods-based guarantee: a value stored as an integer does not later “transmogrify itself into a function.” C lacks that memory-safety abstraction, leaving an especially valuable attack surface exposed unless other mechanisms compensate.

• At the difficult end, CompCert proves that C source maps to assembly with the same semantics. Interactive theorem proving can establish full functional correctness, but historically demanded “a huge amount of brainpower”; choosing which property deserves that expense is part of the art, because every point on the spectrum can be useful.

3. Useful security is a bounded envelope built on explicit assumptions

• Cook rejects “100% security” as the wrong practical goal: a perfectly impenetrable house would become unusable when its owner lost the keys. Current software is closer to a house whose doors and windows are open, so closing and locking them matters long before anyone attempts an invulnerable fortress.

• Fisher prefers underspecification: define the properties that bound safe operation, then let a programmer or LLM choose among multiple valid implementations. A system may need to establish regional data sovereignty without proving every detail of its memory behavior, although memory safety or other properties may be necessary in particular cases.

• Every guarantee rests on assumptions. A software proof might assume the processor’s instruction-set behavior; proving the processor introduces assumptions about lower layers and eventually physics. “There’s always assumptions all the way down,” so formal verification raises assurance rather than supplying metaphysical certainty.

• Fisher’s deliberately absurd comparison is that a room’s air could theoretically collect in one corner and suffocate everyone. Rational confidence means accepting sufficiently stable assumptions; memory safety, parser generators and input validation can then make whole classes of attack rare enough that adversaries “attack their neighbors instead of you.”

4. Proof engineering varies from automatic TLS checks to bespoke hypervisors

• Cook compares formal-methods tools to “looking at all ’80s bands, and then trying to characterize what is a pop song”: their proof representations, automation and required expertise differ radically. Proof length is therefore not governed by a universal code-to-proof ratio.

• For an Amazon-written open-source TLS implementation, Cook describes proof of correctness for the TLS handshake as completely automatic. SAT-based reasoning and inductive-invariant discovery work well because cryptographic loops tend to be simple and avoid the most difficult recursive data structures.

• Amazon’s new Isolation Engine hypervisor will be in the AWS stack for Graviton 5. Its Isabelle proof work involves intricate properties and, in Cook’s rough mental model, approximately one formal-methods expert per software engineer—close to a one-to-one relationship between proof scaffolding and implementation effort.

• CompCert’s assurance similarly has boundaries: early work assumed sequential avionics code, an ISA model such as x86 or ARM, and behaviors for operating-system or third-party APIs; an original parser assumption was later corrected. Unknown external behavior can be modeled with “demonic nondeterminism,” then refined only where the proof needs stronger assumptions.

5. HACMS turned compartment proofs into an airborne red-team test

• DARPA’s 2011–2016 HACMS program used SEO4, a formally verified separation kernel comprising roughly 10,000 lines of C and about 100,000 lines of Isabelle. Its core property was that software in one configured compartment could not interfere with another.

• On Boeing’s unmanned Little Bird, researchers separated the camera, mission-control and flight-control functions. They modeled the architecture in AADL, generated parsers from grammars and proved system-wide properties such as: every ground-station message reaching mission control had to traverse an authenticated, encrypted pathway.

• The baseline mattered. A red team compromised the unmodified military helicopter with about six weeks’ worth of knowledge, surprising Boeing’s engineers, then followed the redesign throughout the program—so its later failure was not attributable to ignorance of the new system.

• In phase two the team attacked on the ground; in phase three it attacked in flight with two test pilots aboard. Hostile code could fork-bomb and crash its camera partition, but the system simply observed, “the camera partition went down, let’s restart that partition.” The pilots could not distinguish the high-assurance helicopter from the normal version, and later DEF CON hackers failed to breach the related quadcopter.

6. Proof answers the questions asked, not every question that could matter

• Fisher says the flight chiefly demonstrated the evidence to outsiders; the people writing the program were willing to risk the pilots’ lives, and everyone in the program expected the system to be fine because of the proof and its surrounding artifacts. Residual attacks remained possible through hardware or physical means—one could still “throw a rock at the rotors”—but in that scenario the software attack was probably a lower risk than other means.

• Cook separates the “how” from the “what.” Even a magical procedure that answered every program query with perfect reliability would face infinitely many possible queries: after 5,000 proved properties, a 5,001st question might expose behavior nobody had realized they disliked.

• This is why “there’s always more to prove.” Verification can conclusively establish a well-specified statement under its assumptions, while still leaving open whether humans chose every load-bearing statement, modeled the environment correctly and composed the local results into the system property they actually care about.

7. AWS has connected customer-facing analysis to production proofs

• When Cook joined Amazon in 2014, customers valued flexible cloud policies and virtual networks but disliked not knowing whether their configurations were correct. AWS responded with IAM Access Analyzer, VPC Reachability Analyzer, S3 Block Public Access and formal reasoning embedded in Inspector, Config Rules and other services.

• Internally, teams focused on high-consequence areas including cryptography, virtualization, storage durability and identity. Rather than proving all of AWS at once, they established “key lemmas” around risky components; over time, proofs of adjacent systems began “to touch each other” and blur into broader verified regions.

• The strongest connecting example is AWS’s policy interpreter, called more than a billion times per second to decide whether API actions are authorized. It is proved correct relative to the policy-language semantics first formalized for customer analysis—answering the natural customer challenge, “How do I know that you’re actually interpreting that policy correctly?”

• After the 2022 holiday period, executives rapidly shifted questions from infrastructure toward chatbot and then multi-agent correctness. Cook says the underlying mathematics transfers: the Family and Medical Leave Act resembles an S3 policy, while proving properties of composed agents resembles proving that composed microservices give S3 strong rather than eventual consistency.

8. Automated Reasoning Checks formalize policy before constraining agents

• The product’s two activities are to formalize what is true and to remove hallucination-driven incorrectness at inference time. A generative model first translates a natural-language source—an HR handbook, for example—into a logical representation suitable for automated reasoning.

• That creates an apparent circularity: an unreliable model is being used to build the guardrail against unreliable models. AWS addresses it by traversing the generated formula, calculating representative corner cases and showing them to the user, who can reject an answer in natural language and trigger another translation-and-test cycle.

• At deployment, the system produces multiple formal translations of an input and asks a theorem prover whether they are equivalent. Agreement yields high rather than absolute assurance—hence “99%, not 100%”—while disagreement supports active listening: if interpretations differ between first-class and coach travel, the system can ask which one the user meant.

• Once the meaning is resolved, the formal model can prove or disprove compliance. The logical checker is “not creative at all”; it defines an infinite envelope of true and false answers while leaving the language model free to phrase an answer creatively inside that envelope.

9. Specification remains harder than proving or repairing the code

• Cook’s emphatic concession is that specifying the intended behavior is “by far” the hardest part, despite subsequent reasoning sometimes being undecidable or intractable, including NP-complete cases. He recalls spending extensive time on shuttle buses between buildings merely trying to get teams to agree that they had written the right specification.

• “All data at rest is encrypted” exposes the problem. What qualifies as encryption—a device “from a cereal box,” or only approved APIs? What is rest—particular storage media, or data continuously circling the world in a high-latency network? A seemingly simple requirement immediately demands several refinements.

• The initial implementation “won’t” satisfy the specification, so verification becomes an iterative repair process. Nathan observes that when a suspected bug appears, one engineer may accept it while two deny that environmental conditions could occur; Cook says the reliable way through that cognitive bias is to construct an exploit or proof of concept.

• Tools differ in diagnostic quality. Some abstractions discard enough information that they report only an incomplete proof; others produce “the crazy path through all the code” and the exact inputs that trigger failure. Concrete counterexamples are much harder for an engineering team to explain away.

10. Continuous delivery makes maintaining a proof a production discipline

• Academic formal methods historically stopped when the theorem was proved, but cloud code changes constantly. Production teams must integrate verification into CI/CD, repair proofs alongside implementations and automatically preserve proofs when a code change is irrelevant to their central argument.

• The underlying problems remain undecidable or intractable, so tools sometimes “just go to lunch.” A variable rename from X to Y can alter an internal hash table enough that a proof previously completed in three seconds takes 400 seconds—or never returns—even though the program’s relevant meaning did not change.

• The reasoning hierarchy begins with loop-free conditionals, where questions such as whether a branch can launch the rockets can already be NP-complete. Add loops or recursion and proving that an assertion never fails requires an inductive invariant: it holds on loop entry, survives every iteration and implies the forbidden state is unreachable.

• Proving eventual termination additionally requires a ranking function plus its supporting invariant; concurrency may require rely-guarantee conditions that abstract each thread’s environment. Those invented artifacts were where scarce human experts mattered most, because strong combinatorial solvers could check them once someone supplied the insight.

11. Generative AI searches for proof insights while deterministic tools judge them

• SAT solvers already transformed formal methods from a research “monastery” into practical automation. Distributed systems—Cook cites a tool called Malibu—run many solvers, share learned lemmas and exhibit a scaling law very similar to transformer models; this progress lets AWS reason reliably about customer policies and VPC networks in under 20 seconds.

• Generative AI attacks the remaining search bottleneck directly: “Find me an inductive invariant, find me a ranking function, and find me rely-guarantee constraints.” Each candidate reduces to combinatorial checks that mature solvers can accept or reject, while cloud infrastructure tries many model-and-tool combinations in parallel.

• The “move 37” analogy understates how often this matters. A successful proof generally requires an insight few humans can find, so Cook says teams are “on the verge of a move 37 miracle every time”; models can ingest documentation, threat models, operations plans and old proofs, then search for the new invariant.

• Fisher sees generative AI “turning that up to 11.” Formal languages have sparse training corpora, but proof checkers can certify synthetic examples, creating trustworthy training data. Her proposed benchmark would make model developers compete on memory safety, type safety and input validation—not merely the volume of code generated.

12. Secure-code models make a great rewrite plausible, not inevitable

• Nathan’s proposed flywheel holds: models generate many proof attempts, checkers retain the successes, certified proofs become training data, and proof success becomes a reward for code generation. Asked whether GPT-6 and Gemini 4 could be superhuman secure coders, Fisher answers yes and also names Nova and open-weight models.

• Translation offers a path through decades of legacy software. The old program can serve as the specification for the new one, making equivalence comparatively tractable; Cook cites Java-to-Rust migration, while Fisher points to DARPA’s TRACTOR effort to translate C into idiomatic, memory-safe Rust.

• Fisher says AICC showed that AI plus cybersecurity can find and fix bugs “at speed and scale,” alongside Google’s CodeMender and a similar OpenAI project. Technology may be ready before society is: cyber harm has increased for roughly 20 years while the public behaved like “the frog getting boiled,” though Y2K proved coordinated repair is possible.

• Cook’s caution is that safety enables risk-taking: “We drive faster because our cars are safer.” Markets trade security against performance, features and availability, as when device drivers moved into kernel space for faster games. Formal methods could help sandbox a highly aggressive AI—even “sandboxing superintelligence”—but stronger containment may encourage deployment of more capable systems.

13. Formal policy can democratize access while making exceptions explicit

• Cook’s Portland zoning example captures the product opportunity. Today, someone planning an accessory dwelling unit may need an architect who works in Portland, Oregon, to interpret setbacks—including whether a structure must sit five feet from a property line. A hallucinating chatbot cannot safely replace that intermediary; a formally checked agent might provide accurate, inexpensive, 24/7 access.

• Policy models could be published by governments, open-sourced, licensed or combined across institutions. Because each answer traces to explicit axioms, citizens can identify “this axiom that makes this rule unfair,” propose a revision and replay prior conversations to see whose outcomes would change.

• Nathan and Fisher preserve the central objection: rules sometimes need legitimate wiggle room. Cook suggests unequal axiom classes—some mandatory, some avoidable unless necessary, and a final escalation such as “What does Steve say?”—but Nathan asks where judgment should reside, since human discretion can supply either humane flexibility or destructive bias.

• The closing synthesis is neurosymbolic AI, Cook’s “peanut butter and chocolate moment.” Formal methods offer guarantees but are rigid and difficult; AI is flexible and accessible but untrustworthy. Their intersection could be multiplicative, provided institutions accept the deeper challenge Nathan identifies: society is “learning how hard it is to figure out what truth is.”