Por que o Rocq é melhor que o Lean para verificação de programas

• Embora o Lean esteja claramente em ascensão na formalização matemática, para verificação de programas executáveis o Rocq se encaixa melhor, com coindução nativa, vários caminhos de extração e um ecossistema de verificação acumulado
• O Rocq declara codados com CoInductive e CoFixpoint, verifica guardedness e depois extrai para código com avaliação preguiçosa, enquanto no Lean é preciso escolher entre codificações em biblioteca, iteradores, Thunk ou partial def
• O verificador de tipos indutivos aninhados do Lean rejeita algumas relações de verificação que o Rocq aceita; no caso do esquema JSON, é preciso dividir uma prova de Forall₂ em várias relações e preparar um princípio de indução separado
• O Rocq oferece caminhos de extração de programas como OCaml, Haskell, Rust, C++, WebAssembly etc., além de bases de verificação como Iris, CompCert e Interaction Trees, permitindo ligar a lógica verificada de jogos reais a código executável
• Até agentes de IA conseguem escrever código em Rocq quando há documentação e exemplos; para migrar para Lean, seria necessário substituir não só as definições, mas também o pipeline de extração, bibliotecas e até o histórico regulatório e institucional, então no trabalho atual isso traz pouco ganho prático

---

Comparação com base em verificação de programas

• O objeto de comparação não é a formalização matemática, mas sim a verificação de programas; na matemática, o Lean de fato tem impulso de crescimento
• “Melhor” não significa superioridade absoluta, mas sim que o Rocq se ajusta melhor ao trabalho realizado no momento
• Com o aumento do interesse pelos resultados da IA em matemática e pelo Lean, o autor passou a receber com frequência perguntas sobre por que continua usando Rocq, e o argumento parte dos slides de uma keynote sobre LangSec

Tipos coindutivos nativos e cofixpoint

• O que o coinductive do Lean oferece

  • O suporte a predicados coindutivos, desenvolvido por Wojciech Różowski e Joachim Breitner no Lean FRO, foi incluído no comando coinductive do Lean 4.25
  • Esse recurso é útil para bissimulação e provas coindutivas, mas não fornece cofixpoints executáveis em Type nem programas extraíveis
  • CoInductive e CoFixpoint do Rocq fornecem diretamente codados (codata) executáveis em Type
  • O Lean não tem uma declaração de kernel correspondente, então é preciso usar funções e estruturas comuns ou codificações em biblioteca

• Restrições de declaração do QPFTypes

  • O QPFTypes, de Alex Keizer, é um pacote de prova de conceito para codados gerais, que gera destructor, corecursor e princípios de bissimulação a partir de especificações codata
  • Diferentemente de CoInductive do Rocq, trata-se de uma codificação em biblioteca, não de uma declaração de kernel
  • Os exemplos usam uma toolchain fixada na versão então mais recente com suporte, Lean 4.25.0
  • No Rocq, as três declarações comuns a seguir não funcionam no QPFTypes
    • Codados sem parâmetros falham por um bug de implementação
    • Declarações coindutivas mútuas como tree e forest não são suportadas por causa das restrições do bloco mutual do Lean
    • Famílias coindutivas indexadas como istream, em que o índice de clock avança a cada etapa, não são suportadas por limitações do próprio QPF
  • Padrões coindutivos indexados também aparecem em protocolos, etapas, tamanhos e máquinas de estado, mas ao sair do escopo simples, não mútuo e não indexado do QPFTypes, é preciso usar diretamente a API de baixo nível MvQPF.Cofix.corec e bisim, ou então a implementação se torna inviável
  • O Rocq também tem um verificador de guardedness difícil de lidar, mas esses casos podem ser declarados sem codificação adicional
  • Paco e coinduction, de Damien Pous, dão suporte a predicados coindutivos e provas de relações, mas não substituem CoFixpoint para programas

