In this video, I demonstrate how to use Coq to prove the functional correctness of a piece of EVM bytecode against a specification.
I do not explain every detail but focus more on the intention why I do certain things and how I feel when I do things.