> has the specification been proved to be bug-free?
Yes for SeL4, but no for a bunch of other systems advertised as "having been proven to be correct". Which often sadly only means "implemented as specified" but not "implemented as specified and proven to have the right properties".
then:
> has the specification been proved to be bug-free?
Yes for SeL4, but no for a bunch of other systems advertised as "having been proven to be correct". Which often sadly only means "implemented as specified" but not "implemented as specified and proven to have the right properties".