True story: after arriving in Canada from the U.S, I was selected for a "special" search. They asked for my laptop, and asked me to enter the login password. I politely declined. I requested to speak to my corporate attorney (via my cell phone) and they refused. They asked again more forcefully, threatening me with arrest if I didn't give in. I gave in. (I'll only go so far to protect my employer's IP).
You should have seen the look on the poor inspector's face when it booted into Linux. He politely asked me how to search for porn on my computer. I taught him the "find" command.
There is nothing in the Common Criteria that specifies that an EAL7 system is "completely secure". It merely indicates that a great deal of evidence exists that the system meets its security function requirements, nothing more, nothing less. In Common Criteria, the actual security function requirements can be extremely weak, but to make EAL 7, a great deal of evidence must be presented to show that the extremely weak requirement was implemented correctly.
The "mathematically irrelevent industry certificate" of which you speak, Common Criteria EAL 6, does require formal analysis, and Integrity did have certain important security properties proved about it. Now, this L4 kernel set a much higher bar, in that it was proven correct, a super-set of what what proved about Integrity.
"I am, therefore I am." -- Akira