We present in this blog post the main properties that need to be formally verified in the circuits of a zkVM to consider it as secure.
The formal verification of zero-knowledge applications is considered a priority by Vitalik Buterin, the founder of Ethereum, among others. The website ethproofs.org lists zkVMs ready to run Ethereum, with formal verification of the code being one of the criteria to appear as 🟩 green.