Nachweis · für Prüfer & Risikoverantwortliche
Vertrauen, das Sie
prüfen können.
Modernisierung scheitert, wenn sich das neue System still anders verhält als das alte. Sie merken es in der Produktion, in einem Audit oder vor Gericht. Constat ist so gebaut, dass "es verhält sich gleich" etwas ist, das Sie prüfen können, nicht etwas, das Sie glauben müssen.
öffentliche NIST-COBOL-85-Programme laufen Byte-genau auf echtem IBM i V7R5. Nicht unser Korpus, sondern Programme, die jeder nachschlagen und selbst ausführen kann.
Eines auf beiden ausgeführt ansehenWie die Zusicherung entsteht
Drei Mechanismen, kein bloßes Versprechen
Beide laufen lassen, vergleichen
Das Original läuft auf IBM i. Das modernisierte System läuft in Rust. Beide verarbeiten dieselben echten Eingaben, und wir vergleichen den resultierenden Geschäftszustand direkt. Äquivalenz wird gemessen, nicht aus Tests angenommen, die zufällig bestehen.
Eine verifizierte Engine
Die Engine, die das Rust erzeugt, ist durch maschinengeprüfte mathematische Beweise abgesichert, mit einer kleinen, explizit benannten Vertrauensgrenze. Es ist ein verifizierter Transpiler, kein Best-Effort-Werkzeug, das auf passende Ausgabe hofft.
Nachweise, die Sie prüfen können
Jedes modernisierte Programm kommt mit einem Nachweispaket: was erzeugt wurde, wie, und der Beweis, dass es sich wie das Original verhält. Ihr Team und Ihre Prüfer sehen es zu ihren eigenen Bedingungen ein.
Die Evidenz, in drei Schichten
Wie weit jede Aussage wirklich bewiesen ist
Wir weisen Sicherheit auf drei getrennten Ebenen aus, von der breitesten zur engsten. Die meisten Werkzeuge vermischen sie. Wir halten sie auseinander, damit Sie genau sehen, wo eine Garantie endet und eine Roadmap beginnt.
Die Pipeline parst die Sprachen, in denen ein IBM i Bestand geschrieben ist, und erzeugt idiomatisches Rust. Das ist die breiteste Schicht und die schwächste Garantie: Code zu transpilieren ist für sich genommen kein Beweis, dass das Verhalten erhalten bleibt.
Der Generator, der das Rust schreibt, wird im Lean-4-Kernel geprüft, mit einem kleinen, explizit benannten Axiom-Fußabdruck. Nichts Tragendes wird ohne Nachweis angenommen.
Die engste und stärkste Schicht: Jedes Programm läuft auf echter IBM i Hardware, während sein modernes Gegenstück mit denselben Eingaben läuft, Byte für Byte verglichen, mit einem Dossier, das jeder nachprüfen kann. Das meinen wir mit bewiesen.
Jede Zahl hier wird aus den Artefakten of record generiert. Eine Zahl ohne Quelle wird nicht ausgeliefert.
Der Prüfpfad
Jeder Schritt bleibt erhalten, damit jeder Schritt prüfbar ist
Modernisierung ist nur vertrauenswürdig, wenn Sie sie zurückverfolgen können. Constat bewahrt den vollständigen Pfad von Ihrem Quellcode bis zum laufenden Rust und übergibt ihn Ihnen. Nichts an der Transpilation ist eine Blackbox.
Formale Beweise (Lean 4)
Die Korrektheit der Engine wird im Beweisassistenten Lean 4 bewiesen. Die Beweise sind maschinengeprüft und reisen mit dem Ergebnis mit.
Zwei Solver, gegengeprüft
Die von uns modellierten Operationen werden vom SMT-Solver Z3 entschieden und von CVC5 unabhängig gegengeprüft, sodass ein Fehler in einem Solver nicht durchrutscht. Die SMT-LIB2-Formeln können für eine Drittprüfung ausgegeben werden.
Die Transpilationsspur
Wir bewahren den abstrakten Syntaxbaum und jede Zwischenrepräsentation aus jeder Stufe. Wie Ihr Code zu Rust wurde, liegt offen, nicht verborgen.
Quellcode-zu-Rust-Zuordnung
Jede Zeile des erzeugten Rust verweist zurück auf das COBOL oder RPG, aus dem sie stammt. Sie lesen den neuen Code gegen den alten, Zeile für Zeile.
Herkunft für jedes Artefakt
Jedes Artefakt wird mit seiner Herkunft festgehalten, sodass ein Dritter bestätigen kann, dass nachträglich nichts vertauscht oder verändert wurde.
Prüfen Sie es selbst nach
Ein einziger Befehl prüft den gesamten Datensatz von Anfang bis Ende erneut: die Artefakte, die Beweise und einen Nachweis, welcher Generator sie genau erzeugt hat. Der Prozess ist deterministisch, sodass zwei Läufe byte-identisch und direkt vergleichbar sind. Hier braucht nichts Ihr Vertrauen, nur Ihre Prüfung.
$ axiom audit --json{ "verdict": "COHERENT" }Ehrlich von Grund auf
Was wir nicht behaupten
Äquivalenz wird pro Programm nachgewiesen, mit Ihren Eingaben. Sie ist keine pauschale Produktgarantie. Ein Programm, das wir nicht modernisiert und validiert haben, ist nicht abgedeckt, und das sagen wir. Wo ein Ergebnis ein Modernisierungsziel statt einer bewiesenen Spur ist, wird es als solches gekennzeichnet. Der Umfang ist immer explizit. Und eine Zeile zu den Beweisen selbst: Der Codegenerator wird im Lean-Kernel maschinell geprüft, doch das finale Rust durchläuft einen auditierten Nachbearbeitungsschritt. Bis dieser Schritt in den verifizierten Generator übernommen ist, gehört er zur Trusted Computing Base, und wir zählen ihn dort, statt ihn als bewiesen auszugeben.
Wir halten IBM i (das auf IBM Power läuft) getrennt vom Mainframe (IBM Z). Unsere Verhaltensvalidierung läuft gegen echte IBM i Hardware; andere Ziele werden in jedem Projekt validiert.
Due Diligence
Gehen Sie so tief, wie Sie müssen
Für die technische Bewertung führen wir Ihre Entwickler und Prüfer durch den Beweis und die Nachweise für echte Programme, unter NDA. Bringen Sie Ihre schwierigsten Fragen mit.