В своем докладе я ссылался на проект Alive2, который позволяет с помощью SMT проверять эквивалентность LLVM IR. Для GCC есть похожий проект - smtgcc, который представляет собой расширение для верификации оптимизаций в GCC, по аналогии с LLVM IR используется внутренее представление компилятора - GIMPLE IR. В списке трофеев 26 проблем в GCC. На ежегодной конференции GNU Cauldron автор проекта Krister Walfridsson сделал доклад про smtgcc.

https://www.youtube.com/watch?v=vrkR7jKcFpw

Добавлено (07.10.2024): Слайды https://gcc.gnu.org/wiki/cauldron2024.