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.