Comment by waffenklang

Good example for the weaknesses of the 'formally verified' sale strategy. It may be formally correct, but the code is full of weaknesses, like no NULL checks, no out of bounds checks, one endless loop based on pointer arithmetic..

good and fast c code looks not like this.