Grand Challenge 3

From elections to energy grids, society depends on computers that must be safe, secure, and reliable: not just 90% or even 99% of the time, but every time.

That’s where verification comes in: using math to prove software always behaves as intended. In the lab, verification has been shown to produce applications that are dramatically safer and more reliable. But real-world code is so complex, most of it can’t be fully verified today, and the rise of unpredictable AI and “vibe coding” only raises the stakes. Allen School researchers are working to make verification practical across the stack — from chips and compilers, to cryptographic protocols and ML-powered apps.