Verificação formal para zkVMs: extraia as restrições que o verificador verifica e depois execute um verificador nessas restrições. Primeiro, verifique circuitos não determinísticos, depois verifique propriedades específicas. O mesmo processo escala para sistemas tão complexos quanto zkVMs.