Tessera
Folgen

Jonathan Protzenko

@protz.bsky.social

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

7 Posts128 Follower65 Folgt
Jonathan Protzenko@protz.bsky.social · last yr.

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 · last yr.

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

Three white icons on a gradient background that transitions from blue on the left to pink on the right. The first icon, on the left, is a microchip with a padlock in the center. The middle icon is a flowchart diagram with connected shapes. The third icon, on the right, consists of two angle brackets facing each other.
Jonathan Protzenko@protz.bsky.social · last yr.

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...

15,000 lines of verified cryptography now in Python

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 inf...

jonathan.protzenko.fr