Isabelle

Isabelle
Isabelle
Autores	Lawrence Paulson, Tobias Nipkow e Makarius Wenzel
Desenvolvedores	Universidade de Cambridge, Universidade Técnica de Munique (TUM) e colaboradores
Lançamento inicial	1986
Lançamento estável	Isabelle2024 / maio de 2024
Escrito em	Standard ML (Poly/ML) e Scala
Sistema; operacional	Linux, Windows e macOS
Tipo	Assistente de prova, lógica matemática, verificação formal
Licença	Licença BSD (duas cláusulas)
Website	isabelle.in.tum.de

Isabelle é um assistente de prova interativo e genérico (provador de teoremas) de código aberto, projetado para a formalização rigorosa de teorias matemáticas e a verificação formal de software e hardware. Concebido inicialmente por Lawrence Paulson na Universidade de Cambridge em 1986 e desenvolvido em contínua cooperação com Tobias Nipkow na Universidade Técnica de Munique (TUM) e Makarius Wenzel, o sistema destaca-se por sua arquitetura lógica parametrizável e por seu elevado grau de automação computacional.

Diferentemente de assistentes focados em um único formalismo dedutivo estrito, o Isabelle foi arquitetado como uma ferramenta genérica estruturada sobre uma metalógica intuicionista de ordem superior chamada Pure. Sobre essa base são instanciadas diversas lógicas-objeto, com destaque absoluto para o Isabelle/HOL, implementação da lógica de ordem superior (baseada na teoria dos tipos de Church) que se tornou o ambiente padrão da comunidade acadêmica.

O Isabelle alcançou notoriedade mundial em 2009 ao ser empregado na verificação formal integral do microkernel de sistema operacional seL4, constituindo o primeiro kernel de uso geral do mundo matematicamente provado livre de falhas de segurança de memória e em conformidade estrita com a sua especificação formal.

Arquitetura e fundamentos lógicos

O paradigma LCF e o núcleo confiável

O Isabelle adota a arquitetura de projeto clássica de provadores descendentes do paradigma LCF (Logic for Computable Functions), concebido por Robin Milner na década de 1970. Sob esse modelo, a confiabilidade de todo o ecossistema assenta-se em um núcleo lógico diminuto e auditável (o trusted kernel).

No núcleo, os teoremas são modelados como um tipo de dado abstrato na linguagem funcional Standard ML (executada primordialmente no compilador otimizado Poly/ML). Novos valores desse tipo só podem ser gerados exclusivamente pela aplicação das regras primitivas de inferência da lógica. Funções auxiliares, táticas automatizadas e provadores externos podem sugerir etapas de dedução complexas, mas caso cometam qualquer erro algorítmico, o núcleo rejeita a operação. Dessa forma, falhas de programação em ferramentas acessórias de automação são incapazes de corromper a consistência lógica do sistema.

A metalógica Pure

O núcleo formal do Isabelle é a metalógica Pure, uma formulação minimalista da lógica intuicionista de ordem superior baseada no cálculo lambda simplesmente tipado ( $\lambda ^{\to }$ ). A sintaxe de qualquer linguagem-objeto é modelada por meio de termos tipados de Pure, e suas regras de inferência são formalizadas utilizando três conectivos primitivos da metalógica:

Meta-implicação ( $\Longrightarrow$ ): Representa a relação de consequência lógica ou causalidade entre premissas e conclusões. A regra de dedução clássica do modus ponens é codificada na forma:

P\Longrightarrow (P\longrightarrow Q)\Longrightarrow Q

Meta-quantificação universal ( $\bigwedge$ ): Quantifica sobre variáveis arbitrárias da linguagem-objeto (análogo formal ao operador "para todo" paramétrico), permitindo expressar hipóteses com escopo local:

(\bigwedge x.\,P(x))\Longrightarrow \forall x.\,P(x)

Meta-igualdade ( $\equiv$ ): Define abreviações notacionais, equivalências lógicas canônicas e regras fundamentais de reescrita terminológica no nível do compilador.

A composição encadeada de passos de demonstração é executada através de um algoritmo uniforme denominado resolução de ordem superior (higher-order resolution), combinando a unificação de termos lambda de ordem superior com o princípio de resolução lógica de Robinson.

Lógicas-objeto

Por ser um demonstrador genérico, o Isabelle pode hospedar múltiplos sistemas formais autônomos construídos sobre a base Pure:

