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.

@article{paperbot3954,
  title = {Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software},
  author = {Danel Ahman and Karthikeyan Bhargavan and Barry Bond and Jay Bosamiya and Christopher Brzuska and Antoine Delignat-Lavaud and Cédric Fournet and Aymeric Fromherz and Sydney Gibson and Chris Hawblitzel and Cătălin Hrițcu and Markulf Kohlweiss and Guido Martínez and Haobin Ni and Bryan Parno and Jonathan Protzenko and Tahina Ramananandro and Aseem Rastogi and Exequiel Rivas and Nikhil Swamy and Santiago Zanella-Béguelin},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {48},
  number = {2},
  year = {2026},
  doi = {10.1145/3805702}
}