Muitos dos bugs e explorações recentes em criptomoedas são devido a falhas ou vulnerabilidades das linguagens de programação de blockchain ou máquinas virtuais subjacentes. A abordagem usual de pós-morte para semântica de linguagem formal e verificação, onde a linguagem é primeiramente implementada e utilizada em produção por muitos anos antes que a necessidade de ferramentas de semântica formal e verificação surja naturalmente, simplesmente não funciona mais. Novas linguagens de blockchain ou máquinas virtuais são propostas a uma taxa alarmante, seguidas por novas versões delas a cada poucas semanas, juntamente com programas (ou contratos inteligentes) nessas linguagens que são responsáveis por transações financeiras de valor potencialmente significativo. Ferramentas de análise e verificação formal são, portanto, necessárias imediatamente para tais linguagens e máquinas virtuais. Apresentamos resultados acadêmicos e comerciais recentes no desenvolvimento de linguagens de blockchain e máquinas virtuais que vêm diretamente equipadas com ferramentas de análise e verificação formal. A ideia principal é gerar tudo isso automaticamente, correto por construção a partir de uma especificação formal. Demonstramos a viabilidade da abordagem proposta aplicando-a a duas blockchains, Ethereum e Cardano.