I love that people can and do undertake this type of thing. It's good for the development and improvement of the state of the art, continued research is valuable purely as research and I don't really want it to stop.
It's also so far removed from pragmatic non-academic reality that it's insane.
SYSGO is a pretty pragmatic non-academic company that has existed in reality since 1991.
Three years, and found two bugs?
Keep in mind that PikeOS was already used in automotive and avionic systems, so it was already rigorously developed and tested. It is indeed quite a testament to the quality of the product.
Let alone the obvious risks around the complexity, completeness and accuracy of a model that took so long to develop.
This model was developed exactly because existing models and theories could not be applied to real-life systems such as the PikeOS microkernel. The papers I linked earlier explicitly discuss managing the complexity.
The EAL link is interesting though, hadn't come across that before.
I hope you are not working on safety-critical systems then.
I suspect most of the systems I work on would qualify at EAL4 but the cost of demonstrating it would kill their commercial value; we'd discontinue the products rather than waste the money.
In the industries where this currently matters, it is the same: you either get your certification (this, or another one depending on the field) or you discontinue the product since you are not allowed to sell it at all (or rather: your prospective customers are not allowed to use it).
EAL7? Comically that's more likely - but only for key algorithms we develop and use. A whole system? Could take down the company..
Another part of the project was about formalising the MILS (multiple independent levels of security) architecture, which enables you to compose components certified at different levels (EAL or otherwise) in a way that does not bring everything down to the level of the least certified component.
And indeed, you will almost never certify an entire system at EAL7.