La verificación formal es una labor de ingeniería exigente y las propias herramientas que la realizan también son difíciles de depurar, por lo que deben probarse de forma rigurosa. Alive2 es una herramienta de validación de traducciones para LLVM IR que compara dos versiones de una función —normalmente antes y después de una optimización— y trata de demostrar si la transformación es correcta. Más de 600 incidencias de LLVM enlazan con la instancia en línea de Alive2, lo que refleja su uso cotidiano por parte de ingenieros de compiladores.
Los defectos de Alive2 se dividen en dos grandes familias: las falsas alarmas, relativamente fáciles de detectar lanzando muchas optimizaciones y revisando los errores señalados, y las alarmas omitidas, mucho más complejas de localizar porque requieren pares de funciones en LLVM IR con la misma signatura pero comportamiento divergente demostrable para alguna entrada. Para encontrar estas últimas, los autores exploraron dos vías. La primera combina YARPGen, un generador aleatorio de programas sin comportamiento indefinido, con una mutación controlada que produce una segunda función también libre de comportamiento indefinido; tras compilar y ejecutar ambas para descartar pares con resultados idénticos, Alive2 debe forzosamente señalar el error, así que si no lo hace se ha descubierto un fallo.
La segunda vía es indirecta: el superoptimizador Minotaur invoca Alive2 constantemente al buscar versiones más baratas de instrucciones LLVM, lo que somete a Alive2 a una batería intensiva de consultas. Si Minotaur produce un candidato que Alive2 acepta como refinamiento correcto sin serlo, y ese código se compila y ejecuta dentro de programas reales con suites de pruebas, una mala compilación quedará al descubierto. Hasta ahora, los autores no han encontrado demasiadas alarmas omitidas, lo que sugiere que Alive2 y el solver Z3 cumplen razonablemente su objetivo. Los autores apuntan, no obstante, a atributos de función y construcciones similares como terreno aún poco explorado donde podrían esconderse errores futuros.