The implementations uses exact rationals numbers. So there are no issues with numerical errors. We can do all geometrical operations exactly.

Many performant implementations have a separate layer that tries to use floats to decide inequalities and fall back to higher precision when floats are not sufficient. As I understand, this layer can be separated from the geometrical predicates we need (what I mean by predicate is for example deciding which side of a plane a point is), so we could formalize that arithmetic layer separately using axioms on floating point numbers and then plug it in the existing code. I think we could do that and still provide exact outputs and prove the same spec we have right now and the performance should increase a lot, since most of the computations right now is computing all these predicates exactly.

I would not say numerical stability is the one enemy of CSG. See the special cases https://github.com/schildep/verified-3d-mesh-intersection#sp... and bugs in an alternative C++ implementation that also used exact rationals mentioned in https://github.com/schildep/verified-3d-mesh-intersection#co....

Also note that many implementations don’t even try to treat special geometrical cases correctly (for example they „cheat“ by using something called simulation of simplicity which provides some guarantees against some bugs, but at the expense of not treating the cases exactly correctly which can lead to artifacts).

Moving to exact predicates on top of floating point numbers would be a big speed boost. CGAL does this.