News
Zellic verifiziert Plonky2-Gate für dezentrale Börse Lighter mathematisch formal
Von KryptoRatgeber · veröffentlicht 15. Juni 2026
Das Sicherheitsunternehmen Zellic hat am 15. Juni 2026 eine formale Verifikation von Plonky2-Gates für die dezentrale Börse Lighter abgeschlossen und die Ergebnisse öffentlich dokumentiert. Dabei wurden zentrale Bausteine des ZK-Circuits mathematisch auf Korrektheit geprüft – ein Prozess, der über klassische Code-Audits deutlich hinausgeht. Für deutsche DeFi-Nutzer ist das relevant, weil solche mathematischen Garantien die Grundlage für vollständig verifizierbare Handelsvorgänge bilden und Sicherheitslücken auf einer sehr fundamentalen Ebene ausschließen sollen.
Zellic beweist Korrektheit des U32AddManyGate in Plonky2 mathematisch
Am 15. Juni 2026 veröffentlichte das Sicherheitsunternehmen Zellic die Ergebnisse einer formalen Verifikation von Plonky2-Gates, die es im Auftrag von Lighter durchgeführt hat. Lighter ist eine dezentrale Börse, die auf vollständig verifizierbaren Handelsvorgängen aufbaut. Die Details beschreibt Formal Verification of a Plonky2 Gate (Zellic).
Plonky2, das rekursive Proof-System von Polygon, definiert Circuits aus einzelnen Gates, die jeweils Polynomial-Constraints festlegen. Zellic wählte das U32AddManyGate als konkretes Beispiel — ein Gate, das die Summe mehrerer 32-Bit-Ganzzahlen berechnet und dabei Limb-Decomposition sowie Range-Checks einsetzt, um sowohl die Summe als auch einen Übertragswert (carryOut) zu begrenzen. Die zugrunde liegenden Constraints sind als Polynome über dem Goldilocks-Feld mit der Primzahl p = 2⁶⁴ − 2³² + 1 definiert.
Der vierstufige Verifikationsprozess umfasste den Export der Constraints aus Rust in den Beweisassistenten Lean, deren Generalisierung, das Schreiben einer formalen Spezifikation sowie den abschließenden Beweis von Soundness und Completeness — zwei voneinander unabhängigen Beweiszielen, die zusammen sicherstellen, dass das Gate weder zu wenig noch zu viel akzeptiert.
Formale Verifikation als Qualitätsmerkmal — was sie leistet und was nicht
Klassische Sicherheitsaudits prüfen, ob ein Code offensichtliche Fehler enthält. Formale Verifikation geht einen entscheidenden Schritt weiter: Sie beweist mathematisch, dass ein System unter allen möglichen Eingaben korrekt funktioniert — oder eben nicht. Für Zero-Knowledge-Circuits ist dieser Unterschied besonders bedeutsam, weil ein einziges fehlerhaftes Gate die gesamte Beweiskette untergräbt. Ein bösartiger Prover könnte dann gültige ZK-Beweise für inhaltlich falsche Aussagen erzeugen, ohne dass dies nach außen sichtbar wird.
Die Arbeit von Zellic für Lighter zeigt, dass die Branche zunehmend erkennt: Je komplexer ein ZK-Proof-System, desto größer die Lücke zwischen "auditiert" und "mathematisch gesichert". Polygon's Plonky2-Arithmetik operiert über dem Goldilocks-Feld — einem Zahlenraum mit spezifischen algebraischen Eigenschaften, in dem sich Fehler subtil und schwer auffindbar einschleichen können.
Gleichzeitig gilt: Die Verifikation einzelner Gates schließt nicht automatisch Sicherheitsprobleme auf anderen Ebenen aus — etwa in der übergeordneten Circuit-Komposition, in Smart Contracts oder in der Systemarchitektur. Formale Verifikation ist kein Generalfreifahrtschein, sondern ein präzises Instrument für einen klar abgegrenzten Bereich.
Für die deutschsprachige DeFi-Community ist relevant zu verstehen, dass "formal verifiziert" eine spezifische technische Aussage ist — keine allgemeine Qualitätsgarantie für ein Protokoll als Ganzes. Der Begriff verdient Präzision, nicht Pauschalvertrauen.
Warum Gates in ZK-Proof-Systemen über die Sicherheit einer ganzen Börse entscheiden
Zero-Knowledge Proofs ermöglichen es, die Korrektheit von Berechnungen nachzuweisen, ohne die zugrundeliegenden Daten offenzulegen. In DeFi-Protokollen wie Lighter kommen sie zum Einsatz, um jeden Handelsvorgang vollständig und überprüfbar abzuwickeln.
Plonky2 — ein rekursives Proof-System von Polygon — baut dabei auf sogenannten Gates auf: atomare Bausteine eines Circuits, die mathematische Beziehungen als Polynomial-Constraints beschreiben. Jeder Gate muss zwei Eigenschaften erfüllen: Soundness (nur wahre Aussagen erzeugen gültige Beweise) und Completeness (jede wahre Aussage lässt sich tatsächlich beweisen). Ein Gate, das diese Eigenschaften verletzt, öffnet einem bösartigen Prover die Tür, falsche Zustände als korrekt auszugeben.
Klassische Smart Contract Audits prüfen Code auf bekannte Muster und Schwachstellen — sie können jedoch keine mathematische Garantie liefern. Formale Verifikation geht weiter: Sie beweist Eigenschaften maschinell und lückenlos für alle möglichen Eingaben.
Häufige Fragen
Was unterscheidet formale Verifikation von einem klassischen Smart-Contract-Audit?
Ein Smart Contract Audit prüft Code auf bekannte Schwachstellen und logische Fehler – überwiegend durch menschliche Experten und heuristische Werkzeuge. Formale Verifikation geht weiter: Sie beweist mathematisch, dass eine Implementierung exakt ihrer Spezifikation entspricht. Beim Plonky2-Gate bedeutet das konkret, dass Soundness und Completeness als Theoreme bewiesen wurden – nicht nur plausibel erscheinen.
Was bedeutet Soundness und Completeness im Kontext von Plonky2?
Die beiden Begriffe beschreiben zwei getrennte Sicherheitseigenschaften. Soundness garantiert: Sind die Polynomial-Constraints eines Gates erfüllt, gilt zwingend auch die fachliche Spezifikation. Completeness garantiert die Umkehrung: Gilt die Spezifikation, existieren stets Witness-Werte, die die Constraints erfüllen. Fehlt eine dieser Eigenschaften, können entweder ungültige Beweise akzeptiert oder gültige Beweise nicht erzeugt werden.
Warum ist ein einzelnes fehlerhaftes Gate so kritisch?
Gates sind die fundamentalen Bausteine eines ZK-Circuits. Ein einziger Fehler in einem Gate kann es einem bösartigen Prover ermöglichen, gültige Beweise für falsche Aussagen zu erzeugen – etwa für Handelsvorgänge, die nie stattgefunden haben. Formale Verifikation schließt dieses Risiko auf mathematischer Ebene aus.