La tecnología blockchain ha atraído cada vez más atención de la academia y la industria recientemente. Ethereum, que utiliza la tecnología blockchain, es una plataforma de computación distribuida y un sistema operativo. Los contratos inteligentes son pequeños programas desplegados en la cadena de bloques de Ethereum para su ejecución. Los errores en los contratos inteligentes pueden provocar grandes pérdidas. La verificación formal puede proporcionar una garantía confiable para la seguridad de los contratos inteligentes de blockchain. En este documento, se aplica el método formal para inspeccionar los problemas de seguridad de los contratos inteligentes. Resumimos cinco tipos de problemas de seguridad en los contratos inteligentes y presentamos métodos de verificación formal para estos problemas, estableciendo así un marco de verificación formal que puede verificar eficazmente las vulnerabilidades de seguridad de los contratos inteligentes. Además, presentamos una verificación formal completa del contrato de Binance Coin (BNB). Se muestra cómo verificar formalmente los problemas de seguridad mencionados anteriormente basados en el marco de verificación formal en un contrato inteligente específico. Todas las pruebas se verifican formalmente utilizando el asistente de prueba Coq en el que se formalizan el modelo de contrato y la especificación. El trabajo formal de este documento tiene una variedad de aplicaciones esenciales, como la verificación de contratos inteligentes de blockchain, la verificación de programas y el establecimiento formal de fundamentos matemáticos y teóricos de la computación.