[Cad] Formally Verifying a B-Rep kernel

[David Kaufman]

My understanding from our discussion last week is that writing a B-Rep
kernel is difficult primarily because there are tons of edge cases for
how objects can intersect each other and it's really hard to get them
all correct/test for all of them. If this is the main challenge then my
intuition is that it would be best solved by building a formally
verified b-rep kernel (and that perhaps it would take much less time to
write that way). Do any of you know if anyone has tried to write a
formally verified b-rep kernel or why not?