El interés en el aprendizaje automático y las redes neuronales ha aumentado significativamente en los últimos años. Sin embargo, sus aplicaciones son limitadas en dominios críticos para la seguridad debido a la falta de garantías formales sobre su fiabilidad y comportamiento. Este artículo muestra avances recientes en solucionadores de satisfacibilidad módulo teoría utilizados en el contexto de la verificación de redes neuronales con funciones de activación lineales por tramos y trascendentales. Se realiza un análisis experimental utilizando redes neuronales entrenadas en un conjunto de datos de mantenimiento predictivo del mundo real. Este estudio contribuye a la investigación sobre la mejora de la seguridad y fiabilidad de las redes neuronales a través de la verificación formal, permitiendo su implementación en dominios críticos para la seguridad.