# Proof-carrying output: cuando la respuesta crítica debe traer prueba ejecutable

> Para decisiones formalizables, un agente debe entregar una afirmación junto con un artefacto que un verificador independiente pueda aceptar o rechazar.

- Author: Viktor Berthelius (BRTHLS)
- Published: 2026-08-29
- Category: ai operating models
- Tags: formal-verification, lean4, agent-evaluation, proof-carrying-output
- Language: es
- Canonical: https://www.brthls.com/magazine/proof-carrying-output-prueba-ejecutable-agentes-es
- Source: BRTHLS Magazine — https://www.brthls.com

---

## Problema

Una explicación larga puede sonar rigurosa y seguir conteniendo un paso falso. Añadir otro agente crítico mejora cobertura, pero ambos continúan operando con lenguaje probabilístico.

En dominios formalizables —cálculos, invariantes, reglas de asignación o propiedades de código— la revisión verbal deja una pregunta abierta: ¿el verificador comprobó la afirmación o solo produjo una explicación más convincente?

## Tesis

Un output crítico debería viajar con una prueba ejecutable o un certificado que otro sistema pueda comprobar sin confiar en el modelo que lo generó.

**La garantía no está en que el agente explique mejor, sino en reducir la parte que exige creerle.**

## Framework

HERMES combina razonamiento informal de un LLM con verificación paso a paso en Lean 4. Su herramienta devuelve estados distintos: probado, refutado o no resuelto. Esa tercera salida es esencial: evita convertir la ausencia de prueba en una falsa aprobación.

El patrón se puede trasladar fuera de las matemáticas. Un agente propone un plan o una transformación. Un compilador, solver, test determinista o motor de políticas comprueba las propiedades formalizables. La operación solo avanza si el certificado coincide con la especificación vigente.

No todo debe formalizarse. Empieza por invariantes pequeños y costosos de violar: el total cuadra, ningún usuario gana privilegios, la asignación respeta capacidad o el cambio conserva una propiedad crítica.

**Señal medible:** porcentaje de decisiones críticas acompañadas por certificado verificable y distribución entre probado, refutado y no resuelto.

## Por que importa ahora

El aumento de agentes y contexto hace más difícil auditar la cadena completa de razonamiento. Un verificador pequeño crea un punto de confianza más estrecho: no necesita evaluar el estilo del argumento, solo comprobar el artefacto.

También mejora el desacuerdo. Si dos agentes proponen soluciones distintas, una propiedad ejecutable permite comparar contra la misma especificación. La discusión pasa de autoridad a evidencia.

## Anti-ejemplo

"Otro LLM revisó la respuesta y dijo que es correcta." Eso es una segunda opinión, no una prueba independiente. Puede ser útil para descubrir problemas, pero comparte modos de fallo con el productor.

El formalismo tampoco salva una especificación equivocada. Probar perfectamente la regla incorrecta solo automatiza el error. La especificación necesita owner, versión y casos que conecten símbolo con realidad.

## Protocolo (3 pasos)

1. **Elige un invariante.** Formula una propiedad estrecha, binaria y valiosa.
2. **Separa productor y checker.** El agente genera; una herramienta independiente valida.
3. **Conserva tres estados.** Distingue probado, refutado y no resuelto, con escalado para el tercero.

Versiona especificación, prueba y output juntos. Si cambia la regla de negocio, los certificados anteriores deben poder identificarse como pertenecientes a otra versión.

| Estado | Significado | Acción |
| --- | --- | --- |
| probado | el checker acepta | continuar |
| refutado | existe contradicción | bloquear |
| no resuelto | falta evidencia | escalar |

## Relacionado

- [Eval-driven development: el prototipo debe descubrir el benchmark](/magazine/eval-driven-development-prototipo-antes-benchmark-es)
- [Output Verification Layer: el seguro invisible de los agentes](/magazine/output-verification-layer-seguro-invisible-agentes-produccion-es)

## Fuentes consultadas

- [HERMES: agente de verificación paso a paso en Lean 4](https://github.com/aziksh-ospanov/HERMES)
- [HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs](https://arxiv.org/abs/2511.18760)
- [Lean 4: introducción a demostración y verificación formal](https://lean-lang.org/theorem_proving_in_lean4/introduction.html)

## Proximo paso

Escoge una decisión donde un error sea caro y escribe un único invariante ejecutable. Si el agente no puede adjuntar evidencia comprobable, el sistema debe declarar "no resuelto", no improvisar certeza.

---

_Cite as: Berthelius, V. (2026). "Proof-carrying output: cuando la respuesta crítica debe traer prueba ejecutable". BRTHLS Magazine. https://www.brthls.com/magazine/proof-carrying-output-prueba-ejecutable-agentes-es_