Ben Wooding
Postdoctoral Researcher, Vanderbilt University
Institute for Convergent Software Integrated Systems (ICONS)
Formal methods for safe AI in cyber‑physical systems
🌍Originally from England — ten years in Uganda as a missionary kid
💍Married to Lucy
⛪Immanuel Church Nashville
Two weeks of headlines
How do we know what’s real? And what’s just noise?
Neural networks are moving into the control loop
Bak & Tran 2022, CC BY 4.0
Huang et al., Sensors 2020, CC BY 4.0
Alibeigi et al. 2023 (ZOD), CC BY 4.0
Cheng et al., Diagnostics 2024, CC BY 4.0
Wang et al., PLOS One 2026, CC BY 4.0
Zhang et al., Sensors 2025, CC BY 4.0
So why are we letting them in at all?
The Turing Award keeps going to formal methods
The ACM A.M. Turing Award — “the Nobel Prize in Computing” — has 81 laureates. Twelve of them laid the foundations of formal methods: the logics, automata and algorithms for proving that programs do what they should.
Edsger Dijkstra1972“composed correctly, not just debugged into correctness”
inductive assertions (1967) — the root of program verification
Tony Hoare1980Hoare logic (1969): {P} S {Q}
Michael Rabin1976nondeterministic finite automata (1959, with Scott)
Dana Scott1976the same paper; later denotational semantics
LCF: machine‑assisted proof; ML; CCS
Stephen Cook1982NP‑completeness (1971) — the wall we hit five slides from now
Amir Pnueli1996temporal logic for programs (1977): “always”, “eventually”
Edmund Clarke2007model checking (1981, with Emerson): search every state
Allen Emerson2007model checking; CTL, a branching‑time temporal logic
Joseph Sifakis2007model checking, independently (1982, with Queille)
Leslie Lamport2013safety and liveness (1977); logical clocks; TLA+
Recently AI too: 2018 — Bengio, Hinton, LeCun; 2024 — Barto & Sutton.
Portraits via Wikimedia Commons — Dijkstra: Hamilton Richards, CC BY‑SA 3.0 · Rabin, Cook: Andrej Bauer, CC BY‑SA 2.5 · Scott: George M. Bergman, CC BY‑SA 4.0 · Hoare, Sifakis: Rama, CC BY‑SA 2.0 FR · Pnueli: David Monniaux, CC BY‑SA 1.0 · Clarke: Dennis Hamilton, CC BY 2.0 · Emerson: E. Allen Emerson, CC BY‑SA 4.0 · Lamport: lamport.org, free use
Challenge 3 — our proofs are local to one input
Local robustness proofs start from the image we tested.
A flying drone meets unseen inputs every frame — it can’t pause mid‑air to verify each one.
Can a guarantee generalise from the photos we tested to the next photo?
2024: the year the big prizes went to machine learning
“for foundational discoveries and inventions that enable machine learning with artificial neural networks”. Hopfield network (1982): 30 nodes, 435 connections. Boltzmann machine (1985). Hinton also holds the 2018 Turing Award.
Half “for computational protein design”; half “for protein structure prediction”. AlphaFold2: structures for nearly all ~200 million known proteins; at CASP14 (2020), median backbone error 0.96 Å against 2.8 Å.
“for developing the conceptual and algorithmic foundations of reinforcement learning”. Temporal‑difference learning (Sutton, 1988); the textbook (1998). The paradigm behind the tokamak and ANYmal controllers of slide 16.
“…when we create digital beings that are more intelligent than ourselves. We have no idea whether we can stay in control.”
Answer 2 — input‑agnostic certificates
each sign: 1,000 noise samples → its own local certificate
The tested images become random samples themselves — a second scenario‑approach bound covers unseen inputs: images nobody has seen yet.
Answer 3 — runtime monitoring
A verified controller is flying — but its proof was made against a model of the world. On board, every split‑second, the monitor checks model against reality.
The moment they diverge — the world doing something the model never promised — a second controller steps in and corrects the course.
We flew it — a union of neural control barrier certificates, in our cluttered two‑room lab, through a 90 cm doorway. With the monitor: 0 of 4,810 states left the certified set. Without it: 177.
Fig. 3, work under review
“Recommendations to my fellow AI scientists”
the fine print under the fourth line: “Use RL only when planning doesn’t yield the predicted outcome, to adjust the world model or the critic.”
“IF YOU ARE INTERESTED IN HUMAN‑LEVEL AI, DON’T WORK ON LLMs”
the last line of the slide — verbatim, and red in the original