Input Output hat für Cardano einen neuen Schritt in Richtung automatisierter formaler Verifikation von Smart Contracts vorgestellt. In einem von Romain Soulat veröffentlichten IO-Blogbeitrag beschreibt das Unternehmen zwei neue Open-Source-Formalisierungen für Lean 4, die zusammen mit dem Theorem Prover Blaster eine durchgängige Prüfung kompilierter Cardano-Smart-Contracts ermöglichen sollen. Für Entwickler bedeutet das: Eigenschaften von Verträgen aus Plinth, Aiken, Plutarch oder anderen Sprachen können gegen das tatsächlich ausgeführte Untyped Plutus Core geprüft werden.
Cardano macht Smart Contracts formal prüfbar
Input Output beschreibt die Neuerung als erstmals vollständig offene Kette „von einer High-Level-Smart-Contract-Quellsprache bis zu einer maschinengeprüften Eigenschaft“ für Cardano-Entwickler. Der Ablauf ist dabei bewusst nah an bestehenden Workflows gehalten: Entwickler schreiben ihren Validator in Plinth, Aiken oder Plutarch, kompilieren ihn zu Untyped Plutus Core, importieren das Ergebnis in Lean 4, formulieren die relevanten Eigenschaften und rufen Blaster auf. Im Blog heißt es dazu: „Der Beweis geht entweder durch, oder man erhält einen konkreten Script Context zurück, der genau zeigt, wo er nicht durchgeht.“
Der zentrale Punkt ist, dass die Verifikation nicht auf einem separaten Modell des Smart Contracts basiert, sondern am kompilierten UPLC ansetzt. IO formuliert das so: „Dies ist eine neue Fähigkeit für das Cardano-Ökosystem, entwickelt vom Cardano High Assurance Team von IO in enger Zusammenarbeit mit dem Formal-Methods-Team. Sie öffnet die Tür zu Assurance-Arbeit, die für die alltägliche Smart-Contract-Entwicklung bisher außer Reichweite lag, ohne Entwickler zu zwingen, die Sprachen zu verlassen, die sie bereits verwenden.“ Damit zielt die Arbeit auf ein praktisches Problem institutioneller und professioneller Smart-Contract-Entwicklung: Fehler sollen nicht nur durch Audits oder Tests gefunden werden, sondern mathematisch gegen präzise formulierte Eigenschaften prüfbar sein.
Für Cardano ist der technische Kontext wichtig, weil Plutus-Skripte bei der Ausführung mit Ledger-Daten, Transaktionskontexten und Kostenmodellen interagieren. Genau diese Verbindung war in der Praxis schwer vollständig abzubilden. IO verweist darauf, dass die neue Pipeline bereits an einem bekannten Übungsvertrag aus einer öffentlichen Security-Challenge demonstriert wurde: Beim nft_sell-Contract aus Invariant0s Capture-the-Flag-Challenge importierte das Team UPLC, formalisierte die Spezifikation, drückte die Eigenschaften in Lean 4 aus und ließ Blaster laufen. Das Ergebnis war ein vollständiger, mit den Ledger-Regeln kompatibler Script Context, der ein Double-Satisfaction-Muster demonstrierte.
Lean 4 und Blaster schließen die Prüflücke
Die erste der beiden neuen Komponenten ist PlutusCoreBlaster, eine Lean-4-Formalisierung von Plutus Core, der Sprache, die auf Cardano ausgeführt wird. IO beschreibt den Umfang detailliert: „Im Kern stellt die Bibliothek maschinengeprüfte Definitionen jeder Built-in-Funktion der Plutus-Core-Spezifikation bereit: Integer- und Bytestring-Arithmetik, String-Operationen, Booleans, Listen, Paare und den universellen Data-Typ.“ Darüber liegt ein vollständiges Modell von UPLC, einschließlich Termtypen wie Variablen, Lambdas, Anwendungen, Built-ins, Konstruktoren und Case Expressions, zweier CEK-Maschinen sowie der in der Praxis genutzten Serialisierungsformate CBOR und Hex-Encoding.
Ergänzt wird PlutusCoreBlaster durch eine eigenständige Cryptograph-Bibliothek, die kryptografische Primitiven formalisiert, die Plutus als Built-ins verfügbar macht. Abgedeckt sind unter anderem SHA-256, SHA-512, SHA3-256, Blake2b-224, Blake2b-256, Keccak-256 und RIPEMD-160, jeweils mit Testvektoren aus NIST-Quellen verifiziert. Auch elliptische Kurven sind enthalten, darunter Secp256k1 mit ECDSA- und Schnorr-Signaturprüfung sowie Ed25519 mit EdDSA-Verifikation. IO schreibt: „Die Implementierung besteht 100 Prozent der Konformitätstests, mit Ausnahme neu hinzugefügter Typen und Built-ins, die sich noch in Arbeit befinden.“
Die zweite Komponente ist CardanoLedgerAPIBlaster, ein Lean-4-Modell der Cardano Ledger API, also der typisierten Schnittstelle, die Plutus-Validatoren zur Ausführungszeit sehen. Die Bibliothek ist um die API-Generationen V1, V2 und V3 strukturiert und definiert zentrale Ledger-Typen wie Adressen mit Zahlungs- und Staking-Credentials, Multi-Asset-Values, TxInfo, ScriptContext, ScriptPurpose, POSIX-Zeitbereiche und Zertifikatstypen. Entscheidend ist die Abbildung der Validierungslogik: „Im Herzen der Bibliothek sitzt eine Reihe entscheidbarer boolescher Prädikate, die die Validierungsregeln des Cardano-Ledgers codieren: eine ausführbare formale Spezifikation dessen, was das Ledger akzeptiert.“ IO betont zudem, dass nicht die Agda-Spezifikation neu implementiert wurde, sondern die vom Node verwendete Variante, weil dort bestimmte Designentscheidungen Script-Optimierungen ermöglichen und falsche Gegenbeispiele vermieden werden sollen.
Die neuen Lean-4-Bibliotheken verschieben formale Methoden auf Cardano näher an den produktiven Entwicklungsalltag. Für Teams, die in Plinth, Aiken oder Plutarch arbeiten, entsteht damit ein Weg, kompilierte Contracts gegen präzise Eigenschaften zu prüfen und bei Fehlschlägen konkrete, ledger-gültige Gegenbeispiele zu erhalten. Die weitere Skalierung und zusätzliche Abdeckung neuer Plutus-Funktionen sollen 2026 im Rahmen der Cardano-High-Assurance-Arbeit fortgesetzt werden.
KI-Transparenzhinweis: Dieser Artikel wurde mit Unterstützung eines KI-Systems auf Basis der angegebenen Quellen vorbereitet und vor der Veröffentlichung redaktionell durch einen menschlichen Editor geprüft, bearbeitet und freigegeben. Alle Zitate, Daten und Tatsachenbehauptungen sollen aus den genannten Quellen stammen; dennoch können Fehler nicht vollständig ausgeschlossen werden.