Aseguramiento · para auditores y responsables de riesgo
Confianza que puedes
inspeccionar.
La modernización fracasa cuando el nuevo sistema se comporta en silencio de forma distinta al antiguo. Te enteras en producción, en una auditoría o en los tribunales. Constat está construido para que "se comporta igual" sea algo que puedas comprobar, no algo que tengas que creer.
programas NIST COBOL-85 públicos corren byte-exact en IBM i V7R5 real. No es nuestro corpus: programas que cualquiera puede buscar y ejecutar.
Ver uno ejecutado en ambosCómo se construye la garantía
Tres mecanismos, no una promesa
Ejecuta ambos, compara
El original corre en IBM i. El sistema modernizado corre en Rust. Ambos procesan los mismos datos reales de entrada, y comparamos el estado de negocio resultante de forma directa. La equivalencia se mide, no se asume a partir de tests que resulta que pasan.
Un motor verificado
El motor que genera el Rust está respaldado por pruebas matemáticas verificadas por máquina, con un límite de confianza pequeño que declaramos de forma explícita. Es un transpilador verificado, no una herramienta de esfuerzo razonable que espera que la salida coincida.
Evidencia que puedes auditar
Cada programa modernizado se entrega con un paquete de evidencia: qué se produjo, cómo, y la prueba de que se comporta como el original. Tu equipo y tus auditores lo inspeccionan en sus propios términos.
La evidencia, en tres capas
Hasta dónde está probada de verdad cada afirmación
Damos garantías en tres niveles separados, de más amplio a más estrecho. La mayoría de herramientas los mezclan. Nosotros los mantenemos aparte, para que veas exactamente dónde acaba una garantía y empieza un plan.
El pipeline parsea los lenguajes en los que está escrito un parque IBM i y emite Rust idiomático. Es la capa más amplia y la garantía más débil: transpilar código no es, por sí solo, prueba de que el comportamiento se preserva.
El motor que escribe el Rust se verifica dentro del kernel de Lean 4, con una huella de axiomas pequeña y nombrada explícitamente. Nada que sostenga el resultado se asume sin registro.
La capa más estrecha y más fuerte: cada programa corre en hardware IBM i real mientras su gemelo moderno corre con las mismas entradas, comparados byte a byte, con un dossier que cualquiera puede re-verificar. Esto es lo que llamamos probado.
Cada cifra aquí se genera desde los artefactos de referencia. Un número sin fuente no se publica.
El rastro de auditoría
Cada paso se conserva, para que cada paso pueda comprobarse
La modernización solo es de fiar si puedes reconstruirla. Constat conserva el rastro completo desde tu fuente hasta el Rust en ejecución, y te lo entrega. Nada de la transpilación es una caja negra.
Pruebas formales (Lean 4)
La corrección del motor se demuestra en el probador de teoremas Lean 4. Las pruebas están verificadas por máquina, y viajan con el resultado.
Dos solvers, contrastados
Las operaciones que modelamos las descarga el solver SMT Z3 y las re-verifica de forma independiente CVC5, así un fallo en un solver no se cuela. Las fórmulas SMT-LIB2 se pueden emitir para que un tercero las re-chequee.
El rastro de transpilación
Conservamos el árbol de sintaxis abstracta y cada representación intermedia de cada fase. Cómo tu código se convirtió en Rust es abierto, no oculto.
Mapa de fuente a Rust
Cada línea del Rust generado enlaza con el COBOL o RPG del que proviene. Lees el código nuevo contra el antiguo, línea a línea.
Procedencia en cada artefacto
Cada artefacto se registra con su procedencia, de modo que un tercero puede confirmar que nada se cambió ni editó a posteriori.
Re-audítalo tú mismo
Un solo comando re-verifica todo el registro de principio a fin: los artefactos, las pruebas y un registro de exactamente qué generador los produjo. El proceso es determinista, así que dos ejecuciones son byte-idénticas y directamente comparables. Aquí nada necesita tu confianza, solo tu comprobación.
$ axiom audit --json{ "verdict": "COHERENT" }Honestos por defecto
Qué no afirmamos
La equivalencia se establece por programa, sobre tus datos de entrada. No es una garantía general del producto. Un programa que no hemos modernizado y validado no está cubierto, y lo decimos. Cuando un resultado es un objetivo de modernización y no un carril probado, se etiqueta como tal. El alcance siempre es explícito. Una línea más, sobre las pruebas en sí: el generador de código está verificado por el kernel de Lean, pero el Rust final pasa por un paso de post-procesado auditado. Hasta que ese paso se integre en el generador verificado, forma parte de la base de cómputo de confianza, y lo contamos ahí en vez de llamarlo probado.
Mantenemos IBM i (que se ejecuta sobre IBM Power) diferenciado del mainframe (IBM Z). Nuestra validación de comportamiento corre contra hardware IBM i real; los demás destinos se validan dentro de cada proyecto.
Due diligence
Ve tan a fondo como necesites
Para la evaluación técnica llevamos a tus ingenieros y auditores por la prueba y la evidencia de programas reales, bajo NDA. Trae tus preguntas más difíciles.