En el artículo «50 years of proof assistants», Lawrence C. Paulson refuta el estancamiento científico mediante la evolución de la verificación formal. Desde 1975, con Edinburgh LCF y el lenguaje ML, se crearon los cimientos de los asistentes de demostración. Entre 1985 y 1995, herramientas como Isabelle y HOL permitieron las primeras verificaciones de hardware y consolidaron la lógica computacional.

Entre 1995 y 2015, la tecnología maduró tras fallos como el del Pentium. Se lograron hitos como la verificación del Teorema de los Cuatro Colores y el procesador ARM6. Posteriormente, se verificó software crítico como el kernel seL4 y el compilador CompCert, demostrando por primera vez que la corrección funcional total de sistemas complejos y el código libre de errores eran objetivos alcanzables.

Desde 2015, la adopción se disparó en matemáticas (con Lean) y en la industria. Gigantes como AWS y proyectos como CHERI integran ahora la verificación formal para garantizar la seguridad del hardware y la nube. El autor concluye que esta tecnología está pasando de ser una curiosidad académica a un estándar industrial «ordinario», demostrando un progreso científico vibrante y continuo.