About me

My name is Paul-Nicolas Madelaine, often shortened to PNM. My pronouns are he/him. I’m a research engineer working in the team Prosecco at Inria Paris.

My face
Fig. 1: My face
The picture I usually use as an avatar.
Fig. 2: The picture I usually use as an avatar, taken from BoJack Horseman


Other E-mail addresses linked to me.

Public online accounts


The team Prosecco specializes in the formal verification of cryptographic protocols and their implementation. I’m using the F* proof assistant to verify a constant-time high-performance software implementation of the AES cypher.

AES is usually computed at hardware level using specialized CPU instructions, to the benefit of side-channel resistance and performance. In some contexts a software implementation is still required though, and various tricks used to speed-up the computation create challenges when writing a formal proof of the code.

The code is built on top of Hacl*, a library of formally verified cryptographic primitives producing high-performance C code.

About this website

This website is built with Jekyll and Nix, source code is available here. It’s hosted on a bare-metal server at OVH. Certificates are issued by Let’s Encrypt. The domain name pnm.tf is registered at Gandi and the top-level domain .tf is administrated by AFNIC.