Die Modernisierung von COBOL-Anwendungen stellt gerade Banken und Versicherungen vor eine grundlegende Herausforderung: Bei der Übertragung bestehender Geschäftslogik in eine andere Programmiersprache darf sich das Verhalten der Anwendung nicht unbemerkt verändern. Besonders kritisch sind Abweichungen bei Berechnungen, Rundungen oder Verzweigungen, die bei herkömmlichen Tests möglicherweise unentdeckt bleiben.
Funktionale Gleichwertigkeit von COBOL- und Python-Programmen im Fokus
Dominik Blain, Entwickler des Verfahrens IRONPROOF, untersucht in einer in diesem Monat veröffentlichten Studie, ob sich die funktionale Gleichwertigkeit von COBOL- und Python-Programmen mathematisch überprüfen lässt. Der Ansatz kombiniert eine regelbasierte Codeübersetzung mit dem sogenannten SMT-Solver Z3. Dieser soll feststellen, ob es Eingabewerte gibt, bei denen die beiden Programmversionen unterschiedliche Ergebnisse berechnen.
Dazu wird der ursprüngliche COBOL-Code zunächst in eine interne Darstellung überführt und anschließend Python-Code erzeugt. Beide Versionen werden mathematisch modelliert und miteinander verglichen. Kann der Solver innerhalb des untersuchten Modells keine Abweichung finden, erstellt das Werkzeug einen überprüfbaren Äquivalenznachweis. Findet es einen Unterschied, kann es konkrete Eingabewerte benennen, bei denen die Ergebnisse auseinanderlaufen.
Der Ansatz greift auf Verfahren der formalen Softwareverifikation zurück, die seit Jahrzehnten Gegenstand der Compilerforschung sind. Dabei wird mithilfe mathematischer Methoden überprüft, ob eine Programmtransformation das ursprüngliche Verhalten erhält. IRONPROOF versucht, dieses Prinzip auf die sprachübergreifende Übersetzung von COBOL nach Python anzuwenden.
Die vom Autor veröffentlichte Grafik zeigt den Ablauf von der COBOL-Analyse über die Python-Generierung bis zur mathematischen Prüfung mit Z3. Bei festgestellten Abweichungen sieht das Verfahren eine KI-gestützte Korrekturschleife vor. (Quelle: Dominik Blain, IRONPROOF: COBOL-to-Python Transpilation with SMT-Based Equivalence Checking, Abbildung 1, S. 3, arXiv:2610.11073v1 (2026))
Mathematischer Nachweis bei 606 Programmen
Für seine Untersuchung stellte Blain eine Sammlung von 2.345 COBOL-Dateien zusammen. Sie stammen unter anderem aus der Testsuite des Open-Source-Compilers GnuCOBOL, einer Validierungssuite des US-amerikanischen National Institute of Standards and Technology (NIST), öffentlich verfügbaren Programmsammlungen sowie selbst entwickelten Testprogrammen.
Allerdings konnten nur 782 Programme überhaupt in den mathematischen Prüfprozess aufgenommen werden. Bei den übrigen 1.563 Programmen fehlten Ausgaben, die das Verfahren mit seinen derzeitigen Möglichkeiten modellieren konnte. Zu den wesentlichen Einschränkungen zählen Dateioperationen, eingebettetes SQL und bestimmte Schleifenkonstruktionen.
Von den 782 überprüfbaren Programmen erhielten 606 einen Äquivalenznachweis. Das entspricht 77,5 Prozent. Bei 101 Programmen gelang lediglich eine teilweise Verifikation, während 75 an Fehlern innerhalb der eigenen Verarbeitungskette scheiterten.
Deutlich niedriger fiel die Erfolgsquote bei Programmen aus, die nicht vom Entwickler selbst stammten. Hier gelang der Nachweis bei 153 von 291 Programmen, also bei 52,6 Prozent. Bei selbst erstellten oder generierten Programmen lag die Quote dagegen bei 92,3 Prozent.
Die Zahlen zeigen nach Darstellung des Autors, wie stark die Ergebnisse von der Zusammensetzung der Testbasis und den unterstützten Sprachkonstruktionen abhängen. Hinzu kommt, dass die untersuchten Programme überwiegend klein waren: Der Median der gesamten Testsammlung lag bei 18 nicht leeren Codezeilen.
Hintergrund: Mathematische Verifikation in der Compilerforschung
Die Überprüfung, ob eine Programmübersetzung oder -optimierung das ursprüngliche Verhalten bewahrt, ist ein etabliertes Forschungsgebiet. Zwei wichtige Ansätze sind die formale Verifikation eines Compilers und die sogenannte Translation Validation, bei der einzelne Programmtransformationen geprüft werden. Bekannte Beispiele sind:
CompCert: Ein formal verifizierter C-Compiler, dessen Korrektheitsnachweis auf dem Beweisassistenten Coq basiert. Maßgeblich entwickelt wurde er unter Leitung des französischen Informatikers Xavier Leroy.
Alive2: Ein Werkzeug, das mithilfe von SMT-Solvern überprüft, ob Optimierungen innerhalb der LLVM-Compilerinfrastruktur das Programmverhalten erhalten.
SymDiff: Ein von Forschern unter anderem bei Microsoft Research vorgestelltes Werkzeug zur semantischen Gegenüberstellung von Programmen.
Was ein mathematischer Beweis tatsächlich aussagt
Eine zentrale Erkenntnis der Studie betrifft die Aussagekraft der Verifikation selbst. IRONPROOF überprüft, ob der generierte Python-Code mit einer zuvor erstellten internen Darstellung des COBOL-Programms übereinstimmt. Ob diese Darstellung das tatsächliche Verhalten des ursprünglichen COBOL-Codes vollständig und korrekt erfasst, wird damit noch nicht bewiesen.
Gerade bei COBOL ist diese Unterscheidung relevant. Die Sprache verfügt über Besonderheiten bei numerischen Datentypen, Feldlängen und der Verarbeitung von Rechenergebnissen. So können Werte beim Speichern in ein begrenztes Datenfeld abgeschnitten werden. Das mathematische Modell von IRONPROOF bildet solche Effekte bislang nicht vollständig ab.
Wie relevant diese Einschränkung ist, zeigt ein zusätzlicher Vergleich mit der COBOL-Laufzeitumgebung GnuCOBOL 3.2.0. Bei 24 von 49 ausführbaren, unabhängig entwickelten Programmen, für die zuvor ein Äquivalenznachweis vorlag, stellte Blain Abweichungen zwischen dem Modell und der tatsächlichen Programmausführung fest.
Diese Ergebnisse beziehen sich allerdings auf eine frühere Version von IRONPROOF vom August 2026. Der Vergleich wurde mit der aktuellen Version noch nicht wiederholt. Blain bezeichnet eine erneute, reproduzierbare Überprüfung selbst als vorrangige Aufgabe.
Eine weitere Einschränkung betrifft die berücksichtigten Eingabewerte. Von den insgesamt 606 Äquivalenznachweisen bezogen sich lediglich 14 auf variable Eingaben, die tatsächlich Einfluss auf eine nachgewiesene Ausgabe hatten. Die meisten Nachweise betrafen Programme mit festgelegten Werten und damit nur einem möglichen Ausführungsverlauf.
Komplexe Geschäftsanwendungen bleiben eine Herausforderung
Wie weit das Verfahren von der Verarbeitung umfangreicher Geschäftsanwendungen entfernt ist, untersuchte Blain zusätzlich anhand zweier öffentlich verfügbarer COBOL-Anwendungssammlungen: AWS CardDemo und IBM GenApp.
Die insgesamt 75 Programme enthalten typische Elemente geschäftlicher Anwendungen, darunter CICS-Bezüge, Datenbankzugriffe und komplexere Programmabläufe. Bei keinem dieser Programme gelang es IRONPROOF, den vollständigen Ablauf mathematisch zu modellieren. Von insgesamt 712 untersuchten Programmabschnitten konnte lediglich einer vollständig erfasst werden.
Damit dokumentiert die Untersuchung eine erhebliche Lücke zwischen der Verifikation einzelner Rechenoperationen und der Absicherung vollständiger Geschäftsanwendungen.
Vergleich mit KI-gestützter Codeübersetzung
Die Studie enthält außerdem einen Vergleich mit einer direkten COBOL-nach-Python-Übersetzung durch ein großes Sprachmodell. In einem Versuch vom April 2026 verwendete Blain dafür Claude Opus 4.7.
Bei 94 unabhängig entwickelten COBOL-Programmen stellte die anschließende Prüfung in 30 Fällen konkrete semantische Fehler fest. Weitere 24 Übersetzungen konnten mit dem eingesetzten Prüfverfahren nicht verifiziert werden. Insgesamt blieben damit 54 Übersetzungen ohne erfolgreichen Äquivalenznachweis.
Die Untersuchung belegt allerdings keine allgemeine Fehlerquote von KI-gestützten COBOL-Migrationen. Getestet wurde nur ein Sprachmodell, und ein fehlender Nachweis bedeutet nicht zwangsläufig, dass der erzeugte Python-Code fehlerhaft ist. Zudem wurden die Vergleichsläufe zu unterschiedlichen Zeitpunkten mit unterschiedlichen Entwicklungsständen des Prüfverfahrens durchgeführt.
Blain beschreibt darüber hinaus eine Möglichkeit, erkannte Abweichungen automatisch an ein Sprachmodell zurückzumelden, damit dieses den Python-Code korrigieren kann. Die Wirksamkeit dieser Korrekturschleife wurde in der Studie jedoch nicht systematisch untersucht.
Einordnung: Verifikation als zusätzlicher Prüfmechanismus
Die Ergebnisse machen deutlich, dass mathematische Verfahren einen zusätzlichen Beitrag zur Qualitätssicherung bei der Code-Migration leisten können. Anders als gewöhnliche Testverfahren können sie innerhalb eines korrekt definierten Modells systematisch nach Eingaben suchen, die zu abweichenden Ergebnissen führen.
Zugleich zeigt die Untersuchung, dass die Qualität eines solchen Nachweises wesentlich davon abhängt, wie vollständig das ursprüngliche Programmverhalten modelliert wird. Gerade typische Eigenschaften gewachsener COBOL-Anwendungen – darunter Datenbankzugriffe, Dateioperationen, komplexe Kontrollflüsse und sprachspezifische Datentypen – stellen das untersuchte Verfahren bislang vor erhebliche Schwierigkeiten.
Blain entwickelt IRONPROOF selbst und weist in der Veröffentlichung ausdrücklich auf ein finanzielles Interesse an dem untersuchten System hin. Auf der Website des Anbieters wird formale Verifikation zudem als Technologieansatz für unterschiedliche Anwendungsfelder positioniert. Die Studie ist deshalb auch als technische Untersuchung eines Anbieters über sein eigenes Verfahren einzuordnen. Ein Vergleich mit kommerziellen Modernisierungswerkzeugen von IBM oder AWS wurde nicht durchgeführt.
Für Unternehmen mit gewachsenen IT-Landschaften liefert die Erhebung damit vor allem eine Erkenntnis: Automatisierte Codeübersetzung und der Nachweis funktionaler Gleichwertigkeit sind zwei unterschiedliche Aufgaben. Formale Verifikation kann helfen, Abweichungen aufzudecken. Ob eine modernisierte Anwendung tatsächlich das Verhalten ihres Vorgängers bewahrt, muss jedoch auch gegenüber der ursprünglichen Laufzeitumgebung und unter realistischen Betriebsbedingungen überprüft werden. (td)
