Languages that make correctness a property you can check, not a hope you carry.
A current focus, and the threads that lead up to it.
AI × Formal Methods
Verifying what AI builds. AI is rapidly becoming a coauthor of the software running our systems. Formal methods give us a way to keep that software trustworthy — checking the code AI produces, constraining what it can produce, and giving humans a precise account of what the resulting systems actually do.
Scaling formal methods with AI. Verification has historically been bottlenecked by the human labor of writing specifications, invariants, and proofs. Modern AI lowers that cost dramatically — and pushes formal methods from a boutique discipline toward a tool that can reach the security- and reliability-critical infrastructure already in production.
Together, the two threads turn formal methods into something that scales with the software it's meant to keep honest.
I lead this work at Galois as principal investigator on DARPA PROVERS (AI + formal methods for high-assurance development), DARPA PWND2 (provably weird networks), ARPA-H UPGRADE (hospital IoT cybersecurity), and 5STARS (multi-domain network resilience).
Foundations the current work builds on — programming languages, type systems, and verification for software and networks.
Fast Symbolic Verification for NetKAT
A decade after NetKAT gave network programming a sound equational theory, KATch makes its verification queries practical at scale. New data structures and symbolic algorithms — including a backward procedure that produces precise counter-examples when equivalence fails — decide reachability, slice isolation, and other network-wide properties on real-world topologies in well under a second, orders of magnitude faster than prior approaches.
With Mark Moeller, Jules Jacobs, Olivier Savary Belanger, David Darais, Steffen Smolka, Nate Foster, Alexandra Silva.
A Theory of Reprogrammable Packet-Processing Pipelines
In a software-defined network, a central controller computes the policy that distributed switches enact. As conditions change, the controller updates rules on the fly. We built a language for targeting reconfigurable packet-processing hardware and a proved-correct compiler that lowers a virtual pipeline onto heterogeneous back ends — grounded in NetKAT's sound equational theory for program transformations.
With Carolyn Anderson, Nate Foster, Arjun Guha, Michael Greenberg, Jean-Baptiste Jeannin, Dexter Kozen, David Walker.
Verified SDN Controllers
Software-defined networking promises rapid innovation by shifting intelligence from switches into software — but software is notoriously error-prone, and SDN bugs can become network vulnerabilities. Cocoon gives engineers a declarative specification language for packet-forwarding properties, embedded in a richer network-design language. It compiles controller programs to Boogie and checks whether the implementation satisfies its spec.
With Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Nina Narodytska, Douglas B. Terry, George Varghese.
Practical Verification for Programmable Data Planes
P4 lets network operators program the data plane itself — and that programmability needs a way to ask whether the resulting forwarding behavior is correct. p4v is a verifier that scales to production-sized P4 programs and has been used to catch real bugs in real switches. The work targets a sweet spot: enough expressivity to reason about realistic programs, enough automation to fit into an engineer's workflow.
With Jed Liu, William Hallahan, Milad Sharif, Jeongkeun Lee, Robert Soulé, Han Wang, Călin Cascaval, Nick McKeown, Nate Foster.
Optimized JavaScript
JavaScript runs everywhere, but its runtime story is a trade-off: just-in-time compilation is fast and memory-hungry; interpretation is lean and slow. SJSx cuts memory use with type-directed ahead-of-time compilation while staying performance-competitive with modern JITs. Getting there required a novel type-inference algorithm for a system with objects, structural subtyping, prototype inheritance, and first-class methods.
With Satish Chandra, Colin Gordon, Jean-Baptiste Jeannin, Manu Sridharan, Frank Tip, Yong-Il Choi.
Error Explanation for Type Inference
Type inference is wonderful when it works; when it fails, the error messages can be opaque, pointing far from the real source of the problem. Hobbes extends existing inference algorithms to produce explanations based on correcting sets — a minimal set of constraints that, if fixed, would let the program type-check. By piggy-backing on the existing inference engine, it stays fast and easy to adopt.
With Satish Chandra, Calvin Loncaric, Manu Sridharan.