Emerging Trends
The Math that Makes Technology Trustworthy
The Math that Makes Technology Trustworthy
Formal methods and automated reasoning are reshaping how agencies can validate critical software, enforce AI guardrails, and eliminate entire classes of vulnerabilities.
By Wyatt Chaffee, featuring Bill Vass and Byron Cook
Velocity Magazine | V5. Summer 2026
Speed Read ↗︎
Automated reasoning uses mathematical proofs to validate that software and AI systems will function as intended, eliminating entire classes of vulnerabilities before deployment. These techniques—already securing cloud infrastructure, aerospace systems, and cryptographic code—are emerging as a solution for AI assurance, enabling engineers to define and enforce the boundaries of safe, policy-aligned model behavior.
This is a web summary.
Download the article for extended analysis, a history of the field, and the complete Q&A interview with Amazon’s Byron Cook, or download the full edition of Velocity for more insights for innovators.
Speed Read ↗︎
- Automated reasoning uses mathematical proofs to validate that software and AI systems will function as intended, eliminating entire classes of vulnerabilities before deployment.
- These techniques—already securing cloud infrastructure, aerospace systems, and cryptographic code—are emerging as a solution for AI assurance, enabling engineers to define and enforce the boundaries of safe, policy-aligned model behavior.
- Amazon's Byron Cook explains how automated reasoning scaled from academic theory to protecting billions of cloud transactions daily—and why neurosymbolic AI is accelerating broader adoption.
This is a web summary.
Download the article for extended analysis, a history of the field, and the complete Q&A with Amazon’s Byron Cook, or download the full edition of Velocity magazine for more insights for innovators.
Speed Read ↗︎
Automated reasoning uses mathematical proofs to validate that software and AI systems will function as intended, eliminating entire classes of vulnerabilities before deployment. These techniques—already securing cloud infrastructure, aerospace systems, and cryptographic code—are emerging as a solution for AI assurance, enabling engineers to define and enforce the boundaries of safe, policy-aligned model behavior.
This is a web summary.
Download the article for extended analysis, a history of the field, and the complete Q&A with Amazon’s Byron Cook, or download the full edition of Velocity Magazine for more insights for innovators.
Federal missions increasingly rely on software and AI systems to make real-time decisions under fast, fluid, and adversarial conditions. Yet our methods for ensuring software correctness have barely changed. Traditional testing shows that software works in some scenarios—not all of them. As AI expands the space of possible behaviors, the gap between what agencies can test and what they must trust is widening.
Automated reasoning and formal methods address this gap directly. Instead of sampling behaviors through tests, they generate mathematical proofs that a system will always uphold its critical properties—regardless of input, environment, or adversary. It replaces "Did we test enough?" with "Do we have a proof?"—the difference between stress-testing a bridge with trucks and demonstrating through structural calculations that it will hold any intended load.
"Automated reasoning is like little mechanical engines of truth. You're reasoning about the infinite, using a composition of very simple parts that are very, very powerful."
—Byron Cook, AWS Vice President & Distinguished Scientist
Beyond Testing
A function operating on 32-bit rational numbers could require exhaustive computation to test every possible input. A formal methods tool can represent that entire set symbolically and prove the desired property for all of them in minutes. While testing scales with cases checked, formal reasoning scales with the logic of the problem.
The result: an automated reasoning tool can examine an authentication module and produce a mathematical proof that no input—no matter how malformed or adversarial—will ever lead to unauthorized access. When it reports that a property holds, that result is mathematically guaranteed. Not for most cases. For all cases.
A formal proof is only as trustworthy as its specification. If the spec doesn't faithfully represent the code, you may have proven the wrong thing.
key capabilities
SAT/SMT SOLVERS
Logical Satisfiability
Determines whether any combination of inputs can satisfy a formula. Microsoft's Z3 is the most widely used, handling integers, arrays, and bit-vectors.
MODEL CHECKERS
State Space Exploration
Examines every state a system can reach. Model Checkers are useful for concurrency and timing bugs that testing alone rarely surfaces.
PROOF ASSISTANTS
Human-Guided Proof
Tools like Rocq, Isabelle, and Lean let engineers construct formal proofs while the computer verifies every step, producing auditable high-assurance artifacts.
SYMBOLIC EXECUTION
Path Exploration
Runs programs with symbolic values, exploring all execution paths to surface vulnerabilities—demonstrated at scale in DARPA's 2016 Cyber Grand Challenge.
Where Automated Reasoning is Already Deployed
Long reserved for chip manufacturers and aerospace, these techniques are now in mainstream engineering. AWS uses automated reasoning to verify identity, access, and network isolation policies—tools like Zelkova and Cedar protect billions of transactions daily. The seL4 operating system kernel has a full machine-checked correctness proof. Airbus used the Astrée tool to confirm no runtime errors in primary flight control software for the A340 and A380.
The federal government has supported this work for decades. DARPA's HACMS program used seL4 to build formally verified software for unmanned military platforms. NASA Ames has applied model checking to autonomous planning software, including systems flown on Deep Space 1.
A Trust Layer For AI
LLMs are non-deterministic by design and sometimes hallucinate. For intelligence analysis, medical decision support, and financial compliance, automated reasoning offers a way to manage these risks—not by explaining how a model thinks, but by constraining what it is allowed to do. Engineers declare allowed and disallowed behaviors; formal tools enforce those limits at runtime.
In LLM-guided formal verification, a language model generates a candidate proof and a formal tool checks it—catching hallucinations before they propagate. Google DeepMind's AlphaProof used this approach in 2024 to solve International Mathematical Olympiad problems at a silver-medal level. In verified code generation, formal tools check AI-generated code before deployment—critical when human review can't scale to the volume AI produces.
GETTING STARTED
A Path to Adoption
1
Start with automated reasoning, not full formal verification.
Solver-backed tools like Z3, TLA+, and Cedar are more accessible and already integrated into commercial services.
2
Identify highest-stakes components.
Cryptographic code paths, authorization modules, and state machine controllers deliver the most value for effort.
3
Integrate into CI/CD pipelines.
Automated reasoning maximizes return when it runs continuously alongside existing tests, not as a one-time exercise.
4
Build internal exemplars.
End-to-end, realistic examples convert skeptics and give teams a concrete model to follow.
5
Move now.
AI-augmented reasoning—where LLMs generate specifications and candidate proofs—is emerging fast. Capability built today becomes guardrails for AI-generated content tomorrow.
Reasoning About the Infinite:
An Interview with Byron Cook
Booz Allen Chief Technology Officer Bill Vass spoke with Byron Cook, AWS Vice President, Distinguished Scientist, and Automated Reasoning Group Lead, to explore new perspectives on automated reasoning and the math that makes technology trustworthy.
This is an excerpt of their conversation. Download the full interview.
What are formal methods, what is automated reasoning, and how do they relate?
They’re cousins. “Formal methods” is the term people used in the seventies and eighties before the tools were very automated. Automated reasoning is the automation of the reasoning you were doing when you did formal methods manually.
The idea behind formal methods—going back to the Greeks—is that rather than thinking about the content of the argument, you think about the form of the argument. Now you can say: If the argument has this form, it’s correct, regardless of what “P” and “Q” actually are. Automated reasoning is the automation of the reasoning over that form.
How would you explain automated reasoning to a non-mathematician?
Usually, people have done just a little bit of algebra. They’ve pushed symbols around—X plus Y is the same as Y plus X. You’ve moved symbols, so X and Y are symbols; that’s symbolic reasoning. And I think everyone can look at X plus Y and Y plus X and say, yeah, it’s roughly the same thing. But you’ve actually just reasoned about the infinite—X and Y range over potentially all the integers, all the rationals.
There’s some equipment you can pull in to ensure that X plus Y equals Y plus X, and they’re the very same mechanisms used around 300 BC to show that the Pythagorean theorem held. Reasoning, in the sense I’m talking about, is finding an air-tight argument as to why something is true, where each step of the argument rests on axioms, or the foundations we’ve agreed on as a society for how to establish truth. The automated part is just algorithms over that. You’re searching for finite arguments about the infinite.
How do you recommend thinking about the cost of implementing automated reasoning?
Automated reasoning is largely a CPU activity, not a GPU activity, so it's relatively cheap. But culturally it's expensive, because familiarity and intuition about where these techniques will and won't work are not commonly held in the IT community. You have to think about things differently.
Automated reasoning is like jazz. Miles Davis said jazz is all about the notes you don't play. It's all about how you reframe a question into a different question that you can answer efficiently—even though you're reasoning about the infinite without running the program.
Read the Full Article
The article PDF includes the complete Q&A interview—covering agentic AI policy envelopes, DARPA programs, the future of auto-formalization, and how Cook built AWS's 350-person automated reasoning organization—plus a history of the field from 1956 to today.
Explore Velocity V5.
in conversation
Infrastructure to impact
a16z’s Raghu Raghuram on AI’s next frontier, defense tech, and why the future of innovation runs through government.
tech watch
Don't Take My Word For It
Zero‑knowledge proofs are emerging as a transformative way to break the “proof vs. privacy” tradeoff.
in conversation
Infrastructure to impact
a16z’s Raghu Raghuram on AI’s next frontier, defense tech, and why the future of innovation runs through government.
tech watch
Don't Take My Word For It
Zero‑knowledge proofs are emerging as a transformative way to break the “proof vs. privacy” tradeoff.
New edition | v5. summer 2026
Explore the New Velocity
cover story
Reimagining Cyber for a Faster Fight
Securing enterprises against AI threats requires disrupting operating models, enriching detection, and strengthening resilience—because attacks now unfold in minutes, not days.
tech spotlight
How Can You Trust Agentic AI? Start with Engineering
Why trust must be designed, governed, and validated—not assumed.
mission spotlight
Infrastructure Under Attack: The Zero Trust Imperative
Cybersecurity must go beyond compliance to defeat new threats.
in conversation
Infrastructure to Impact with Raghu Raghuram
An interview with Raghu Raghuram, managing partner at a16z.
emerging trends
The Math that Makes Technology Trustworthy
Formal methods and automated reasoning are reshaping software and AI security.
lessons from the edge
Resilience Tops Perfection: Desiging for Failure Wins
Resilience doesn't come from preventing failure, it comes from surviving it well.
tech watch
Don't Take My Word For It: Zero-Knowledge Proofs
Trusting more (but revealing less) with zero-knowledge proofs for government.
in conversation
Infrastructure to Impact with Raghu Raghuram
An interview with Raghu Raghuram, managing partner at a16z.
emerging trends
The Math that Makes Technology Trustworthy
Formal methods and automated reasoning are reshaping software and AI security.
lessons from the edge
Resilience Tops Perfection: Desiging for Failure Wins
Resilience doesn't come from preventing failure, it comes from surviving it well.
tech watch
Don't Take My Word For It
Trusting more (but revealing less) with zero-knowledge proofs for government.
New edition | v5. summer 2026
Explore the New Velocity
cover story
Reimagining Cyber for a Faster Fight
Securing enterprises against AI threats requires disrupting operating models, enriching detection, and strengthening resilience—because attacks now unfold in minutes, not days.
tech spotlight
How Can You Trust Agentic AI? Start with Engineering
Why trust must be designed, governed, and validated—not assumed.
mission spotlight
Infrastructure Under Attack: The Zero Trust Imperative
Cybersecurity must go beyond compliance to defeat new threats.
in conversation
Infrastructure to Impact with Raghu Raghuram
An interview with Raghu Raghuram, managing partner at a16z.
emerging trends
The Math that Makes Technology Trustworthy
Formal methods and automated reasoning are reshaping software and AI security.
lessons from the edge
Resilience Tops Perfection: Desiging for Failure Wins
Resilience doesn't come from preventing failure, it comes from surviving it well.
tech watch
Don't Take My Word For It: Zero-Knowledge Proofs
Trusting more (but revealing less) with zero-knowledge proofs for government.
in conversation
Infrastructure to Impact with Raghu Raghuram
An interview with Raghu Raghuram, managing partner at a16z.
emerging trends
The Math that Makes Technology Trustworthy
Formal methods and automated reasoning are reshaping software and AI security.
lessons from the edge
Resilience Tops Perfection: Desiging for Failure Wins
Resilience doesn't come from preventing failure, it comes from surviving it well.
tech watch
Don't Take My Word For It
Trusting more (but revealing less) with zero-knowledge proofs for government.
New edition | v5. summer 2026
Explore the New Velocity
cover story
Reimagining Cyber for a Faster Fight
Securing enterprises against AI threats requires disrupting operating models, enriching detection, and strengthening resilience—because attacks now unfold in minutes, not days.
tech spotlight
How Can You Trust Agentic AI? Start with Engineering
Why trust must be designed, governed, and validated—not assumed.
mission spotlight
Infrastructure Under Attack: The Zero Trust Imperative
Cybersecurity must go beyond compliance to defeat new threats.
in conversation
Infrastructure to Impact with Raghu Raghuram
An interview with Raghu Raghuram, managing partner at a16z.
emerging trends
The Math that Makes Technology Trustworthy
Formal methods and automated reasoning are reshaping software and AI security.
lessons from the edge
Resilience Tops Perfection: Desiging for Failure Wins
Resilience doesn't come from preventing failure, it comes from surviving it well.
tech watch
Don't Take My Word For It: Zero-Knowledge Proofs
Trusting more (but revealing less) with zero-knowledge proofs for government.
in conversation
Infrastructure to Impact with Raghu Raghuram
An interview with Raghu Raghuram, managing partner at a16z.
emerging trends
The Math that Makes Technology Trustworthy
Formal methods and automated reasoning are reshaping software and AI security.
lessons from the edge
Resilience Tops Perfection: Desiging for Failure Wins
Resilience doesn't come from preventing failure, it comes from surviving it well.
tech watch
Don't Take My Word For It
Trusting more (but revealing less) with zero-knowledge proofs for government.
New edition | v5. summer 2026
Explore the New Velocity
cover story
Reimagining Cyber for a Faster Fight
Learn how CISOs are rebuilding to keep pace with AI-powered attacks.
tech spotlight
How Can You Trust Agentic AI? Start with Engineering
Why trust must be designed, governed, and validated—not assumed.
mission spotlight
Infrastructure Under Attack: The Zero Trust Imperative
Cybersecurity must go beyond compliance to defeat new threats.
in conversation
Infrastructure to Impact with Raghu Raghuram
An interview with Raghu Raghuram, managing partner at a16z.
emerging trends
The Math that Makes Technology Trustworthy
Formal methods and automated reasoning are reshaping software and AI security.
lessons from the edge
Resilience Tops Perfection: Desiging for Failure Wins
Resilience doesn't come from preventing failure, it comes from surviving it well.
tech watch
Don't Take My Word For It: Zero-Knowledge Proofs
Trusting more (but revealing less) with zero-knowledge proofs for government.
