Jonathan Protzenko

Jonathan Protzenko

@protz.bsky.social

I talk about Rust, verification, cryptography, programming languages… and pets

133 followers65 following7 posts

Jonathan Protzenko
@protz.bsky.social

This is what I've been driving for the past year! It's an exciting time, with Rust making its way into one of the most critical pieces of software: the core crypto library used in Azure and Windows. With Rust, formal verification becomes easier, and so far, no blockers to Rust adoption.

Microsoft Research@msftresearch.bsky.social

We're rewriting parts of Microsoft's SymCrypt cryptographic library in Rust to improve memory safety and defend against side-channel attacks, enabling formal verification while maintaining backward compatibility via a Rust-to-C compiler: msft.it/6011SU7Fc

Jonathan Protzenko
@protz.bsky.social

Friday blogging, about our journey replacing Python's built-in cryptography with verified code from HACL*. I'm very proud of this work: I wrote the first version in 2020, and along the way it had both research (ICFP paper) and industrial impact (Python). jonathan.protzenko.fr/2025/04/18/p...

jonathan.protzenko.fr15,000 lines of verified cryptography now in PythonIn 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 inf...

You are up to date.