• Diferença nos programas extraídos

  • O cofixpoint nativo do Rocq é extraído como um valor OCaml preguiçoso de verdade
  • O unfold_cotree da game tree library vira uma árvore envolta em Lazy.t e uma função recursiva de geração preguiçosa
  • O resultado fica próximo de uma estrutura de árvore preguiçosa que uma pessoa escreveria manualmente
  • No QPFTypes, a construção e a observação passam por MvQPF.Cofix.corec e MvQPF.Cofix.dest, e o programa extraído também mantém a representação generalizada de Cofix
  • BadCoinduction.lean inclui Colist, Cotree, a interface gerada, casos de falha com codados sem parâmetros, mútuos e indexados, além do commit do QPFTypes e dos comandos para reprodução

Alternativas disponíveis no Lean

• Streams e iteradores

  • O Stream' da mathlib é uma função Nat → α
  • É possível calcular o elemento na posição n, e ele fornece corecursor, extensionalidade, bisimulation e lemas auxiliares de coindução
  • Porém, ele não é um construtor preguiçoso cujo tail é outro stream, nem resolve codados mútuos ou indexados arbitrários
  • Uma máquina de estados que usa estado explícito e uma função step também pode atuar como corecursor
  • O Iter do Lean é uma interface sequencial que calcula um passo por vez sob demanda
  • Iteradores podem ter provas de Productive garantindo geração de valor ou término, e Iter.repeat já fornece isso
  • Para iteradores definidos pelo usuário, é preciso fornecer manualmente a interface step, invariantes e, quando necessário, provas de produtividade
  • O CoFixpoint do Rocq verifica a guardedness das chamadas recursivas e retorna valores coindutivos sem exigir um trabalho extra de conexão entre a máquina de estados e a sequência

• Thunk, partial def, unsafe def

  • O Thunk do Lean calcula quando é forçado pela primeira vez no código compilado e armazena o resultado em cache, mas não fornece coindução
  • Na lógica, ele aparece como Unit → α, então a definição inteira pode ser usada em provas, mas o cache não é visível
  • Ele também não permite recursão nem verifica se a recursão eventualmente produz um construtor
  • O código extraído do Rocq também usa lazy evaluation em tempo de execução, mas primeiro passa pela verificação de guardedness
  • partial def pode executar o corpo recursivo, mas na lógica só resta uma constante opaca
  • Como não verifica terminação nem produtividade, ele permite tanto produtores de naturais quanto produtores que entram imediatamente em recursão infinita
  • unsafe def também pode ser executado, mas não pode ser referenciado em declarações theorem-safe
  • O MLList do Batteries combina uma implementação preguiçosa unsafe privada, uma interface pública opaca e produtores fix e iterate escritos com partial def
  • Esses produtores não podem ser unfolded em provas como um cofixpoint observável do Rocq
  • partial_fixpoint preserva equações, mas não aceita recursão que combine construtores e thunk
  • QPFTypes fornece corecursor e princípios de bisimulation, evitando a opacidade, mas ao custo de uma representação Cofix generalizada e restrições nas declarações

Programas com efeitos e que não terminam

• Interaction Trees representam programas com efeitos e potencialmente não terminantes como árvores coindutivas
  • Com a mesma árvore, é possível escrever, interpretar e extrair programas, e normalmente provar equações, incluindo weak bisimulation
• Stream' e Iter fornecem apenas sequências, então não conseguem expressar a continuação de ramificação necessária para efeitos
• Ao executar árvores de efeitos com Thunk e partial def, os produtores recursivos se tornam opacos para provas, e para dar suporte conjunto a computação e prova é necessário um encoding de biblioteca para codados
• O lean4-itree do MIT PLV implementa Interaction Trees com a álgebra final PFunctor.M da Mathlib
• PolyFun adiciona handlers, procedimentos recursivos, rastros de execução, strong/weak bisimulation e provas das leis de monad e iteration
  • É possível calcular e provar sobre árvores no Lean, mas elas ainda são M-types codificados em biblioteca
  • Não há declaração nativa de codados, e permanece uma representação geral em vez de programas preguiçosos diretos
