Provably Secure: Math Against Superintelligent Hackers

Byron Cook started his journey through formal verification with PhD work in formalizing the interface between CPUs and software. He then worked for many years at Microsoft Research, where he made important contributions in model checking, one of the first formal verification approaches to be scaled for serious industry impact. In 2014, he took a leap of faith, joining Amazon Web Services to lead a new effort in applying formal verification throughout the organization, to improve cybersecurity and system reliability. The project succeeded beyond all expectations, with formal methods now woven deep into how AWS builds and operates, and increasingly paired with AI to prove the correctness of systems at scale and AI itself. The AWS Automated Reasoning Group, founded by Byron in 2016, contributes across many business units to strengthen internal systems and build tooling that makes it easier for other organizations to apply formal verification, probably the largest buy-in to diverse formal verification by any company.

Noah Evans started his research career in systems software and high-performance computing at IBM and Bell Labs.  Later he joined the new formal-methods team being spun up at Sandia National Laboratory, one of several U.S. national labs charged with securing the nation’s nuclear stockpile.  The team found great success proving correctness and security of hardware and software, including in several projects he led, growing into one of the largest formal-methods teams in U.S. government-adjacent organizations.  He recently moved to Draper Laboratory near MIT, continuing to lead efforts applying principled techniques to cybersecurity in national defense.

Armando Solar-Lezama did undergraduate research in high-performance computing and started exploring formal methods in his PhD work, where his thesis reinvigorated the area of program synthesis, generating code from its mathematical requirements. In particular, he and his collaborators introduced the technique of program sketching, where automated tools fill in gaps left in code. He then joined the computer-science faculty at MIT. After quite some time making the case that “this stuff can really work,” the generative-AI boom made that point clear to everyone, and Armando has been helping make sense of the relative strengths and weaknesses of machine learning and logical methods, to create the next generation of tools that combine the two.

Adam Chlipala (moderator) lucked into working with computer theorem-proving tools during his PhD and has since focused on machine-checked proofs of correctness and security for programs. He wrote a popular introduction Certified Programming with Dependent Types to the Rocq Prover. After joining the MIT faculty, collaborations took him into applications in computer hardware, operating systems, high-performance computing, and applied cryptography. The last one has included a project Fiat Cryptography, which generates fast cryptographic software automatically with mathematical guarantees of correctness; it has been adopted by all major web browsers for small but important parts of their code for secure browsing. He is also cofounder of Nectry, a startup spinning out MIT research to support AI-assisted development of enterprise software with mathematical guarantees of security.