This provides a guarantee that the properties proved about the API actually hold for the real kernel, a degree of assurance which goes beyond even CC EAL7.
それにより、APIについて証明された属性が実際のカーネルでも保持されていることが保証でき、CC EAL7 をも越える保証の程度となっている。