本文介绍了Certora团队开发的一款用于验证编译器优化的等价性检查工具，该工具通过比较优化前后程序的行为来检测编译器bug。文章还分享了该工具在Vyper编译器中发现的一个优化bug，该bug导致局部变量被错误地映射到相同的堆栈位置，从而改变了程序的行为。该bug已在Vyper 0.4.2版本中修复。
Certora