El desarrollo de contratos inteligentes sigue en sus etapas iniciales, con diferencias significativas en los lenguajes de programación subyacentes y las plataformas de aplicación que resultan en una falta de estandarización. Esta falta de estandarización aumenta la susceptibilidad a vulnerabilidades y pérdidas financieras asociadas. Para abordar las vulnerabilidades de seguridad en contratos inteligentes en la plataforma de blockchain Ethereum, este documento propone un método de auditoría de seguridad basado en verificación formal. El método integra un módulo de entrada, un módulo de análisis estático, un módulo de verificación formal, un módulo de ejecución análoga y un módulo de informe y recomendación, que pueden descubrir con precisión las vulnerabilidades de seguridad y fallos lógicos de los contratos inteligentes a través de la verificación formal y otras técnicas de análisis, logrando así la detección de corrección. Durante el experimento, el método detecta 8 tipos de vulnerabilidades comunes en 148 contratos inteligentes y marca 21 contratos inteligentes con vulnerabilidades. Después de una revisión y análisis manuales, se descubre que 17 de estos 21 contratos inteligentes marcados sí tienen vulnerabilidades de seguridad. Los resultados experimentales muestran que el método propuesto puede detectar con precisión las vulnerabilidades de seguridad y fallos lógicos en contratos inteligentes a través de la verificación formal y otras técnicas de análisis antes de que los contratos inteligentes se desplieguen, mejorando significativamente la seguridad de los contratos inteligentes y reduciendo las pérdidas económicas que puedan ser causadas por defectos de código.