1.1. Por que Verificar Software Formalmente?
Software controla aeronaves, dispositivos médicos, sistemas financeiros e redes de comunicação. Erros nesses sistemas custam dinheiro e vidas. O modo usual de encontrar erros é o teste, e o teste examina finitas execuções de um programa que admite infinitas. Dijkstra enunciou a limitação com precisão.E. W. Dijkstra, Notes on Structured Programming, EWD249, Technological University Eindhoven, 1970.
O teste de programas pode ser usado para mostrar a presença de erros, mas nunca para mostrar a sua ausência!
A verificação formal segue o caminho complementar. Enunciamos uma propriedade de um programa como uma proposição matemática e provamos que toda execução a satisfaz. A prova cobre todas as entradas de uma vez, o que nenhum conjunto finito de testes alcança.
Provas sobre programas reais crescem muito, então delegamos a sua verificação a uma máquina. Um assistente de prova é um programa que verifica cada passo de uma prova com respeito às regras de uma lógica formal e que ajuda o usuário a construir a prova interativamente. Lean, Rocq (antigo Coq), Isabelle/HOL e Agda são assistentes de prova em uso corrente. Resultados marcantes incluem a verificação do micronúcleo de sistema operacional seL4G. Klein et al., seL4: Formal Verification of an OS Kernel, Proceedings of SOSP 2009, pp. 207–220. e do compilador otimizante de C CompCert.X. Leroy, Formal Verification of a Realistic Compiler, Communications of the ACM 52(7), 2009, pp. 107–115.
Modelos de linguagem escrevem hoje uma parcela crescente do código. Um modelo produz texto plausível, e plausível não é o mesmo que correto. Código gerado pode invocar funções que não existem, tratar apenas os casos que o seu prompt sugere ou desviar do requisito enunciado de maneiras que sobrevivem à revisão de código. A literatura chama esse modo de falha de alucinação.
A verificação formal, em particular quando automatizada, muda a maneira como podemos confiar nesse código.L. de Moura, The Lean Programming Language and Theorem Prover, ETAPS 2026. Quando o código gerado chega com uma prova, verificada por máquina, de que satisfaz a sua especificação, o assistente de prova verifica a prova independentemente de como o código surgiu, então código alucinado ou simplesmente errado não passa. O ônus da correção move-se de ler o código para escrever a especificação certa. As técnicas desta disciplina aplicam-se sem mudança a código gerado, e a automação das aulas finais, com a tática mvcgen, aponta para verificação no ritmo da geração de código.
Nesta disciplina usamos Lean. Lean é ao mesmo tempo uma linguagem de programação e um assistente de prova, então podemos escrever um programa e provar as suas propriedades no mesmo sistema. As aulas 1 e 2 revisam a lógica clássica e introduzem a linguagem de provas de Lean, seguindo HTPIwL. As aulas 3 a 8 seguem LoVe1 por prova interativa, programação funcional e predicados indutivos. O bloco final trata a semântica de uma linguagem imperativa, a lógica de Hoare e a verificação prática com a tática mvcgen.
A Figura 1.1 mostra os componentes de Lean que a disciplina exercita. O analisador sintático lê o texto de um arquivo .lean e produz árvores de sintaxe, e o expansor de macros desdobra as notações definidas pelas bibliotecas e pelo código do usuário. O elaborador transforma essas árvores em termos da linguagem núcleo e faz o trabalho que a sintaxe de superfície deixa implícito, inferindo argumentos omitidos, resolvendo instâncias de classes de tipos e executando táticas. As táticas são elas próprias programas Lean e constroem termos, não certificados da própria correção. O kernel reverifica o termo pronto com respeito às regras da teoria de tipos dependentes, então uma tática que produz um termo errado falha aí, e somente o kernel pertence à base confiável. O compilador leva os mesmos termos a código nativo, que é o que #eval executa. As bibliotecas fornecem notações, instâncias e lemas a todas as etapas acima do kernel.
Figura 1.1. Principais componentes de Lean.
Esses componentes servem a qualquer desenvolvimento em Lean, e a disciplina os usa para um fim específico. A linguagem imperativa das últimas aulas, a sua semântica e a sua lógica de Hoare são definições Lean comuns, as condições de verificação são objetivos (goals)2 que as táticas fecham, e o kernel verifica o resultado como verifica qualquer outra prova. O objetivo desta disciplina é mostrar como usar Lean para verificar formalmente programas imperativos, e a Figura 1.2 descreve uma arquitetura para isso.
Um programa e a sua especificação formam uma tripla de Hoare. A semântica operacional big-step dá o significado da tripla. A tática mvcgen gera as condições de verificação, que são objetivos (goals) puramente lógicos. Provas por táticas as fecham, e o kernel de Lean verifica cada prova.
Figura 1.2. Arquitetura de um verificador de programas em Lean.
1. LoVe reúne os arquivos Lean que acompanham o Hitchhiker's Guide to Logical Verification, edição de 2026. A sua biblioteca de apoio LoVelib não é publicada como pacote Lake, então estas notas guardam uma cópia dela em Lectures/LoVe/, junto com a licença BSD de três cláusulas. A cópia é literal, com uma única alteração, o atributo @[reducible] em Set.PartialOrder, exigido pelo linter de definições de Lean v4.32.0 e ausente no original, escrito para Lean v4.24.0.
2. Um objetivo é o que falta provar em um ponto da prova. Lean o mostra como as hipóteses em escopo, uma por linha, seguidas do símbolo ⊢ e da proposição a provar. Cada tática ou fecha um objetivo ou o substitui por objetivos mais simples, e a prova termina quando nenhum resta. Provar Q ∧ P a partir de uma hipótese h : P ∧ Q, por exemplo, começa no objetivo
P Q : Prop h : P ∧ Q ⊢ Q ∧ P
que a tática exact ⟨h.right, h.left⟩ fecha. A Seção 1.8 retoma o assunto em detalhe.