I.
Verifying what AI builds.
Bringing formal methods to bear on the software and systems AI now produces — so we can adopt AI-generated code without giving up the ability to check, constrain, and trust what it does.
Currently
My recent work sits at the meeting point of AI and formal methods — two directions of the same pairing:
II.
Scaling formal methods with AI.
Using AI to automate the human labor that has kept verification expensive — generating specifications, invariants, and proofs — so formal methods reach the security- and reliability-critical infrastructure already in production.
Leading
Principal investigator on four programs at Galois, spanning network resilience, healthcare cybersecurity, hidden-network defense, and high-assurance development.
DARPA · PROVERS
High-assurance systems at the speed of AI
Combining AI and formal methods to accelerate the development of high-assurance systems — raising the pace at which provably correct software can be built and deployed.
DARPA · PWND2
Provably weird networks
Formal models of emergent communication pathways — the "weird networks" hiding inside ordinary systems — to fundamentally improve trust in the security and safety of robust hidden communication channels.
ARPA-H · UPGRADE
Cybersecurity for hospital IoT
A multi-layered system that helps hospital IT teams make sense of complex medical IoT environments, automating security where possible and assisting human operators where it isn't.
DoD · 5STARS
Resilient networks across land, sea, air, and space
Improving network reliability, survivability, and resilience by providing proactive, real-time network monitoring for complex networks spanning land, sea, air, and space. 5STARS supports user-friendly threat-driven development by detecting and remediating incidents introduced by bugs, operator misconfiguration, and adversarial action.
About
I'm a Principal Scientist at Galois, Inc., where my work focuses on language-based modeling and verification of software systems and networks.
My research lives at the intersection of programming languages, type theory, formal methods, and network verification — building tools that let people state what a system should do and check that it actually does. Most recently, that work has expanded toward the pairing of AI and formal methods described above.
Before Galois, I was an Applied Scientist in the Automated Reasoning Group at Amazon Web Services. I earned my Ph.D. from Princeton in 2015, advised by David Walker.
Selected work
KATch: A Fast Symbolic Verifier for NetKAT
A decade on from NetKAT, KATch makes its verification queries practical at scale — symbolic algorithms that decide reachability and equivalence on real-world topologies in well under a second, orders of magnitude faster than prior approaches.
NetKAT: Semantic Foundations for Networks
A network programming language with a sound and complete equational theory, built on Kleene Algebra with Tests. The semantic foundation for much of the work that followed.
p4v: Practical Verification for Programmable Data Planes
A practical verifier for P4 programs that scales to production-sized data plane code. Used to catch real bugs in real switches.
Correct-by-Construction Networks Using Stepwise Refinement
The Cocoon project: a declarative language for network design where high-level specifications are refined, step by step, into deployable controllers — with formal guarantees preserved at each step.