Resumo Técnico: KVerus

Declaração do Problema

A verificação formal oferece a mais alta garantia de correção de software, mas permanece difícil de escalar para sistemas grandes e em evolução devido ao esforço manual substancial necessário para escrever provas, gerenciar dependências e adaptar-se a mudanças na cadeia de ferramentas. Embora os Modelos de Linguagem Grandes (LLMs) tenham mostrado promessa na automação da geração de provas, eles falham em configurações do mundo real com múltiplos módulos. Os autores identificam a causa raiz como a Lacuna Semântico-Estrutural: os LLMs operam sobre padrões semânticos de código, enquanto a verificação formal (especificamente em Rust usando Verus) é governada por dependências estruturais rígidas, implicações lógicas e regras de sintaxe precisas.

As abordagens atuais baseadas em LLMs sofrem de quatro limitações principais:

1. Falta de Compreensão Contextual: Incapacidade de raciocinar através de sistemas modulares para identificar componentes relevantes.
2. Descoberta Pobre de Lemas: Falha em descobrir e reutilizar lemas existentes, especialmente quando a documentação está incompleta.
3. Fragilidade à Evolução da Cadeia de Ferramentas: Incapacidade de adaptar-se quando as cadeias de ferramentas de verificação (por exemplo, Verus) são atualizadas, fazendo com que provas anteriormente válidas quebrem.
4. Problemas de Escalabilidade: Dependência de especificações globais frágeis e mantidas manualmente que não podem evoluir junto com grandes bases de código.

Metodologia: KVerus

Para superar a Lacuna Semântico-Estrutural, os autores propõem o KVerus, um sistema de verificação auto-adaptativo e aumentado por recuperação. O KVerus opera como um pipeline que constrói uma base de conhecimento dinâmica e a utiliza para gerar e refinar provas. O sistema consiste em quatro módulos principais:

1. Pré-processador (Pré-processamento de Código e Lemas)

• Grafo de Dependência de Metadados: Realiza análise estática profunda para construir um grafo direcionado tipado da base de código. Os nós representam objetos da linguagem (funções, tipos, traits) e as arestas representam dependências (tipo/estrutura e chamada/especificação).
• Extração de Código Dependente: Para uma função-alvo, percorre o grafo (até profundidade 3) para extrair definições, assinaturas e dependências relevantes entre arquivos, fornecendo uma visão estrutural holística além de um único arquivo.
• Extração de Lemas: Extrai assinaturas, pré-condições (requires), pós-condições (ensures) e localizações de todas as funções de lema.

2. Compreendedor (Compreensão e Síntese de Conhecimento)

• Indexação Semântica de Lemas: Aborda a falta de documentação em projetos do mundo real. Utiliza um LLM para gerar resumos em linguagem natural para lemas não documentados com base em suas especificações formais. Esses resumos, juntamente com a documentação existente, são vetorizados e indexados para Geração Aumentada por Recuperação (RAG).
• Conhecimento Verus Auto-atualizado: Analisa periodicamente a documentação oficial do Verus para extrair regras de sintaxe e recursos atualizados (por exemplo, cláusulas de término de loop). Essa base de conhecimento evolui automaticamente com a cadeia de ferramentas, prevenindo a obsolescência.

3. Provedor (Geração de Provas Orientada por Conhecimento)

• Montagem de Contexto: Combina a função-alvo com seu código dependente extraído.
• Análise de Requisitos: Utiliza um LLM para analisar a função-alvo e o código dependente a fim de gerar descrições em linguagem natural dos lemas necessários para a prova.
• Recuperação RAG: Consulta a base de conhecimento de lemas usando essas descrições para recuperar lemas relevantes.
• Síntese: Constrói um prompt estruturado contendo o alvo, dependências e lemas recuperados para gerar uma tentativa inicial de prova.

4. Refinador (Refinamento de Provas Orientado por Erros)

