EasyCrypt and Jasmin Tutorial, Šibenik 2022

This page is meant as an index to the helper material for the Summer School lecture on Machine-Checked Cryptography with EasyCrypt and Jasmin, which will take place on June 16th.

Contributors: Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Pierre-Yves Strub, Tiago Oliveira


Jasmin Files

EasyCrypt Files

Folder proof/example contains the EasyCrypt specs and proofs for the example:

Folder proof/aeslib contains the EasyCrypt specs and proofs for AES-NI:

Folder extraction contains the EasyCrypt code that is automatically generated from the Jasmin souces (the correctness and constant-time proofs then import these files):

Folder test contains the wrapper C files for executing the Jasmin examples:

Folder installation constains Docker and shell scripts to set up your own EasyCrypt and Jasmin environments. A pre-built Docker image with only the command-line tools can also be found here.


Make sure to edit the Makefile so that it can find easycrypt and jasminc.

Then, from root directory:

Calling Jasmin libraries from other programming languages

Fun Stuff

Getting support

The Formosa Zulip Server is the place to go. There is already a significant Q\&A back-log and your questions usually get answers in a short time.

Background reading

Prior editions of the tutorial