De nombreux bugs et exploits récents dans les cryptomonnaies sont dus à des défauts ou des faiblesses des langages de programmation blockchain ou des machines virtuelles sous-jacentes. L'approche habituelle d'analyse post-mortem des sémantiques des langages formels et de vérification, où le langage est d'abord mis en œuvre et utilisé en production pendant de nombreuses années avant qu'un besoin d'outils de sémantique formelle et de vérification n'émerge naturellement, ne fonctionne tout simplement plus. De nouveaux langages blockchain ou machines virtuelles sont proposés à un rythme alarmant, suivis de nouvelles versions toutes les quelques semaines, ainsi que des programmes (ou contrats intelligents) dans ces langages qui sont responsables de transactions financières d'une valeur potentiellement significative. Des outils d'analyse et de vérification formelles sont donc nécessaires immédiatement pour ces langages et machines virtuelles. Nous présentons des résultats académiques et commerciaux récents dans le développement de langages blockchain et de machines virtuelles qui sont directement équipés d'outils d'analyse et de vérification formelles. L'idée principale est de générer tout cela automatiquement, correct par construction à partir d'une spécification formelle. Nous démontrons la faisabilité de l'approche proposée en l'appliquant à deux blockchains, Ethereum et Cardano.