Você pode provar que seu código Rust está correto sem escrever uma única prova. A ferramenta que faz isso se chama model checker, e para Rust o mais prático no momento é Kani, construído pela AWS. Você escreve assertions Rust normais. Kani as transforma em claims matemáticos e as verifica para cada entrada possível. Sem theorem provers. Sem proof assistants. Sem desvio de seis meses para Coq.

O problema é que “cada entrada possível” só funciona quando o espaço de entrada é pequeno o suficiente para ser exaurido. Se sua função recebe um Vec<u8> com um milhão de elementos, Kani não verificará cada permutação. Verificará até um limite que você especificar, ou rodará até seu laptop ficar sem RAM. A prova é real, mas é limitada.

O que “prova sem provas” realmente significa

Verificação formal geralmente significa escrever seu programa em um proof assistant como Coq, definir invariantes manualmente e guiar o solver através de passos tácticos. Um compiler verificado como CompCert levou anos. A maioria dos times não tem anos.

Model checking é diferente. Você escreve Rust normal. Adiciona uma função de teste anotada com #[kani::proof]. Dentro, cria valores simbólicos com kani::any(), chama seu código e faz assertions. Kani compila seu código em uma fórmula lógica e a entrega a um SMT solver. O solver confirma que a propriedade vale para todas as entradas dentro do limite, ou produz um contraexemplo concreto.

Você não escreveu uma prova. Você escreveu um teste com um quantificador universal. A ferramenta escreveu a prova.

Como Kani transforma Rust em lógica

Kani é um bounded model checker. Ele desenrola seu código em uma fórmula lógica e pergunta a um SMT solver se algum caminho de execução pode violar uma assertion. O solver trata variáveis como simbólicas. Um teste normal dá a x o valor 5. Uma prova Kani dá a x um token que representa cada u32 possível.

Aqui está um exemplo trivial. Temos uma função que nunca deveria estourar, e queremos provar isso.

// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
    x.saturating_mul(2)
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    fn check_saturating_double_never_overflows() {
        let x: u32 = kani::any();
        let result = saturating_double(x);
        if x > u32::MAX / 2 {
            assert_eq!(result, u32::MAX);
        } else {
            assert_eq!(result, x * 2);
        }
    }
}

Execute cargo kani e Kani verifica isso em segundos. Ele verifica todos os 4.294.967.296 valores possíveis de x sem executá-los um a um. O SMT solver raciocina sobre a representação simbólica e conclui que nenhum contraexemplo existe.

O guard #[cfg(kani)] significa que este código só compila sob Kani. Ele não incha seu release build.

Um exemplo real: provar que um parser nunca dá crash

Overflows são fáceis. Os casos interessantes dependem dos dados. Digamos que temos uma função que faz parse de um pequeno header de protocol. Queremos provar que ela nunca panic, não importa quais bytes alimentemos a ela.

// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
    TooShort,
    InvalidVersion,
}

pub struct Header {
    pub version: u8,
    pub length: u16,
}

/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
    if buf.len() < 4 {
        return Err(ParseError::TooShort);
    }
    let version = buf[0];
    if version != 1 {
        return Err(ParseError::InvalidVersion);
    }
    let length = u16::from_be_bytes([buf[2], buf[3]]);
    Ok(Header { version, length })
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)]
    fn check_parse_header_no_panic() {
        let len: usize = kani::any();
        kani::assume(len <= 8);
        let buf: [u8; 8] = kani::any();
        let _ = parse_header(&buf[..len]);
    }
}

Kani verifica que parse_header nunca panic para qualquer buffer de entrada de comprimento 0 a 8. Ele verifica o teste de bounds, o check de versão e o indexamento do array. Se tivéssemos escrito buf[1] em vez de verificar o comprimento primeiro, Kani encontraria um contraexemplo: um buffer de 1 byte onde buf[1] está fora de bounds.

A anotação #[kani::unwind(5)] diz a Kani quantas vezes desenrolar loops. Como nossa função não tem loops, isso é conservador.

O problema do bounding: onde o model checking bate na parede

O model checking é exaustivo dentro de seus limites. Fora desses limites, ele não diz nada. Este é o trade-off fundamental.

Loops são a primeira parede. Kani deve desenrolar cada loop um número fixo de vezes. Se sua função itera sobre um Vec e você define o limite de unwind em 10, Kani prova correção para vectors de comprimento 0 a 10. Ele não diz nada sobre comprimento 11. Cada incremento multiplica o espaço de estados. Um unwind de 50 pode terminar em minutos. Um unwind de 500 pode não terminar nunca.

Recursão é similar. Cada chamada expande a fórmula. Recursão profunda explode o uso de memória.

Tamanho dos dados é a segunda parede. Kani lida bem com arrays de tamanho fixo. Ele tem dificuldade com coleções alocadas dinamicamente a menos que você limite seu tamanho explicitamente.

A standard library é a terceira parede. Kani modela muito dela, mas não tudo. Se você chamar algo que Kani não entende, a prova falha com uma definição de função faltante.

