Not really shifted. If you think about it, a bug in the proof will require a bug in the code. This visibility is a good thing. Overall, note that the critica

Not really shifted. If you think about it, a bug in the proof will require a bug in the code. This visibility is a good thing. Overall, note that the critical code, such as the microkernel itself, is small (kLoC wise) to begin with, which minimizes the odds a bug will go undetected for long.