Jonathan Protzenko

Aeneas is a toolchain for verifying Rust programs, relying on a functional translation to Lean.

Perhaps the greatest surprise of the last two years was, for me, the realization that people not only care about compiling C to Rust (for obvious reasons, such as, ahem, memory safety) – they also care about compiling Rust to C!

In November 2022, I opened issue 99108 on Python’s GitHub repository, arguing that after a recent CVE in its implementation of SHA3, Python should embrace verified code for all of its hash-related infrastructure.

I recently wrote about ongoing efforts to retarget the compilation of HACL* from C to Rust.

Over the past few years, a lot of eyes in the software verification community have turned towards Rust.

Long gone are the days of my youth where AOL Messenger and IRC ruled online communication spaces… in this day and age, people use WhatsApp, Signal, Facebook Messenger, or even Instagram Messages (or so I am told).

For the past five years or so, I have been exploring, along with many other collaborators, the space of verified cryptography and protocols.

In a valiant attempt to wean myself off of doomscrolling, I thought I’d try to write a few blog posts this summer.

Earlier this year, I was paired up with my colleagues Chris, Tom, Madan and intern Danielle Gonzalez (from Rochester) for the annual Microsoft Hackathon.

Today, we’re announcing a preview release of EverCrypt, a verified cryptographic provider that offers a comprehensive collection of cryptographic algorithms.