The Curious Engineer

All blogs / Compilers

Jonathan Protzenko

jonathan.protzenko.fr

Google Information Security Engineering (Seattle)

CompilersRustSecurityFunctional / PL theory

’19’20’21’22’23’24’25’26
Posts
14 from 4 Jan 2019 to 5 May 2026
Posting
now and then (1 in the last year)
Kind
personal blog
Feed
https://jonathan.protzenko.fr/feed.xml

2026 1

  1. A case study with Aeneas and jxl-rs

2025 2

  1. Eurydice: a Rust to C compiler (yes)
  2. 15,000 lines of verified cryptography now in Python

2024 2

  1. First alpha release of HACL* in Rust
  2. Rust verification and backwards compatibility

2023 3

  1. Verified Secure Group Messaging with MLS
  2. software
  3. research

2022 2

  1. 5 Years of Meta-Programming Cryptography
  2. wonderful collaborators

2020 1

  1. What’s new in Everest: Summer 2020

2019 3

  1. GitHub strange
  2. The EverCrypt verified cryptographic provider
  3. Generating C code that people actually want to use