[nano_o]

Also, it seems they proved a behavioral equivalence property: any user-space program has exactly the same behaviors when running on the C+assembly implementation of the OS (6500 lines) and when running on the abstract machine specified by the high-level specification of the OS (450 lines). Their specification also includes liveness properties (e.g. no deadlocks or livelocks).

For comparison, seL4 has verified behavioral refinement between implementation and specification, termination of all syscalls, and several security properties (non-interference and information-flow properties among threads), worst case execution times, and other things; but, seL4 does not support fined-grained concurrency.