Programming critical systems with proofs, a long-standing goal of computer science, is beginning to come within reach of modern programming languages and proof assistants. I provide a brief overview of recent accomplishments in this space, related to work in the F* proof assistant and Project Everest, one of its flagship applications. Programs developed in F* with proofs of correctness & security are now deployed in wide variety of settings, ranging from Microsoft Windows and Hyper-V, Microsoft Azure, the Linux kernel, Firefox, mbedTLS, and several other production systems.

I’ll also provide a general overview of research in programming languages and software engineering at Microsoft Research and the RiSE group, in particular.