Los contratos inteligentes son los componentes de software clave para realizar aplicaciones blockchain, desde una sola moneda digital encriptada hasta varios campos. Debido a la naturaleza inmutable de la cadena de bloques, cualquier error o fallo se volverá permanente una vez publicado y podría provocar enormes pérdidas económicas. Recientemente, se han expuesto una gran cantidad de problemas de seguridad en los contratos inteligentes. Es importante verificar la corrección de los contratos inteligentes antes de que se desplieguen en la cadena de bloques. Este documento tiene como objetivo verificar la corrección de los contratos inteligentes en transacciones de Ethereum, y se adopta el verificador de modelos Spin para la verificación formal de los contratos inteligentes con el fin de garantizar su ejecución con respecto a la voluntad de las partes, así como su interacción fiable con los clientes. En esta dirección, proponemos un método formal para construir los modelos de contratos inteligentes. Luego, el método se aplica a un caso de estudio en el mercado de materias primas de Ethereum. Finalmente, se implementa un modelo de caso en Spin, que puede simular la ejecución del proceso y verificar las propiedades que se abstraen de los requisitos. En comparación con las técnicas existentes, el análisis formal puede verificar si los contratos inteligentes cumplen con las especificaciones de los comportamientos dados y fortalecer la credibilidad de los contratos inteligentes en la transacción.