Você não precisa de LTL para usar um model checker

Você não precisa aprender lógica temporal linear para usar um model checker. Ferramentas como Kani, CBMC e Alloy permitem verificar propriedades com assertions e constraints relacionais ordinários. Você troca a capacidade de provar propriedades de liveness por uma curva de aprendizado medida em horas em vez de semanas, e para a maioria dos bugs de software, essa é uma troca que vale a pena.

Temporal logic é o guardião que a maioria dos model checkers exige

Os model checkers clássicos, SPIN e NuSMV, pedem que você expresse propriedades em LTL ou CTL. Você escreve coisas como G(request -> F(response)) para dizer “globalmente, toda requisição é eventualmente seguida por uma resposta”. Isso é poderoso. Pode provar que seu protocol nunca entra em deadlock, que toda mensagem é eventualmente reconhecida, que seu sistema é fair.

Também é uma habilidade especializada que a maioria dos desenvolvedores em atividade não possui. Ler uma fórmula LTL não é como ler código. Os operadores são modais, a semântica é sobre traces infinitos, e a intuição que você construiu escrevendo unit tests não se transfere. Então a pergunta é justa: se você quer o poder de bug-finding do model checking, realmente precisa escalar aquela montanha primeiro?

Não. Uma classe diferente de ferramentas existe há décadas, e elas verificam código com os mesmos assertions que você já escreve.

Bounded model checkers transformam assertions em problemas SAT

Bounded model checkers não pedem que você aprenda uma nova lógica. Eles pedem que você escreva um test harness. Você declara inputs não determinísticos, os restringe com assumptions e afirma propriedades na linguagem hospedeira. A ferramenta então desenrola loops até um bound, codifica o programa como uma fórmula SAT ou SMT, e pede ao solver que encontre um counterexample.

Se o solver retornar UNSAT, sua propriedade vale para todos os paths dentro daquele bound. Se encontrar um counterexample, você recebe um trace concreto mostrando exatamente quais inputs disparam o bug. Sem operadores temporais. Sem traces infinitos. Apenas um assertion falhado com um vector de input reproduzível.

Kani é o bounded model checker mais acessível para Rust. Instala-se com cargo install kani-verifier e funciona em código Rust ordinário.

Um exemplo real: verificando uma state machine em Rust

Aqui está uma state machine com um bug. Ela rastreia um counter simples que decrementa a cada tick até chegar a zero, então transiciona de volta para idle.

#[derive(Clone, Copy, PartialEq, Debug)]
enum State {
    Idle,
    Running,
    Stopped,
}

struct Machine {
    state: State,
    count: u32,
}

impl Machine {
    fn start(&mut self, initial: u32) {
        if self.state == State::Idle && initial > 0 {
            self.state = State::Running;
            self.count = initial;
        }
    }

    fn tick(&mut self) {
        if self.state == State::Running {
            self.count -= 1;
            if self.count == 0 {
                self.state = State::Idle;
            }
        }
    }

    fn stop(&mut self) {
        if self.state == State::Running {
            self.state = State::Stopped;
        }
    }
}

O bug é sutil. Olhe para stop. Ele define o estado como Stopped mas deixa count inalterado. Se algo mais tarde assumir que count == 0 quando state == State::Stopped, essa assumption está errada.

Aqui está um Kani proof harness que o captura:

#[kani::proof]
fn check_stopped_implies_count_zero() {
    let mut machine = Machine {
        state: State::Idle,
        count: 0,
    };

    let initial: u32 = kani::any();
    kani::assume(initial > 0 && initial <= 10);

    machine.start(initial);
    machine.tick();
    machine.stop();

    assert!(
        machine.state != State::Stopped || machine.count == 0,
        "Stopped state should have count == 0"
    );
}

Kani explora cada path. Ele descobre que se initial == 2, após start a máquina está Running com count == 2. Um tick decrementa count para 1 mas o estado permanece Running. Então stop define o estado como Stopped com count == 1. O assertion falha. Kani reporta exatamente esse trace.

Esta é a experiência de model checking sem temporal logic. Você escreve Rust. Você escreve assertions em Rust. A ferramenta diz quais inputs os quebram.

Alloy encontra bugs em nível de design com lógica relacional

Bounded model checkers verificam código. Alloy verifica designs.

Alloy é um model finder, não um model checker tradicional, mas a distinção importa menos do que o workflow. Você descreve seu sistema como um conjunto de relações, invariantes de estado como constraints de first-order logic, e pede ao Alloy para encontrar um counterexample. Ele busca todas as instâncias possíveis até um scope definido pelo usuário e mostra diagramas da falha.

