Michelson (Tezos) Börsenlexikon Vorheriger Begriff: Metcalfe's Law Nächster Begriff: Miner

Michelson ist die domänenspezifische Programmiersprache für Smart Contracts auf der Tezos-Blockchain. Sie wurde speziell für Tezos entwickelt und unterscheidet sich grundlegend von anderen Smart-Contract-Sprachen wie Solidity (Ethereum) oder Rust (Solana), da sie stackbasiert, funktional und formell überprüfbar ist. Ziel von Michelson ist es, sichere, transparente und verifizierbare Verträge zu ermöglichen – ein zentrales Element des Tezos-Ökosystems, das besonderen Wert auf formale Verifikation und Governance-Fähigkeit legt.

Einordnung und Zielsetzung

Michelson steht im Zentrum der Tezos-Architektur und dient als Low-Level-Sprache für die Ausführung von Smart Contracts. Im Gegensatz zu vielen anderen Blockchains wird Michelson nicht durch die Community ersetzt oder weiter abstrahiert, sondern bildet die einzige direkt ausführbare Sprache im Tezos-Protokoll.

Die wesentlichen Ziele von Michelson sind:

1. Formale Verifizierbarkeit: Ermöglicht mathematische Beweise über Korrektheit und Sicherheit von Smart Contracts.

2. Determinismus und Einfachheit: Vermeidung von Nebeneffekten, keine unbegrenzten Schleifen, vollständige Vorhersagbarkeit der Ausführung.

3. Sicherheit auf Protokollebene: Die Sprache ist integraler Bestandteil der Governance – etwa bei Protokoll-Upgrades.

4. Transparenz und Lesbarkeit: Michelson ist vollständig transparent und standardisiert – kein proprietärer Bytecode.

Sprachcharakteristik

Michelson ist eine statische, typisierte, stackbasierte Sprache, in der alle Operationen über einen Stack ablaufen. Die Syntax ist an S-Expressions (Lisp-artige Strukturen) angelehnt, jedoch mit spezifischem Fokus auf deterministische Ausführung und formale Analyse.

Wichtige Eigenschaften:

• Turing-vollständig, aber ohne klassische Schleifen

• Keine Nebenwirkungen außerhalb des Kontrakts

• Kein Zugriff auf globale Speicherbereiche – nur lokaler Speicher und Parameter

• Strenge Typsicherheit – jeder Ausdruck und jeder Stack-Übergang ist typgeprüft

Beispiel für eine einfache Michelson-Anweisung:

parameter int;
storage int;
code { CAR; PUSH int 1; ADD; NIL operation; PAIR }

Dieser Code empfängt einen ganzzahligen Parameter, addiert 1 und speichert das Ergebnis. Es handelt sich um eine typische Struktur: parameter, storage, code.

Typensystem und Stack-Operationen

Michelson arbeitet ausschließlich mit einem Stack, der während der Ausführung verändert wird. Jeder Befehl nimmt eine bestimmte Anzahl von Stackelementen auf und gibt veränderte Elemente zurück.

Typische Datentypen:

• Primitive Typen: int, nat, string, bool, bytes, mutez (Tezos-Währungseinheit)

• Strukturierte Typen: pair, option, list, map, set

• Spezielle Typen: operation, timestamp, address, contract, key_hash

Beispielhafter Ablauf:

1. PUSH int 5 – legt die Zahl 5 auf den Stack

2. PUSH int 3 – legt die Zahl 3 auf den Stack

3. ADD – nimmt die beiden Zahlen vom Stack und legt ihre Summe (8) zurück

Speicher- und Kontraktstruktur

Jeder Michelson-Vertrag besteht aus drei wesentlichen Komponenten:

1. parameter – der Datentyp, der beim Aufruf übergeben wird

2. storage – der persistent gespeicherte Zustand

3. code – der eigentliche Anweisungsblock, der Stack-Operationen enthält

Beispiel für eine Kontraktdefinition:

parameter nat;
storage nat;
code {
    DUP;
    DIP { DUP };
    ADD;
    NIL operation;
    PAIR
}

Dieser Code dupliziert den Parameter, addiert ihn zum aktuellen Speicherwert und gibt den neuen Zustand zusammen mit einer leeren Liste von Operationen zurück.

Sicherheit und formale Verifikation

Ein zentraler Vorteil von Michelson ist die Möglichkeit, formale Verifikationen durchzuführen. Dabei handelt es sich um mathematisch beweisbare Aussagen über das Verhalten eines Smart Contracts, etwa:

• Ein Vertrag wird niemals abstürzen

• Es können keine unzulässigen Speicherzustände erreicht werden

• Ein bestimmtes Invariantenverhalten bleibt gewahrt

Tezos verwendet dazu Tools wie:

• Mi-Cho-Coq: Ein Coq-basiertes Framework zur formalen Verifikation von Michelson-Code

• Why3: Eine Plattform zur automatisierten Generierung von Beweisen

• Static Analyzers: Werkzeuge zur automatisierten Prüfung auf Stackfehler, Endlichkeit und Typkonsistenz

High-Level-Sprachen, die in Michelson kompilieren

Da Michelson eine Low-Level-Sprache ist, wird sie häufig nicht direkt geschrieben, sondern über High-Level-Sprachen erzeugt, darunter:

• LIGO (PascaLIGO, CameLIGO, ReasonLIGO): Typsichere, für Entwickler vertraute Sprachen

• SmartPy: Python-ähnliche Syntax, populär in der Tezos-Community

• Archetype: DSL speziell für rechtssichere Verträge

• JSLIGO: JavaScript-nahe Alternative für Webentwickler

Diese Sprachen erlauben eine abstraktere Entwicklung und erzeugen durch Kompilierung lesbaren, validierten Michelson-Code.

Relevanz im Tezos-Ökosystem

Michelson ist mehr als nur eine Sprache – sie ist ein integraler Bestandteil der Tezos-Governance-Mechanik:

• Protokoll-Upgrades enthalten häufig neue Anweisungen oder Optimierungen im Michelson-Code

• Governance-Votes stimmen oft über Michelson-Erweiterungen ab

• Verträge auf Tezos werden direkt in Michelson gespeichert und ausgeführt

Damit unterscheidet sich Michelson grundlegend von anderen Smart-Contract-Umgebungen, bei denen der ausführbare Code eine vom Compiler erzeugte Zwischenform ist, deren Interpretation nicht Teil des Protokolls ist.

Fazit

Michelson ist eine spezialisierte, stackbasierte und formal überprüfbare Sprache für Smart Contracts auf der Tezos-Blockchain. Ihr Design folgt strengen sicherheits- und verifizierungsbezogenen Prinzipien, um transparente und mathematisch analysierbare Verträge zu ermöglichen. Obwohl die Sprache komplex und ungewohnt erscheint, liegt ihre Stärke in der Formalisierbarkeit und der direkten Integration in das Tezos-Protokoll. In Kombination mit High-Level-Sprachen und Werkzeugen zur Verifikation stellt Michelson ein mächtiges Fundament für sichere und governancefähige Smart-Contract-Entwicklung im Tezos-Ökosystem dar.