• HITrees também não contorna essa limitação
  • Como o Lean não tem tipos coindutivos nativos, ele não usa a abordagem de Delay-monad coindutivo de ITrees
  • As árvores são indutivas, e a não terminação se torna um efeito recursivo de ordem superior
  • O cálculo recursivo ganha significado quando um handler interpreta o efeito, em vez de ser uma árvore infinita observável e expansível
  • É possível executar por interpretação monádica e provar por interpretação de máquina de estados, mas a teoria equacional de HITree não fornece as equações gerais de unfolding recursivo
• O Rocq oferece em um único fluxo declaração de codados, produtores guarded, raciocínio baseado em observação e extração direta de código preguiçoso

Tipos indutivos aninhados e predicados

• Caso de validação de esquema JSON

  • O Lean permite várias definições indutivas aninhadas, mas rejeita algumas definições aceitas pelo Rocq
  • Essa diferença foi usada em A Rose Tree Is Blooming e pode ser reproduzida com um caso menor de esquema JSON
  • Tanto JSON quanto o próprio esquema podem ser definidos sem problemas em ambas as linguagens
  • Na validação de esquema de objeto, é preciso verificar em pares se os nomes dos campos coincidem e se cada valor JSON é válido para o subesquema correspondente
  • O Rocq pode armazenar a igualdade dos nomes e a validação recursiva em uma única derivação de Forall2
  • O Rocq 9.0 rejeita lambda com tuple-pattern em torno de ocorrências recursivas como violação de strict positivity, mas compila ao usar projection em vez de pattern
  • O Lean 4.32.1 rejeita o And interno como um tipo de dado indutivo aninhado inválido quando uma ocorrência recursiva passa por Forall₂ e And no mesmo construtor de objeto
  • Ele permite Forall₂ ParRed, recursão direta por meio de And·Exists e formas adjacentes como Forall₂ (fun sf jf => Valid sf.2 jf.2)
  • Forall₂ (Eval env), em que o parâmetro de relação captura a variável local do construtor env, falha já na etapa de Forall₂

• Formas de contorno e custo das provas

  • No Lean, a validação de objeto pode ser dividida em duas derivações de Forall₂
    • uma preserva a igualdade dos nomes dos campos
    • a outra preserva a validação recursiva dos valores correspondentes
  • Sem índices separados nem provas de comprimento, ainda é possível manter a estrutura da lista e provar estruturalmente a remoção da head, mas é preciso decompor ambas as derivações
  • Ao separar a relação, perde-se o objeto de prova único que reúne cada igualdade de nome e validação recursiva como um par
  • É possível restaurar essa união com uma relação mútua ValidFields, mas a tática induction do Lean não dá suporte a tipos indutivos mútuos, e o recursor gerado também exige um motive para cada relação
  • Criar um teorema de indução definido pelo usuário pode ocultar essa configuração
  • O Rocq mantém a representação padrão de Forall2 e, quando é necessária uma definição mútua, pode gerar um princípio combinado com Scheme
  • O Lean também pode expressar a mesma proposição sem codificação baseada em índices, mas exige reorganizar declarações e criar mais aparato de prova
  • O arquivo completo de comparação está em NestedPain.v para Rocq 9.0.0 e NestedPain.lean para Lean 4.32.1, e as falhas esperadas no Lean são verificadas na compilação com #guard_msgs