Isabelle/HOL: É a lógica mais ampla, documentada e ativamente desenvolvida do sistema. Implementa a lógica de ordem superior com tipos polimórficos de estilo Hindley-Milner, axioma do infinito e escolha booleana clássica. Contém uma gigantesca biblioteca nativa de estruturas matemáticas (álgebra abstrata, topologia, cálculo diferencial, teoria da medida e probabilidade) e estruturas de dados computacionais (árvores, grafos, listas e semântica de linguagens de programação).
Isabelle/ZF: Implementa a teoria axiomática de conjuntos de Zermelo-Fraenkel com o axioma da escolha, adequada para formalizações fundamentadas diretamente em construções clássicas de conjuntos não tipados.
Isabelle/FOL: Formaliza a lógica de primeira ordem pura (em variantes clássica e intuicionista).
Outras lógicas históricas: O sistema já hospedou formalizações da teoria dos tipos construtivos de Martin-Löf (CTT), lógicas modais e a lógica de predicados computáveis (LCF).

A linguagem de prova declarativa Isar

Nas primeiras versões do Isabelle, as demonstrações eram conduzidas exclusivamente por meio de scripts procedurais imperativos na linguagem Standard ML, consistindo em sequências opacas de comandos de táticas (como `apply (rule ...)`, `apply (erule ...)`) que manipulavam a pilha de submetas em memória. Tais scripts mostravam-se frágeis a alterações e virtualmente ilegíveis por seres humanos sem a execução interativa concomitante da ferramenta.

Para superar essa limitação, Makarius Wenzel concebeu o Isar (Intelligible Semi-Automated Reasoning). Inspirado na clareza do formato de provas do sistema Mizar, o Isar introduziu uma sintaxe declarativa onde o raciocínio matemático se estrutura em passos textuais explícitos, documentando hipóteses locais, lemas intermediários e resultados visados.

Uma prova típica em Isar apresenta a seguinte estrutura inteligível:

lemma "A & B --> B & A"
proof
  assume "A & B"
  then have "A" and "B" by (rule conjunct1, rule conjunct2)
  then show "B & A" by (rule conjI)
qed

As palavras-chave `assume` (introdução de hipóteses), `have` (afirmação intermediária), `show` (demonstração da meta final da seção) e `qed` (fechamento formal do bloco) tornam a leitura das formalizações acessível e similar a artigos matemáticos tradicionais rigorosos.

Recursos de automação e raciocínio assistido

O mecanismo Sledgehammer

Uma das maiores inovações desenvolvidas no âmbito do Isabelle/HOL é o subsistema Sledgehammer. Trata-se de uma ponte de automação inteligente que conecta a submeta corrente a múltiplos demonstradores automáticos de teoremas (ATPs) externos de alta performance (tais como E, Vampire, SPASS) e resolvedores de teorias satisfatíveis módulo teorias (SMT solvers, como Z3 e CVC5).

O fluxo de operação do Sledgehammer preserva rigorosamente a segurança lógica:1. O sistema seleciona centenas de lemas e fatos relevantes da biblioteca do Isabelle por meio de algoritmos de relevância semântica (filtros me-sh);2. Traduz a meta e os fatos para formatos compatíveis com os provadores externos (como TPTP ou SMT-LIB);3. Executa os provadores externos de forma massivamente concorrente em segundo plano;4. Quando um ATP encontra uma prova, o Isabelle não aceita o resultado cegamente. Em vez disso, o Sledgehammer analisa quais fatos foram indispensáveis e reconstrói uma prova formal estrita dentro do próprio Isabelle por meio de métodos internos do núcleo (como o algoritmo `metis`), assegurando que apenas deduções verificadas pelo núcleo confiável sejam homologadas.

Ferramentas de contraexemplo: Quickcheck e Nitpick

Para evitar que o usuário despenda tempo tentando provar conjecturas que são matematicamente falsas ou incompletas, o Isabelle oferece ferramentas de refutação prévia:

Quickcheck: Testa conjecturas automaticamente compilando as metas para código executável funcional e gerando conjuntos aleatórios e exaustivos de entradas para detectar contraexemplos imediatos.
Nitpick: Utiliza solucionadores de satisfatibilidade booleana (SAT solvers) de primeira linha para pesquisar contraexemplos finitos complexos baseados na semântica de modelos hereditariamente finitos de alta ordem.

Geração de código executável

