Do verified monokernels exist? You can say that a comparison is unfair, but what matters is the end result of "which system ends up with the fewest vulnerabili

Do verified monokernels exist? You can say that a comparison is unfair, but what matters is the end result of "which system ends up with the fewest vulnerabilities if/when it becomes widely used", and a formally verified microkernel seems like a strong bet on that front.