Aqui está um modelo Alloy de uma propriedade de grafo direcionado simples:

sig Node {
    next: set Node
}

pred reachable[n1, n2: Node] {
    n2 in n1.^next
}

assert symmetric_reachability {
    all n1, n2: Node |
        reachable[n1, n2] implies reachable[n2, n1]
}

check symmetric_reachability for 3

O assertion afirma que reachability é simétrica. Alloy verifica isso para todos os grafos de até três nodes e imediatamente desenha um counterexample: um grafo onde n1 aponta para n2 mas n2 não tem arestas de saída. Nenhum operador G, F ou U aparece em lugar algum.

O que você abre mão: liveness e comportamento infinito

Essa conveniência tem um custo. Bounded model checkers apenas verificam comportamento até um loop bound ou comprimento de trace. Eles não podem provar que uma requisição é eventualmente respondida, apenas que coisas ruins não acontecem nos primeiros N passos. Alloy apenas verifica instâncias dentro de seu scope. Ele não pode provar propriedades para sistemas arbitrariamente grandes, apenas que nenhum counterexample existe abaixo do bound.

Se você precisa provar que seu protocol de consensus nunca perde writes committed, ou que toda mensagem é eventualmente entregue, você ainda precisa de temporal logic e unbounded model checking. Ferramentas como TLA+ envolvem temporal logic em uma sintaxe que parece mais com matemática do que com lógica modal, mas a semântica subjacente ainda é temporal.

Para invariantes de estruturas de dados, enforcement de contratos de API, e encontrar a race condition que só dispara no 47º path de execução, ferramentas bounded geralmente são suficientes. Elas pegam os bugs que os unit tests deixam passar, e fazem isso com assertions que você pode ler sem um livro didático.

Começando com Kani em cinco minutos

Se você tem Rust instalado, bounded model checking está a um comando de distância.

cargo install kani-verifier
cargo kani setup

Crie uma nova crate, escreva uma função com um bug sutil, e adicione um harness #[kani::proof]. Execute cargo kani. Se Kani encontrar um counterexample, ele imprime os inputs concretos que disparam a falha. Se reportar VERIFICATION SUCCESSFUL, sua propriedade vale para todos os paths dentro dos bounds padrão.

Comece com funções que têm state spaces pequenos e invariantes claras. State machines, validação de parsers, e transições de estado de protocols são alvos ideais para começar. Evite tentar verificar um servidor HTTP inteiro na primeira tentativa. O SAT solver tem limites, e sua paciência também.

FAQ: bounded vs. unbounded, liveness e por onde começar

Bounded model checking é realmente model checking?

Tecnicamente, é uma variante que codifica o problema como uma satisfiability query ao invés de explorar o state graph explicitamente. Para um desenvolvedor tentando encontrar bugs, a distinção é acadêmica. Ele explora todos os paths sistematicamente, o que é o que model checking significa na prática.

Posso provar liveness com Kani ou CBMC?

Não diretamente. Propriedades de liveness requerem raciocinar sobre comportamento infinito, e ferramentas bounded limitam explicitamente sua busca. Você pode às vezes codificar uma verificação de liveness bounded desenrolando passos suficientes para alcançar um fixpoint, mas isso é uma técnica avançada.

E o TLA+? Ele requer temporal logic?

TLA+ usa a Temporal Logic of Actions, então sim, tecnicamente. Mas Leslie Lamport projetou a sintaxe para ler como matemática ordinária. A maioria das especificações TLA+ gasta 90% de seu texto em invariantes de estado e constraints de estruturas de dados, não em operadores temporais. É o caminho mais acessível se você precisa de raciocínio temporal unbounded.

Devo usar Alloy ou Kani?

Use Kani se você tem código Rust e quer verificar detalhes de implementação. Use Alloy se você ainda está projetando o sistema e quer explorar se suas invariantes são mesmo possíveis antes de escrever o código.

Escolha a ferramenta que combina com seu problema, não com sua ambição

Temporal logic é bela e poderosa, mas não é um pré-requisito para verificação formal. Bounded model checkers e relational model finders permitem expressar propriedades nas linguagens que você já conhece. Elas não vão provar que seu sistema eventualmente termina, mas vão encontrar o erro off-by-one que corrompe sua state machine de banco de dados. Para a maioria das equipes, esse é o bug que importa.

Comece com Kani em uma única função com estado. Escreva um assertion. Deixe o solver dizer o que você perdeu.