Input Output hat f\u00fcr Cardano einen neuen Schritt in Richtung automatisierter formaler Verifikation von Smart Contracts vorgestellt. In einem von Romain Soulat ver\u00f6ffentlichten IO-Blogbeitrag beschreibt das Unternehmen zwei neue Open-Source-Formalisierungen f\u00fcr Lean 4, die zusammen mit dem Theorem Prover Blaster eine durchg\u00e4ngige Pr\u00fcfung kompilierter Cardano-Smart-Contracts erm\u00f6glichen sollen. F\u00fcr Entwickler bedeutet das: Eigenschaften von Vertr\u00e4gen aus Plinth, Aiken, Plutarch oder anderen Sprachen k\u00f6nnen gegen das tats\u00e4chlich ausgef\u00fchrte Untyped Plutus Core gepr\u00fcft werden.<\/p>\n
Input Output beschreibt die Neuerung als erstmals vollst\u00e4ndig offene Kette \u201evon einer High-Level-Smart-Contract-Quellsprache bis zu einer maschinengepr\u00fcften Eigenschaft\u201c f\u00fcr 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\u00dft es dazu: \u201eDer Beweis geht entweder durch, oder man erh\u00e4lt einen konkreten Script Context zur\u00fcck, der genau zeigt, wo er nicht durchgeht.\u201c<\/p>\n
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: \u201eDies ist eine neue F\u00e4higkeit f\u00fcr das Cardano-\u00d6kosystem, entwickelt vom Cardano High Assurance Team von IO in enger Zusammenarbeit mit dem Formal-Methods-Team. Sie \u00f6ffnet die T\u00fcr zu Assurance-Arbeit, die f\u00fcr die allt\u00e4gliche Smart-Contract-Entwicklung bisher au\u00dfer Reichweite lag, ohne Entwickler zu zwingen, die Sprachen zu verlassen, die sie bereits verwenden.\u201c 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\u00e4zise formulierte Eigenschaften pr\u00fcfbar sein.<\/p>\n
F\u00fcr Cardano ist der technische Kontext wichtig, weil Plutus-Skripte bei der Ausf\u00fchrung mit Ledger-Daten, Transaktionskontexten und Kostenmodellen interagieren. Genau diese Verbindung war in der Praxis schwer vollst\u00e4ndig abzubilden. IO verweist darauf, dass die neue Pipeline bereits an einem bekannten \u00dcbungsvertrag aus einer \u00f6ffentlichen Security-Challenge demonstriert wurde: Beim Die erste der beiden neuen Komponenten ist PlutusCoreBlaster, eine Lean-4-Formalisierung von Plutus Core, der Sprache, die auf Cardano ausgef\u00fchrt wird. IO beschreibt den Umfang detailliert: \u201eIm Kern stellt die Bibliothek maschinengepr\u00fcfte Definitionen jeder Built-in-Funktion der Plutus-Core-Spezifikation bereit: Integer- und Bytestring-Arithmetik, String-Operationen, Booleans, Listen, Paare und den universellen Data-Typ.\u201c Dar\u00fcber liegt ein vollst\u00e4ndiges Modell von UPLC, einschlie\u00dflich 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.<\/p>\n Erg\u00e4nzt wird PlutusCoreBlaster durch eine eigenst\u00e4ndige Cryptograph-Bibliothek, die kryptografische Primitiven formalisiert, die Plutus als Built-ins verf\u00fcgbar 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\u00fcfung sowie Ed25519 mit EdDSA-Verifikation. IO schreibt: \u201eDie Implementierung besteht 100 Prozent der Konformit\u00e4tstests, mit Ausnahme neu hinzugef\u00fcgter Typen und Built-ins, die sich noch in Arbeit befinden.\u201c<\/p>\n Die zweite Komponente ist CardanoLedgerAPIBlaster, ein Lean-4-Modell der Cardano Ledger API, also der typisierten Schnittstelle, die Plutus-Validatoren zur Ausf\u00fchrungszeit 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: \u201eIm Herzen der Bibliothek sitzt eine Reihe entscheidbarer boolescher Pr\u00e4dikate, die die Validierungsregeln des Cardano-Ledgers codieren: eine ausf\u00fchrbare formale Spezifikation dessen, was das Ledger akzeptiert.\u201c IO betont zudem, dass nicht die Agda-Spezifikation neu implementiert wurde, sondern die vom Node verwendete Variante, weil dort bestimmte Designentscheidungen Script-Optimierungen erm\u00f6glichen und falsche Gegenbeispiele vermieden werden sollen.<\/p>\n Die neuen Lean-4-Bibliotheken verschieben formale Methoden auf Cardano n\u00e4her an den produktiven Entwicklungsalltag. F\u00fcr Teams, die in Plinth, Aiken oder Plutarch arbeiten, entsteht damit ein Weg, kompilierte Contracts gegen pr\u00e4zise Eigenschaften zu pr\u00fcfen und bei Fehlschl\u00e4gen konkrete, ledger-g\u00fcltige Gegenbeispiele zu erhalten. Die weitere Skalierung und zus\u00e4tzliche Abdeckung neuer Plutus-Funktionen sollen 2026 im Rahmen der Cardano-High-Assurance-Arbeit fortgesetzt werden.<\/p>\n KI-Transparenzhinweis: Dieser Artikel wurde mit Unterst\u00fctzung eines KI-Systems auf Basis der angegebenen Quellen vorbereitet und vor der Ver\u00f6ffentlichung redaktionell durch einen menschlichen Editor gepr\u00fcft, bearbeitet und freigegeben. Alle Zitate, Daten und Tatsachenbehauptungen sollen aus den genannten Quellen stammen; dennoch k\u00f6nnen Fehler nicht vollst\u00e4ndig ausgeschlossen werden.<\/em><\/p>\n","protected":false},"excerpt":{"rendered":" Input Output \u00f6ffnet Cardano-Entwicklern eine End-to-End-Verifikation f\u00fcr Smart Contracts \u2013 inklusive Lean-4-Modellen f\u00fcr Plutus Core und Ledger-Regeln.<\/p>\n","protected":false},"author":2,"featured_media":1327,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[72],"tags":[75],"class_list":{"0":"post-1324","1":"post","2":"type-post","3":"status-publish","4":"format-standard","5":"has-post-thumbnail","7":"category-news","8":"tag-cardano"},"yoast_head":"\nnft_sell<\/code>-Contract aus Invariant0s Capture-the-Flag-Challenge importierte das Team UPLC, formalisierte die Spezifikation, dr\u00fcckte die Eigenschaften in Lean 4 aus und lie\u00df Blaster laufen. Das Ergebnis war ein vollst\u00e4ndiger, mit den Ledger-Regeln kompatibler Script Context, der ein Double-Satisfaction-Muster demonstrierte.<\/p>\nLean 4 und Blaster schlie\u00dfen die Pr\u00fcfl\u00fccke<\/h2>\n