Hacker News Reader

> and some of them do indeed require mathematical proof of correctness > (EAL6+ being a key standard)

Nitpick: EAL6 is still semi-formal, EAL7 is formally verified design and tested. EAL7 is very rare, on the CC certified products page [1] there are only 2 EAL7 certified products: a hardware diode, and a virtual machine OS.

[1] https://www.commoncriteriaportal.org/products/

View on HN

> Nitpick: EAL6 is still semi-formal, EAL7 is formally verified design and tested. EAL7 is very rare, on the CC certified products page [1] there are only 2 EAL7 certified products: a hardware diode, and a virtual machine OS.

You are definitely correct. Also, disclosure... I worked on that EAL7 Virtual OS. When I left it was only EAL6+, likely leading to my bias towards it.

Reply on news.ycombinator.com