This presumes that checking composes which may not if you have orthogonal checker implementations. You might end up risking accepting an invalid program because part of it is valid under one checker, part under another, but the combination isn't actually valid. But maybe that's not actually possible in practice.
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).
