Note that the claims are about the kernel that computes the mesh intersection, not the web demo: While the kernel is formally verified, the UI and glue code (that call the kernel) are not. I once hit a bug that looked like there were holes in the resulting mesh: I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specification, to floats before sending them to the GPU. All geometry is happening inside the kernel, for which we know the specification holds.
> I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specification, to floats
Preserving the topology of mesh intersections while rounding the coordinates is a hard problem. In particular, it is only in 2020 that an algorithm was found that handles all the cases [1]. In practice, an efficient algorithm for that was published last year [2].
[1]: https://doi.org/10.1007/s00454-020-00202-2 https://hal.science/hal-02549290/file/DCG.pdf
[2]: https://doi.org/10.1111/cgf.70197 https://hal.science/hal-05242294/file/Snap-SGP-revised.pdf