El artículo repasa los argumentos del clásico paper de 1979 'Social Processes and Proofs of Theorems and Programs', que sostenía que la verificación formal de programas estaba abocada al fracaso, y los contrasta con la situación actual. En 1979, los autores defendían que las demostraciones matemáticas son procesos sociales, que las especificaciones formales pierden información al traducir requisitos informales, que la verificación totalmente automática es inalcanzable y que, aunque lo fuera, resultaría contraproducente al impedir la comprensión del programa y reducir los incentivos a otras capas de defensa. También argumentaban que los sistemas reales son demasiado desordenados para ser especificados y que la fiabilidad del software va mucho más allá de la verificación.
Cincuenta años después, el texto señala que la verificación formal vive un renovado interés impulsado por la programación asistida por IA. Herramientas como Lean, lenguajes como Quint y proyectos como Signal Shot muestran que la disciplina avanza hacia el uso mainstream. Los argumentos de 1979 se matizan: las especificaciones, aunque informales, están más cerca de los requisitos que las implementaciones; la intervención humana sigue siendo esencial para fijar el significado de 'correcto'; y los LLM están reduciendo la distancia hacia verificadores más automáticos. El artículo concluye que la verificación formal no sustituirá otras prácticas de fiabilidad, pero se ha vuelto más relevante por el aumento de las apuestas en infraestructura crítica y por la necesidad de especificar con precisión lo que se quiere cuando se trabaja con agentes de código.