I don't think you're reading that quote right. "Trusted" doesn't mean "trustworthy". What the implementors were probably trying to explain to this poor techn

I don't think you're reading that quote right. "Trusted" doesn't mean "trustworthy". What the implementors were probably trying to explain to this poor technical writer is that they have proven that their kernel correctly implements the isolation policies they have formally specified - enabling it to separate (isolate) trusted (kernel level) from untrusted (user level) software.