Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software
- D. Ahman ,
- Karthik Bhargavan ,
- Barry Bond ,
- Jay Bosamiya ,
- Chris Brzuska ,
- Antoine Delignat-Lavaud ,
- Cédric Fournet ,
- Aymeric Fromherz ,
- Sydney Gibson ,
- Chris Hawblitzel ,
- Cătălin Hrițcu ,
- Markulf Kohlweiss ,
- Guido Martínez ,
- Haobin Ni ,
- Bryan Parno ,
- Jonathan Protzenko ,
- Tahina Ramananandro ,
- Aseem Rastogi ,
- Exequiel Rivas ,
- Nikhil Swamy ,
- Santiago Zanella-Béguelin
ACM Transactions on Programming Languages and Systems |
Project Everest began at Microsoft Research in 2016, aiming to spur research in program verification to produce industrial-grade software. In collaboration with INRIA and Carnegie Mellon University, Project Everest’s goal was to produce drop-in verified replacements of secure communications software used in the HTTPS ecosystem, including TLS, the underlying cryptography, and related subprotocols. Now, almost a decade later, we reflect on the project, sharing both its successes and failures, and look ahead to the next decade of program verification research.