Viele der aktuellen Bugs und Exploits im Bereich Kryptowährungen sind auf Mängel oder Schwächen der zugrunde liegenden Blockchain-Programmiersprachen oder virtuellen Maschinen zurückzuführen. Der übliche post-mortem Ansatz zur formalen Semantik und Verifikation von Sprachen, bei dem die Sprache zunächst implementiert und über viele Jahre in der Produktion verwendet wird, bevor der Bedarf an formalen Semantik- und Verifikationstools auf natürliche Weise entsteht, funktioniert einfach nicht mehr. Neue Blockchain-Sprachen oder virtuelle Maschinen werden in alarmierendem Tempo vorgeschlagen, gefolgt von neuen Versionen alle paar Wochen, zusammen mit Programmen (oder Smart Contracts) in diesen Sprachen, die für finanzielle Transaktionen von potenziell erheblichem Wert verantwortlich sind. Daher werden sofort formale Analyse- und Verifikationstools für solche Sprachen und virtuellen Maschinen benötigt. Wir präsentieren aktuelle akademische und kommerzielle Ergebnisse zur Entwicklung von Blockchain-Sprachen und virtuellen Maschinen, die direkt mit formalen Analyse- und Verifikationstools ausgestattet sind. Die Hauptidee besteht darin, all dies automatisch und korrekt-by-construction aus einer formalen Spezifikation zu generieren. Wir demonstrieren die Machbarkeit des vorgeschlagenen Ansatzes, indem wir ihn auf zwei Blockchains, Ethereum und Cardano, anwenden.