Provas formais

Uma prova diz algo que uma avaliação não consegue dizer: que uma propriedade vale em todos os casos de um modelo, não só nos casos que uma suíte contém. O Oloproof guarda o resultado de um solver como evidência, e um lançamento pode exigir um. Uma prova trata do modelo formalizado que você escreveu, nunca da implantação: uma prova de que toda transferência é autorizada vale para o modelo de permissões, e se o sistema em execução implementa esse modelo é uma questão separada, que as suas suítes respondem.

Guardando um resultado

O resultado de qualquer solver entra sob um único contrato, um arquivo JSON:

{
  "property": {"id": "transfer-authorized", "notation": "LTL", "statement": "G(transfer -> authorized)"},
  "model": {"digest": "sha256:...", "description": "the agent's tool-permission model"},
  "solver": {"name": "nuXmv", "version": "2.0.0"},
  "assumptions": ["the tool router is the only path to transfer"],
  "outcome": "PROVED",
  "scope": "the permission model, not the deployment",
  "produced_at": "2026-10-19T09:00:00Z"
}

oloproof proofs import result.json

O desfecho é um entre PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR ou NOT_APPLICABLE, e é um campo próprio: nunca um estado de decisão. certificate e counterexample guardam o que o solver forneceu; timeout_seconds e environment, como ele foi executado. O resultado é selado pelo seu conteúdo, então uma cópia editada é um resultado diferente. Um arquivo que viola o contrato é recusado com o código de saída 2, assim como um produced_at sem fuso horário ou no futuro, e um PROVED que traz um contraexemplo; o schema é schemas/v1/proof_result.schema.json.

Executando o z3

Para SMT-LIB, o Oloproof executa ele mesmo um solver, o z3, quando ele está no seu PATH (brew install z3, apt install z3 ou pip install z3-solver). O arquivo afirma a negação da propriedade:

oloproof proofs run transfer.smt2 --property transfer-authorized --statement "every transfer is authorized"

unsat significa que não existe contraexemplo no modelo: PROVED. sat significa que existe um: DISPROVED, com o modelo do z3 como contraexemplo quando o arquivo o pede com (get-model). unknown é UNKNOWN, uma execução que passa de --timeout é TIMEOUT, e qualquer outra coisa é ERROR: várias respostas, um erro depois da resposta ou uma saída diferente de zero. O único erro aceito é o z3 dizer que nenhum modelo está disponível depois de unsat, já que não há nenhum a fornecer. oloproof proofs list mostra todos os resultados que o projeto guarda.

Um arquivo vácuo dá PROVED: quando as próprias asserções do modelo se contradizem ((assert false), ou duas restrições que não podem valer juntas), unsat não consegue distinguir isso de uma propriedade que vale. Verifique que o modelo é satisfazível sem a propriedade negada antes de confiar em uma prova dela.

Exigindo uma prova

proofs:
  - id: no-unauthorized-transfer
    property: transfer-authorized

Uma entrada proofs: no release.yaml é decidida em cada gate sobre o último resultado recebido para a sua propriedade, ou para o modelo nomeado por model: (um digest) quando você define um. A data que um resultado traz não ordena nada, então um resultado com data posterior não pode esconder um recebido depois dele. Quando um DISPROVED é guardado para a propriedade, a regra o lê, seja o que for que tenha chegado depois, então um PROVED posterior nunca esconde um contraexemplo, nem mesmo um de outro modelo: o digest de um modelo é a palavra de quem enviou o resultado. Para passar a um modelo corrigido, nomeie o digest dele em model:, e a regra lê apenas os resultados desse modelo. PROVED é PASS e DISPROVED é FAIL. Qualquer outro desfecho é INSUFFICIENT_EVIDENCE com o motivo proof_undecided, e nenhum resultado é INSUFFICIENT_EVIDENCE com proof_missing, então um lançamento que exige uma prova espera por ela. requires_manual_review: true a envia para revisão qualquer que seja o desfecho.

Onde aparece

oloproof push leva os resultados que um gate leu. O seu espaço de trabalho os guarda, mas não pode reexecutar um solver nem ver o seu modelo, então retém o PASS de uma prova como MANUAL_REVIEW para uma pessoa ler; um FAIL ou um INSUFFICIENT_EVIDENCE se mantém. Um registro de decisão leva os resultados que o gate da sua execução leu, não resultados importados depois dele: record verify relê a decisão de cada regra a partir deles, reprova um resultado editado depois de selado e apresenta o próprio resultado como a palavra da equipe.

Próximos passos

• Registro de perigos cobre o que pode dar errado, que uma prova pode descartar no modelo.
• Gating cobre como uma regra bloqueia um lançamento.