O Isabelle/HOL possui um gerador de código funcional nativo comprovado correto. Especificações de algoritmos matemáticos e estruturas de dados expressas construtivamente na lógica podem ser convertidas de forma direta e automática em programas executáveis eficientes nas linguagens Haskell, OCaml, Standard ML e Scala.

Ambiente de desenvolvimento: PIDE e Isabelle/jEdit

Historicamente, o Isabelle utilizava o ambiente genérico Proof General, executado sobre o GNU Emacs, no qual as provas eram processadas sequencialmente passo a passo, bloqueando o editor.

A partir de 2010, Makarius Wenzel liderou o desenvolvimento de uma arquitetura inovadora de interação denominada PIDE (Prover IDE Framework). Implementado sobre a plataforma JVM em linguagem Scala, o PIDE transforma o provador em um motor reativo e assíncrono em tempo real. O ambiente padrão, Isabelle/jEdit (baseado no editor de código aberto jEdit), verifica dinamicamente o texto formal de modo multithreaded e paralelo: enquanto o usuário redige, edita ou reorganiza o documento, os teoremas são reavaliados em plano de fundo com destaque sintático e semântico instantâneo de erros e avisos. Suporte análogo baseado no protocolo PIDE foi posteriormente desenvolvido sob a forma de extensões para o Visual Studio Code (Isabelle/VSCode).

O Archive of Formal Proofs (AFP)

O Archive of Formal Proofs (AFP) é a biblioteca digital e repositório central comunitário de formalizações do Isabelle. Operando de maneira similar a um periódico acadêmico com revisão por pares aberta, o arquivo reúne formalizações extensas em matemática avançada pura, algoritmos, criptografia, modelos de concorrência e teorias físicas.

Todas as submissões no AFP são testadas e recompiladas continuamente em servidores de integração contínua a cada nova versão de lançamento do Isabelle, garantindo a reprodutibilidade científica e a imunidade a quebras de compatibilidade reversa.

Aplicações e casos notáveis

O Isabelle consolidou-se como instrumento central em projetos científicos de alta complexidade:

O microkernel seL4: Entre 2004 e 2009, pesquisadores do NICTA (Austrália), liderados por Gerwin Klein, utilizaram o Isabelle/HOL para provar formalmente que a implementação de baixo nível em linguagem C do kernel seL4 satisfazia plenamente a sua especificação matemática de alto nível, demonstrando a ausência absoluta de estouros de pilha (buffer overflow), ponteiros nulos ou condições de corrida em memória.
Munique e o algoritmo Java: Formalização semântica integral do núcleo da linguagem Java e da máquina virtual Java (JVM) no projeto Jinja, provando formalmente a segurança de tipos do bytecode e de seu compilador.
Matemática pura formalizada: Formalizações do teorema dos números primos, do teorema de Gödel e da classificação de álgebras de Lie e grupos finitos foram integralmente homologadas no sistema.
Certificação de segurança de voo: Utilização por consórcios aeroespaciais e agências de defesa na análise rigorosa e certificação de protocolos de comunicação distribuída e pilotos automáticos.

Ver também

Referências

