One of the points of concern in the Tezos code is integer overflows. To ensure that no overflow occurs, the development team created abstractions over the native OCaml integers. This makes it possible to check if an overflow happened and to return an error if that is the case.
But how to be sure that such abstractions are correct? In this post, we will explain how integer arithmetic can be verified using Coq.