Verificação formal para zkVMs: extrair restrições que o verificador verifica, depois executar um verificador sobre essas restrições. Primeiro, verificar circuitos não determinísticos, depois verificar propriedades específicas. O mesmo processo escala para sistemas tão complexos quanto zkVMs.