4 ms·
> ... but I am not aware of actual (direct) use of Coq in the industry (but would be interested to learn of any). The first EAL7 certified smart card certifica
by yaantc 11y ago
> ... but I am not aware of actual (direct) use of Coq in the industry (but would be interested to learn of any).
The first EAL7 certified smart card certification used coq, see:
https://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pdf https://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pd...
- pron 11y agoOh, wow, they have verified a (JavaCard) JVM. Impressive! Thanks. They mention > 117,000 lines of Coq with > 1600 proofs to get EAL7 for the JVM.
- brohee 11y agoThis link is about an EAL4+ evaluation
- wolfgke 11y agoIf you read slide 4, you'll see that the SIM card was evaluated at EAL4+ level and the design of the Java Card System at EAL7 level.