Pruebas formales

Una prueba dice algo que una evaluación no puede decir: que una propiedad se cumple en todos los casos de un modelo, no solo en los casos que contiene una suite. Oloproof conserva el resultado de un solucionador como evidencia, y una publicación puede exigir uno. Una prueba trata del modelo formalizado que usted escribió, nunca del despliegue: una prueba de que toda transferencia está autorizada se cumple para el modelo de permisos, y si el sistema en ejecución implementa ese modelo es una pregunta aparte que responden sus suites.

Conservar un resultado

El resultado de cualquier solucionador entra bajo un único contrato, un archivo 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

El resultado es uno de PROVED, DISPROVED, UNKNOWN, TIMEOUT, ERROR o NOT_APPLICABLE, y es un campo propio: nunca un estado de decisión. certificate y counterexample guardan lo que dio el solucionador, timeout_seconds y environment cómo se ejecutó. El resultado queda sellado por su contenido, así que una copia editada es un resultado distinto. Un archivo que incumple el contrato se rechaza con el código de salida 2, igual que un produced_at sin zona horaria o en el futuro, y un PROVED que lleva un contraejemplo; el esquema es schemas/v1/proof_result.schema.json.

Ejecutar z3

Para SMT-LIB, Oloproof ejecuta él mismo un solucionador, z3, cuando está en su PATH (brew install z3, apt install z3 o pip install z3-solver). El archivo afirma la negación de la propiedad:

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

unsat significa que no existe ningún contraejemplo en el modelo: PROVED. sat significa que existe uno: DISPROVED, con el modelo de z3 como contraejemplo cuando el archivo lo pide con (get-model). unknown es UNKNOWN, una ejecución que supera --timeout es TIMEOUT, y cualquier otra cosa es ERROR: varias respuestas, un error después de la respuesta o una salida distinta de cero. El único error aceptado es que z3 diga que no hay modelo disponible después de unsat, ya que no hay ninguno que dar. oloproof proofs list muestra cada resultado que guarda el proyecto.

Un archivo vacuo da PROVED: cuando las propias aserciones del modelo se contradicen ((assert false), o dos restricciones que no pueden cumplirse a la vez), unsat no puede distinguirlo de una propiedad que se cumple. Compruebe que el modelo es satisfacible sin la propiedad negada antes de fiarse de una prueba de ella.

Exigir una prueba

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

Una entrada proofs: en release.yaml se decide en cada gate sobre el último resultado recibido para su propiedad, o para el modelo que nombra model: (un digest) cuando usted fija uno. La fecha que lleva un resultado no ordena nada, así que un resultado con fecha posterior no puede ocultar uno recibido después de él. Cuando se guarda un DISPROVED para la propiedad, la regla lo lee sea lo que sea lo que llegó después, así que un PROVED posterior nunca oculta un contraejemplo, ni siquiera uno de otro modelo: el digest de un modelo es la palabra de quien subió el resultado. Para pasar a un modelo corregido, nombra su digest en model: y la regla lee solo los resultados de ese modelo. PROVED es PASS y DISPROVED es FAIL. Cualquier otro resultado es INSUFFICIENT_EVIDENCE con el motivo proof_undecided, y la ausencia de resultado es INSUFFICIENT_EVIDENCE con proof_missing, de modo que una publicación que exige una prueba la espera. requires_manual_review: true la envía a revisión sea cual sea el resultado.

Dónde aparece

oloproof push lleva los resultados que leyó un gate. Su espacio de trabajo los guarda, pero no puede volver a ejecutar un solucionador ni ver su modelo, así que retiene el PASS de una prueba como MANUAL_REVIEW para que lo lea una persona; un FAIL o un INSUFFICIENT_EVIDENCE se mantiene. Un registro de decisión lleva los resultados que leyó el gate de su ejecución, no resultados importados después: record verify vuelve a leer a partir de ellos la decisión de cada regla, hace fallar un resultado editado después de sellarse y presenta el resultado en sí como la palabra del equipo.

Siguientes pasos

• Registro de peligros cubre lo que puede salir mal, que una prueba puede descartar en el modelo.
• Gating cubre cómo una regla bloquea una publicación.