In diesem Video zeige ich, wie man Coq verwendet, um die funktionale Korrektheit eines Stücks EVM-Bytecode gegenüber einer Spezifikation zu beweisen.
Ich erkläre nicht jedes Detail, sondern konzentriere mich mehr auf die Absicht, warum ich bestimmte Dinge tue und wie ich mich dabei fühle.