Not surprised, Java vm is literally everywhere. From your credit card to sim, if it is a ic card then there is Java vm. It is almost universal language for mini embedded system for some reason I don't understand.

IIUC, it's because it's easier to rigorously prove the VM prevents classes of bugs (i.e. memory safety issues) and then reuse that VM in many places than it is to rigorously prove that many separate embedded systems not relying on the VM have independently avoided those bugs.

Is there an example of a JVM that has been proven correct in this sense?

I haven't heard of one.

I don't know specific details about the correctness of any particular VM, sorry. That was just the explanation I got from another engineer that apparently had experience in developing embedded java things.

> It is almost universal language for mini embedded system for some reason I don't understand.

Marketing-fueled hype.