Also a C compiler (https://compcert.org/). I did exaggerate bit in saying that anything non-trivial is "nearly impossible".
However, both CompCert and sel4 took a few years to develop, whereas it would only take months if not weeks to make versions of both which aren't formally verified but heavily tested.
It takes years to develop a quality C compiler. I am a professional compiler writer and the difference between a toy compiler and a production compiler is vast.
It demonstrates that proving a full featured operating system, as complex as Windows 7 for example, is within the realm of possibility. It would just likely take a Manhattan project equivalent, with a truly unlimited budget.
However, both CompCert and sel4 took a few years to develop, whereas it would only take months if not weeks to make versions of both which aren't formally verified but heavily tested.