Muchos de los errores y exploits recientes en criptomonedas se deben a fallos o debilidades de los lenguajes de programación de blockchain o máquinas virtuales subyacentes. El enfoque habitual de post-mortem sobre la semántica y verificación formal de lenguajes, donde el lenguaje se implementa y utiliza en producción durante muchos años antes de que surja la necesidad de herramientas de semántica y verificación formal, simplemente ya no funciona. Nuevos lenguajes de blockchain o máquinas virtuales se proponen a un ritmo alarmante, seguidos de nuevas versiones de ellos cada pocas semanas, junto con programas (o contratos inteligentes) en estos lenguajes que son responsables de transacciones financieras de valor potencialmente significativo. Por lo tanto, se necesitan de inmediato herramientas de análisis y verificación formal para tales lenguajes y máquinas virtuales. Presentamos resultados académicos y comerciales recientes en el desarrollo de lenguajes de blockchain y máquinas virtuales que vienen directamente equipados con herramientas de análisis y verificación formal. La idea principal es generar todo esto automáticamente, correcto por construcción a partir de una especificación formal. Demostramos la viabilidad del enfoque propuesto aplicándolo a dos blockchains, Ethereum y Cardano.