Clean: Uma DSL Embutida e Framework de Verificação Formal para Circuitos ZK em Lean4

Pesquisadores desenvolveram Clean, uma linguagem específica de domínio (DSL) embutida e framework de verificação formal em Lean4 para construir circuitos de conhecimento zero (ZK). Circuitos ZK são propensos a bugs, e Clean visa melhorar a correção permitindo que os usuários definam circuitos em Lean4, especifiquem suas propriedades desejadas e os comprovem formalmente. Este projeto faz parte do Projeto de Verificação Formal zkEVM, com o objetivo de fornecer infraestrutura e ferramentas para a verificação formal de zkEVMs. Clean suporta quatro operações básicas para definir circuitos: witness, assert, lookup e subcircuit, e oferece uma interface monádica para melhor usabilidade. Seu núcleo é a estrutura FormalCircuit, que empacota de forma fortemente tipada a definição do circuito, as suposições, a especificação, as provas de solidez e completude. Circuitos grandes podem ser verificados formalmente substituindo recursivamente as restrições de subcircuitos por suas especificações (formalmente verificadas). O framework já verificou com sucesso circuitos simples como a adição de 8 bits, com planos futuros para adicionar mais gadgets de baixo nível, definir circuitos de funções hash comuns e construir uma máquina virtual mínima formalmente verificada para um subconjunto de RISC-V.