🛡️ Verificação Formal
No PAEBIRU, a verificação formal não é um luxo acadêmico, mas uma ferramenta pragmática de engenharia. Utilizamos modelos formais para provar invariantes críticas de concorrência, economia e matemática.
1. Abordagem Pragmática
Não tentamos provar cada linha de código. Aplicamos a verificação cirurgicamente onde o custo da falha é alto ou o comportamento é complexo.
| Ferramenta | Uso Principal | Localização |
|---|---|---|
| TLA+ | Concorrência, loop GALS, liveness de atores, consenso bizantino. | crates/*/formal/tla/ |
| Lean 4 | Pureza algorítmica, precisão geodésica, conservação de energia. | crates/*/formal/lean/ |
2. TLA+ (Temporal Logic of Actions)
Usado para modelar o estado global e a interação entre atores.
- Exemplo: Provar que o loop do Kernel nunca entra em deadlock mesmo sob saturação de backpressure.
- Execução: Através do
TLC Model Checker.
3. Lean 4 (Prova de Teoremas)
Usado para garantir a correção de funções puras e fundamentação matemática.
- Exemplo: Prova de que o Hamiltoniano de Ising converge para um estado de energia mínima sob as regras do scheduler.
- Execução: Através do comando
lake buildno diretório formal.
4. Integração com o Fluxo RSE
Toda RFC que introduz um novo protocolo crítico (ex: um novo portão de segurança ou mecanismo de crédito) deve ser acompanhada de uma especificação formal mínima.
- Research: Identificar as propriedades de segurança e liveness.
- Strategy: Escrever o modelo TLA+ ou Lean.
- Execution: Implementar em Rust e validar contra o modelo.
5. Como rodar as verificações
Utilize o orquestrador canônico:
make verify-formal
Este comando invocará os checkers de TLA+ e os compiladores de Lean 4 configurados no workspace.