• Triagem de Erros: Quando a verificação falha, o módulo classifica os erros (por exemplo, sintaxe, estouro de aritmética, invariantes de loop ausentes) usando correspondência de padrões na saída do compilador.
• Recuperação de Conhecimento Direcionada: Recupera orientações corretivas específicas da base de conhecimento do Verus correspondente ao tipo de erro.
• Refinamento Iterativo: Constrói um novo prompt com a mensagem de erro, o código falho e o conhecimento corretivo, solicitando ao LLM que refine a prova. Este loop continua até que a verificação tenha sucesso ou o limite máximo de iterações seja atingido.

Contribuições Principais

1. Identificação da Lacuna Semântico-Estrutural: O artigo define formalmente o desacoplamento entre o raciocínio semântico dos LLMs e a rigidez estrutural da verificação formal como o principal gargalo para a escalabilidade.
2. Paradigma de Verificação Auto-adaptativo: Um novo framework que vai além da geração estática para uma adaptação contínua, permitindo que o sistema de verificação evolua junto com a base de código e a cadeia de ferramentas.
3. Implementação do KVerus: Um sistema funcional que integra análise consciente de dependências, indexação semântica de lemas e auto-refinamento orientado por erros.
4. Validação no Mundo Real: Aplicação bem-sucedida ao kernel do sistema operacional Rust Asterinas, especificamente ao módulo de gerenciamento de memória CortenMM.

Resultados

Os autores avaliaram o KVerus em três benchmarks de arquivo único (Verus-Bench, MBPP, Human-Eval) e três benchmarks em nível de repositório (MathSpec-Bench, Memory Allocator, CortenMM).

• Desempenho em Arquivo Único: O KVerus verificou 80,2% das tarefas (251/313), superando o estado da arte AutoVerus (56,9%) e AlphaVerus (24,9%). Também reduziu os custos de tokens em mais de 50% em comparação com o AutoVerus.
• Robustez a Atualizações da Cadeia de Ferramentas: Em experimentos através de três versões do Verus, o KVerus demonstrou estabilidade superior. Quando uma mudança disruptiva (cláusulas decreases explícitas para loops) foi introduzida, a taxa de sucesso do AutoVerus caiu 23,9%, enquanto a do KVerus caiu apenas 1,2%.
• Desempenho em Nível de Repositório: Em benchmarks de dependência entre arquivos, o KVerus alcançou uma taxa de sucesso de 51,0%, superando significativamente uma linha de base de prompting multi-rota (4,5%).
• Estudo de Caso Asterinas: O KVerus verificou com sucesso 23 funções anteriormente não verificadas no módulo CortenMM, representando 21,0% do código de prova nesse módulo. Essas provas foram aceitas na linha principal do kernel e na biblioteca padrão do Verus.
• Estudo de Ablação: A remoção do conhecimento do Verus causou a maior queda no desempenho de arquivo único (destacando a necessidade de regras de sintaxe atualizadas), enquanto a remoção de metadados de código causou a maior queda no desempenho em nível de repositório (destacando a necessidade de contexto entre arquivos).

Significado e Alegações

O artigo afirma que o KVerus representa um passo significativo em direção a tornar a verificação formal uma prática escalável e sustentável para software moderno e crítico para a segurança. Ao abordar a Lacuna Semântico-Estrutural por meio de uma arquitetura centrada no conhecimento e auto-adaptativa, o KVerus supera a fragilidade das abordagens anteriores baseadas em LLMs.

Os autores enfatizam que seu trabalho muda o paradigma de "geração estática de uma única vez" para "verificação contínua e adaptativa". Eles demonstram que, ao organizar sistematicamente sintaxe, semântica e conhecimento de domínio, é possível automatizar a verificação de sistemas complexos do mundo real (como um kernel de SO) que anteriormente eram intratáveis para ferramentas automatizadas. A aceitação a montante das provas geradas serve como evidência concreta da utilidade prática do sistema e da qualidade de sua saída.