One of the best in the field. :) Although I think they just have dev assurance. Not total high assurance. An early one with total was GEMSOS by Schell, one of INFOSEC's founders:
A comparable one for dev assurance, but maybe easier to emulate, was CompCert. Testing of it against many other compilers validated formal verification gave best reliability.
That's right: a formal specification, formal security model, and proof the spec implements it. An implementation formally proven to implement that spec will then posses the security property unless done in by stuff not covered by that model.
Which is where EAL6/7's other assurance activities come in.
