This is the first post in a series on how to prove that Jasmin programs are correct with respect to a high-level specification written in EasyCrypt. The examples used in this posts are taken from the correctness proof of the XMSS signature scheme, which is available here.
Overview