• Princípios de indução mais fortes para argumentos aninhados

  • Em provas que exigem hipóteses por elemento de dados aninhados, como quando Term contém list Term, ambos os sistemas precisaram de um recursor mais forte
  • O Rocq 9.2 gera hipóteses de indução para argumentos aninhados quando o predicado e o teorema All são registrados para o tipo de nesting
  • A biblioteca padrão não registra isso por padrão, então é preciso adicionar uma linha Scheme All for list. antes da declaração de Term
  • Os Term_ind e Term_rect gerados obtêm a hipótese list_all Term P l no caso app, e o corpo chama list_all_forall
  • Ao adicionar Scheme All for Forall2., ParRed_ind também passa a fornecer hipóteses de indução para a premissa Forall2 ParRed args args'
  • Sem esse registro, aparece o aviso [register-all] junto com os princípios fracos já existentes
  • No Lean, ainda é necessário providenciar manualmente um recursor forte

Opções de extração de programas

• O toolchain padrão do Lean compila por meio do seu próprio runtime, o que é vantajoso ao criar bibliotecas Lean e quando o desenho do runtime se encaixa bem
• O lean-zip verificado por Kim Morrison pode até compactar mais rápido do que o miniz_oxide puro em Rust, o que mostra um desempenho impressionante
• No entanto, o Lean não oferece vários backends alternativos de extração, e o pipeline de compilação atual não tem prova de correção de ponta a ponta
  • Problemas raros como o bug de runtime encontrado por Kiran Gopinathan podem acontecer
  • O código gerado é especializado para o runtime e não foi projetado para ser lido por humanos
• O Rocq tem vários caminhos com diferentes compromissos entre base de confiança e legibilidade
  • OCaml·Haskell·Scheme
  • pipeline verificado de extração para Malfunction
  • Rust
  • Elm
  • Clight e WebAssembly via CertiRocq, embora parte disso ainda esteja em desenvolvimento
  • extração para C++ do Crane, voltada a código gerado de alta legibilidade

Jogos que executam lógica verificada

• No Rocq, após verificar mecanicamente propriedades do mesmo código-fonte do programa executável, a lógica e o event loop são extraídos para C++ com o Crane e conectados ao SDL2 com rocq-crane-sdl2

• Rocqman

  • Rocqman prova as transições de estado do jogo usadas pelo frame loop
    • a pontuação não diminui
    • vidas e colecionáveis restantes não aumentam
    • estados finais são pontos fixos de tick
    • transições de pausa e tela de encerramento são verificadas

• Rocqsweeper

  • Rocqsweeper prova as regras do Minesweeper e a camada de entrada
    • o primeiro clique é seguro
    • a marcação com bandeira preserva minas e dados de adjacência
    • o flood fill preserva minas e não aumenta casas seguras ocultas
    • o cursor não sai dos limites
    • eventos de mouse são interpretados como a célula esperada

• Reversirocq

  • Reversirocq usa a IA coindutiva alpha-beta da game tree library, com regras de Reversi adicionadas por Charles C. Norton
  • Os teoremas tratam da enumeração de jogadas legais e dos resultados do jogo, ligando alpha-beta e minimax no prefixo finito explorado

• Limite da verificação

  • O limite da prova termina no código-fonte em Rocq; SDL, Crane, o C++ gerado e o runtime nativo não estão incluídos
  • Dentro desse limite, são provadas propriedades da lógica realmente executada, e não de um modelo separado do programa executável

Ecossistema de verificação de programas do Rocq

• Abstrações para representar programas

  • Interaction Trees: representam programas com efeitos e potencialmente não terminantes como árvores coindutivas de eventos externos, fornecendo semântica denotacional e raciocínio equacional para código não puro
  • Choice Trees: adicionam escolhas internas não determinísticas para modelar sistemas não determinísticos, como concorrência

• Frameworks de verificação de programas

  • Iris: framework de lógica de separação concorrente de ordem superior para programas com estado e concorrência
  • Iris-Lean também evolui rapidamente e oferece muitos recursos, mas não foi usado de forma tão ampla quanto o Iris do Rocq
  • CFML: importa código-fonte OCaml para o Rocq, gera characteristic formulas e fornece táticas para especificações em lógica de separação de ordem superior
  • Perennial: framework baseado em Iris para verificar concorrência, armazenamento seguro contra falhas e sistemas distribuídos, conectado a programas executáveis de um subconjunto de Go por meio do Goose
  • VST: o Verified Software Toolchain, que prova a correção funcional de programas em C com base na semântica do CompCert
  • BRiCk: lógica de programas e cadeia de ferramentas para programas C++ reais

