JavaCard is also one of the few areas where high-assurance security use commercially. Names that come to mind are Kesterel Institute and Gemalto with EAL7-style

JavaCard is also one of the few areas where high-assurance security use commercially. Names that come to mind are Kesterel Institute and Gemalto with EAL7-style VM's with formal verification. Examples: https://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pdf https://www.commoncriteriaportal.org/iccc/9iccc/pdf/B2404.pd... http://www.kestrel.edu/home/projects/jcapplets/ http://www.kestrel.edu/home/projects/jcapplets/