O que Kani pode provar e onde falha

Kani é bom em encontrar panics, overflows de inteiros e violações de assertions em código limitado. Ele é excelente para primitivas criptográficas, parsers de protocol e pequenas state machines. São lugares onde uma única entrada ruim causa catástrofe, e o código é naturalmente limitado.

Kani não é bom em provar propriedades de liveness, como “cada request eventualmente recebe uma resposta.” Isso requer raciocínio sobre execuções infinitas, que o bounded model checking explicitamente não faz. Para liveness, você quer um temporal model checker como TLA+.

Kani também não é substituto para tests. Uma prova que passa diz que nenhum contraexemplo existe dentro do limite. Um test diz que o código se comporta corretamente para uma entrada específica que lhe importa. Kani pega os edge cases que você não pensou. Tests pegam os problemas de integração que Kani não pode ver.

Rodando Kani em CI sem derreter seus runners

Uma única prova Kani em uma função pequena leva segundos. Uma suite em uma crate real leva minutos. Uma prova com limites de unwind altos pode levar horas. Você não quer que sua pipeline de CI espere um solve de SMT de duas horas.

Mantenha provas Kani pequenas e rápidas. Prove as funções safety-critical, aquelas onde um bug é um incident. Não tente provar todo seu web framework. Defina um timeout, talvez cinco minutos por prova, e trate um timeout como failure to prove, não como proof of failure.

Aqui está um padrão de Makefile que funciona:

# Makefile
kani:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 300 --all-functions --enable-unstable

kani-fast:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 60 --all-functions --enable-unstable

kani-fast roda em CI a cada pull request. kani roda todas as noites. Se uma prova regredir, você descobre dentro de um dia, não depois de fazer ship.

Se você expõe uma API pública, escreva uma prova Kani por função pública que a chame com entradas completamente simbólicas. Isso é o mais próximo de um formal contract test. Não prova que a implementação está correta, mas prova que a implementação não dá crash com entradas válidas arbitrárias.

Quando recorrer a um proof assistant de verdade

Se você precisa provar propriedades sobre estruturas de dados ilimitadas, como “esta linked list é sempre acíclica,” Kani não vai ajudá-lo. O limite de unwind anula a alegação. Para isso, você precisa de uma ferramenta como Creusot, que traduz Rust para WhyML e usa um proof assistant. É mais trabalho, mas lida com estruturas ilimitadas.

Se você precisa de provas de equivalência ou detecção de undefined behavior, ferramentas como MIRI ou KLEE situam-se em pontos diferentes no espectro effort-versus-coverage. Kani é o sweet spot para “eu tenho código limitado e quero saber se ele panic.” Parsers, decoders, serializers e validadores de configuração se encaixam todos. O sistema de tipos de Rust já elimina classes inteiras de bugs. Kani elimina os que o sistema de tipos não consegue alcançar.

O que tentar primeiro

Se você tem uma crate de Rust com uma função que lhe assusta, adicione Kani. A função assustadora é geralmente a que parseia untrusted input, faz manipulação de bits ou indexa em arrays. Escreva um proof harness que a chame com kani::any(). Execute cargo kani. Se passar, você tem uma prova limitada de liberdade de crash. Se falhar, você tem um contraexemplo concreto que teria sido um bug report.

Você não precisa aprender uma nova linguagem. Você não precisa entender cálculo de sequentes. Você escreve assertions Rust, e um solver diz se elas valem. Isso não é uma prova formal no sentido acadêmico. É uma prova mecânica no sentido prático, e para a maioria do software, prático é exatamente o que você precisa.

Perguntas frequentes

O que é model checking na verificação de software?

Model checking é uma técnica automatizada que explora exaustivamente todos os estados possíveis de um sistema para verificar se as propriedades especificadas valem. Para Rust, ferramentas como Kani usam bounded model checking para provar assertions sobre todas as entradas possíveis dentro de limites definidos, sem exigir construção manual de provas.

Como Kani difere de escrever unit tests?

Um unit test verifica uma entrada específica. Uma prova Kani verifica cada entrada dentro de um limite. Se uma prova Kani passa, você sabe que nenhum contraexemplo existe no espaço de estados limitado. A prova é mais forte, mas é limitada pelos limites que você define.

Kani pode provar que toda minha aplicação Rust está correta?

Não. Kani funciona melhor em funções pequenas e limitadas. O espaço de estados cresce exponencialmente com iterações de loops, profundidade de recursão e tamanho dos dados. Use Kani para componentes safety-critical como parsers e handlers de protocol, não para lógica de nível de aplicação.

O que acontece quando Kani encontra um loop sem limite fixo?

Kani requer um limite de unwind para loops. Se o loop puder executar mais vezes do que o limite permite, Kani insere uma unwinding assertion que falha. Você deve aumentar o limite ou refatorar o código para ter uma contagem de iterações conhecida estaticamente. Esta é a principal limitação do bounded model checking.