Pipeline
Cómo funciona
Cada acción atraviesa un pipeline determinista de siete etapas. Ninguna acción se considera certificada hasta completar la última.
- 1
Recepción de la acción
El agente envía la acción propuesta con su contexto: estado de origen, parámetros y ámbito declarado.
- 2
Transformación functorial
El funtor envía la acción de la categoría de acciones a la categoría de predicados, preservando composición e identidad.
- 3
Generación del predicado
Se construye el predicado formal asociado a la acción a partir de los invariantes categóricos aplicables.
- 4
Verificación formal
El predicado se comprueba con Z3 y Dafny junto con la verificación de invariantes categóricos.
- 5
Trazabilidad criptográfica
Se emite hash, sello temporal y evidencia verificable del resultado de la verificación.
- 6
Supervisión humana
Si la acción es sensible, la certificación queda pendiente de validación humana explícita.
- 7
Certificación final
La acción queda certificada como predicado verificable y se incorpora al registro de auditoría continua.
Resultado del pipeline
La salida es un certificado por acción: el predicado verificado, la evidencia criptográfica que lo respalda y, cuando procede, el registro de la validación humana.
certificado := {
accion: a
predicado: F(a)
veredicto: verificado | rechazado | pendiente_supervision
invariantes: [ ámbito, seguridad, legalidad, trazabilidad ]
evidencia: { hash, sello_temporal, prueba }
}