1 2 3 4 Lawrence C. Paulson (1986). «Natural deduction as higher-order resolution». The Journal of Logic Programming (em inglês). 3 (3): 237-258. doi:10.1016/0743-1066(86)90015-4
1 2 3 Tobias Nipkow, Lawrence C. Paulson e Markus Wenzel (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic (em inglês). Berlim: Springer-Verlag. pp. 1–25. ISBN 978-3540433767
1 2 Mike Gordon (16 de novembro de 1994). «History of Isabelle and HOL». Isabelle and HOL (em inglês). University of Cambridge. Consultado em 18 de outubro de 2023
1 2 Gerwin Klein; et al. (2010). «seL4: Formal verification of an OS kernel». Communications of the ACM (em inglês). 53 (6): 107-115. doi:10.1145/1743546.1743574
↑ Robin Milner (1979). Logic for Computable Functions: description of a machine implementation (em inglês). [S.l.]: Stanford University
1 2 Markus Wenzel (2002). Isabelle/Isar — A Versatile Environment for Human-Readable Formal Proof Documents (Doutorado em Ciência da Computação) (em inglês). Technische Universität München
1 2 3 4 Jasmin Christian Blanchette, Lukas Bulwahn e Tobias Nipkow (2011). Automatic Proof and Disproof in Isabelle/HOL (em inglês). Frontiers of Combining Systems (FroCoS 2011). Springer. pp. 12–27. doi:10.1007/978-3-642-24364-6_2
↑ Jasmin Christian Blanchette e Tobias Nipkow (2010). Nitpick: A Counterexample Generator for Higher-Order Logic Based on a SAT Solver (em inglês). Interactive Theorem Proving (ITP 2010). Springer. pp. 131–146. doi:10.1007/978-3-642-14052-5_11
↑ Florian Haftmann e Tobias Nipkow (2010). Code Generation from Specifications in Higher Order Logic (em inglês). Static Analysis (SAS 2010). Springer. pp. 38–54. doi:10.1007/978-3-642-15769-1_4
↑ Makarius Wenzel (2012). Isabelle/jEdit — a Prover IDE within the PIDE framework (em inglês). Conferência Internacional de Raciocínio Automatizado. pp. 468–471. doi:10.1007/978-3-642-31365-3_38
1 2 3 Manuel Eberl, Gerwin Klein, Tobias Nipkow, Larry Paulson e René Thiemann. «Archive of Formal Proofs» (em inglês). Consultado em 18 de outubro de 2023
↑ Tobias Nipkow (2006). Jinja: Towards a Full Formal Type-Safety Proof for a Real-World Language (em inglês). [S.l.]: Springer

Ligações externas

Sítio oficial do Isabelle (em inglês)
Sítio oficial do Archive of Formal Proofs (AFP) (em inglês)
Documentação oficial e tutoriais do Isabelle/HOL (em inglês)

[Paulson1986-1] 1 2 3 4 Lawrence C. Paulson (1986). «Natural deduction as higher-order resolution». The Journal of Logic Programming (em inglês). 3 (3): 237-258. doi:10.1016/0743-1066(86)90015-4

[NipkowPaulsonWenzel-2] 1 2 3 Tobias Nipkow, Lawrence C. Paulson e Markus Wenzel (2002). Isabelle/HOL: A Proof Assistant for Higher-Order Logic (em inglês). Berlim: Springer-Verlag. pp. 1–25. ISBN 978-3540433767

[Gordon1994-3] 1 2 Mike Gordon (16 de novembro de 1994). «History of Isabelle and HOL». Isabelle and HOL (em inglês). University of Cambridge. Consultado em 18 de outubro de 2023

[Klein2009-4] 1 2 Gerwin Klein; et al. (2010). «seL4: Formal verification of an OS kernel». Communications of the ACM (em inglês). 53 (6): 107-115. doi:10.1145/1743546.1743574

[Milner1979-5] Robin Milner (1979). Logic for Computable Functions: description of a machine implementation (em inglês). [S.l.]: Stanford University

[Wenzel2002-6] 1 2 Markus Wenzel (2002). Isabelle/Isar — A Versatile Environment for Human-Readable Formal Proof Documents (Doutorado em Ciência da Computação) (em inglês). Technische Universität München

[Blanchette2011-7] 1 2 3 4 Jasmin Christian Blanchette, Lukas Bulwahn e Tobias Nipkow (2011). Automatic Proof and Disproof in Isabelle/HOL (em inglês). Frontiers of Combining Systems (FroCoS 2011). Springer. pp. 12–27. doi:10.1007/978-3-642-24364-6_2

[8] Jasmin Christian Blanchette e Tobias Nipkow (2010). Nitpick: A Counterexample Generator for Higher-Order Logic Based on a SAT Solver (em inglês). Interactive Theorem Proving (ITP 2010). Springer. pp. 131–146. doi:10.1007/978-3-642-14052-5_11

[9] Florian Haftmann e Tobias Nipkow (2010). Code Generation from Specifications in Higher Order Logic (em inglês). Static Analysis (SAS 2010). Springer. pp. 38–54. doi:10.1007/978-3-642-15769-1_4

[10] Makarius Wenzel (2012). Isabelle/jEdit — a Prover IDE within the PIDE framework (em inglês). Conferência Internacional de Raciocínio Automatizado. pp. 468–471. doi:10.1007/978-3-642-31365-3_38

[AFP-11] 1 2 3 Manuel Eberl, Gerwin Klein, Tobias Nipkow, Larry Paulson e René Thiemann. «Archive of Formal Proofs» (em inglês). Consultado em 18 de outubro de 2023

[12] Tobias Nipkow (2006). Jinja: Towards a Full Formal Type-Safety Proof for a Real-World Language (em inglês). [S.l.]: Springer