• Ferramentas com backend ou componentes em Rocq

  • Frama-C: plataforma de análise e verificação dedutiva de C que pode enviar obrigações de prova ao Rocq
  • Why3: envia objetivos de sua própria linguagem para vários provadores e pode exportar obrigações de prova interativas para o Rocq
  • Cerberus: semântica formal executável de um grande subconjunto prático de C, com implementação em Rocq para o modelo de memória CHERI C

• Semântica de linguagens reais e compiladores verificados

  • CompCert: compilador otimizador de C formalmente verificado
  • Vellvm: fornece uma especificação em Rocq e uma semântica abstrata de LLVM IR, além de um interpretador executável cuja refinação é provada
  • Vélus: compilador verificado de Lustre para Clight do CompCert
  • WasmCert: semântica formal mecanizada do WebAssembly
  • JSCert: semântica formal de JavaScript que acompanha a especificação ECMAScript 5

• Verificação leve baseada em tradução

  • hs-to-coq: traduz código-fonte Haskell para Rocq
  • rocq-of-ocaml: traduz código-fonte OCaml para Rocq
  • rocq-of-python: traduz código-fonte Python para Rocq
  • rocq-of-rust: traduz código-fonte Rust para Rocq
  • Aeneas: transforma Rust que passou no borrow check em modelos de funções puras para verificação, e também oferece suporte ao Lean como destino

• Síntese de programas e parsing

  • Fiat Crypto: deriva aritmética criptográfica de alto desempenho, utilizável em navegadores e bibliotecas TLS, de forma correct-by-construction
  • Rupicola: ferramenta de compilação relacional que converte programas funcionais Gallina de baixo nível em programas imperativos Bedrock2
  • Narcissus: deriva encoder e decoder correct-by-construction de formatos binários
  • Verbatim: lexer verificado baseado em expressões regulares
  • CoStar: parser verificado baseado no algoritmo ALL(*)

• Estado de manutenção

  • Alguns projetos não são mantidos ativamente, mas foi possível reconstruí-los e executá-los delegando isso a agentes
  • Mesmo que seja possível portar rapidamente para Lean um elemento necessário, os recursos acumulados e o histórico de uso de todo o ecossistema não são transferidos automaticamente

Histórico regulatório e de certificação

• Não há experiência direta de certificação em aceitação regulatória, embora isso possa ser um fator mais importante especialmente para profissionais na Europa
• A ANSSI da França publicou critérios para o uso do Rocq em avaliações Common Criteria
• O CompCert informa que foi qualificado com sucesso para o computador MFC_NG das aeronaves ATR 42/72 de 2026, por meio de um trabalho realizado pela AbsInt sob orientação da Airbus
• Não se sabe quais requisitos um port para Lean precisaria atender no mesmo contexto, e mesmo um port limpo não herda automaticamente o histórico de certificação existente

Agentes de IA e custo de transição

• Ao contrário da premissa de que agentes de IA só escrevem bem em Lean, eles também conseguem escrever código em Rocq de forma adequada
• O Rocq existe desde o fim dos anos 1980 e acumulou muito código e documentação
• Os modelos atuais se adaptam bem até a linguagens menos familiares quando recebem documentação e exemplos, então conhecer apenas linguagens populares não é uma justificativa de longo prazo para trocar de proof assistant
• Também há trabalhos sérios de verificação de programas em Lean, como mvcgen e Velvet
• Para migrar o trabalho atual para Lean, seria necessário reconstruir definições e substituir o pipeline de extração, bibliotecas e histórico institucional, portanto, neste momento, o Rocq é mais adequado