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 checagem a uma máquina. Um assistente de prova é um programa que checa 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 o modo 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, checada por máquina, de que satisfaz a sua especificação, o assistente de prova checa 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 LoVe 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.