Regarding fuzzing. It cannot find the special cases I listed in the readme, because these cases are very rare.

Yet with formal verification we can prove that the implementation actually satisfies the specification for all of infinitely many possible inputs.