This is the last article of a series of blog post presenting our formal verification effort in ย Rocq/Coq to ensure the correctness of the type-checker of the Move language for Sui.
Here we show how the formal proof works to check that the type-checker is correct on a particular instruction, for any possible initial states. The general idea is to symbolically execute the code step by step on the type-checker side, accumulating properties about the stack assuming the type-checker succeeds, and then to show that the interpreter will produce a stack of the expected type as a result.