Comment by vlovich123

I’ll take your word for that although it feels like there may be other cases. Even still there is the subtle problem that bugs in the proof checkers now result in O(n^m) safety issues because an incorrectly accepted program is more likely to get through 1 of the borrow checkers (similar to how in a distributed system adding single points of failure results in exponentially decreasing reliability).