# Looking for Missed Alarm Bugs in a Formal Verification Tool

DevFeed: [Looking for Missed Alarm Bugs in a Formal Verification Tool](<https://devfeed.tech/articles/looking-for-missed-alarm-bugs-in-a-formal-verification-tool-39746.md>)

Original publisher: [Read original article](<https://blog.regehr.org/archives/2124>)

Author: regehr

Published: 2024-09-04T18:29:03Z

Content type: article

Language: en

Sources: [Embedded in Academia](<https://devfeed.tech/sources/embedded-in-academia.md>)

Topics: [Formal verification](<https://devfeed.tech/topics/formal-verification.md>), [LLVM](<https://devfeed.tech/topics/llvm.md>), [Compiler](<https://devfeed.tech/topics/compiler.md>), [Testing](<https://devfeed.tech/topics/testing.md>), [C](<https://devfeed.tech/topics/c.md>), [C++](<https://devfeed.tech/topics/c-plus-plus.md>), [undefined\_behavior](<https://devfeed.tech/topics/undefined-behavior.md>)

Tags: [bugs](<https://devfeed.tech/tags/bugs.md>), [c](<https://devfeed.tech/tags/c.md>), [c-plus-plus](<https://devfeed.tech/tags/c-plus-plus.md>), [compiler](<https://devfeed.tech/tags/compiler.md>), [formal-verification](<https://devfeed.tech/tags/formal-verification.md>), [llvm](<https://devfeed.tech/tags/llvm.md>), [testing](<https://devfeed.tech/tags/testing.md>), [uncategorized](<https://devfeed.tech/tags/uncategorized.md>), [undefined-behavior](<https://devfeed.tech/tags/undefined-behavior.md>), [verification](<https://devfeed.tech/tags/verification.md>)

## AI overview

This co-authored article explains how formal verification tools themselves require rigorous engineering and testing. It describes testing Alive2, a translation validation tool for LLVM optimizations, including the challenge of finding missed-alarm bugs and the use of randomized program generation with YARPGen.

## Source excerpt

[This piece is co-authored with Vsevolod Livinskii.] Formal verification isn't some sort of magic pixie dust that we sprinkle over a computer system to make it better. Real formal verification involves a lot of the same kind of difficult, nasty, grungy engineering work that any other systems-level job involves. Furthermore, the verification tools themselves are [...]