Hunting for Missed Alarm Bugs in Formal Verification Tool Alive2

Looking for Missed Alarm Bugs in a Formal Verification Tool

Formal verification tools like Alive2, used to validate LLVM optimizations, are themselves prone to bugs. While false alarms are easy to catch, missed alarms—where Alive2 fails to flag an incorrect optimization—are harder to detect. The authors describe two methods: a modified YARPGen that generates pairs of similar, undefined-behavior-free functions, and using the Minotaur superoptimizer, which passively tests Alive2 with many candidates. Despite extensive testing, few missed alarms were found, suggesting Alive2 is reliable, though areas like function attributes remain unexplored.