From their verification roadmap, it sure seems generous to refer to this as “formally verified”. They don’t prove anything important about the kernel clearly at

From their verification roadmap, it sure seems generous to refer to this as “formally verified”. They don’t prove anything important about the kernel clearly at all. Seems very disingenuous to describe it as they do since it lacks any of the merits of other formally verified kernels like seL4 and Tock.