Dans cette vidéo, je montre comment utiliser Coq pour prouver la correction fonctionnelle d'un morceau de bytecode EVM par rapport à une spécification.
Je n'explique pas chaque détail mais me concentre davantage sur l'intention derrière certaines actions et sur ce que je ressens en les réalisant.