Comment by nemo1618

That's the nice thing about the approach described in the blog: you use the same Rocq theorem for every binary (it just says "this binary doesn't crash") and then you express the property you want in your language of choice. For example, to prove that your compression algorithm round-trips, you would write something like assert(x == decompress(compress(x))).