Project Everest

Building and deploying provably secure communication software

News & features

In the news | Mozilla Security Blog

Traditionally, software is produced in this way: write some code, maybe do some code review, run unit-tests, and then hope it is correct. Hard experience shows that it is very hard for programmers to write bug-free software. These bugs are…

In the news | Microsoft Story Labs

At any point in time on any day of the week, Microsoft’s cloud computing operations are under attack: The company detects a whopping 1.5 million attempts a day to compromise its systems. Microsoft isn’t just fending off those attacks. It’s…

In the news | F* for the Masses

The work we do these days on F* is often in service of Project Everest. The goal of Everest is to verify and deploy a drop-in replacement for the HTTPS stack, the protocol using which you are probably reading this…

In the news | Quanta Magazine

In the summer of 2015 a team of hackers attempted to take control of an unmanned military helicopter known as Little Bird. The helicopter, which is similar to the piloted version long-favored for U.S. special operations missions, was stationed at…

Awards | Computer-Aided Verification (CAV)

Samin Ishtiaq will be receiving the 2016 CAV Award for the development of Separation Logic and for demonstrating its applicability in the automated verification of programs that mutate data structures. He is winning this award alongside Josh Berdine, a former…

Microsoft Research Blog

Jeannette M. Wing Photo credit: Scott Eklund/Red Box pictures By Jeannette M. Wing, corporate vice president, Microsoft Research “Think Bolder, Aim Higher” is a mantra I’ve been chanting since my arrival at Microsoft three years ago. I’ve wanted to encourage…