PyPy has formally verified the integer abstract domain using Z3, a quite important part of our jit optimizer (will write about that in the coming weeks). We al

PyPy has formally verified the integer abstract domain using Z3, a quite important part of our jit optimizer (will write about that in the coming weeks). We also run a fuzzer regularly to find optimization bugs, using Z3 as a correctness check: https://pypy.org/posts/2022/12/jit-bug-finding-smt-fuzzing.html https://pypy.org/posts/2022/12/jit-bug-finding-smt-fuzzing.h... The peephole optimizations aren't themselves formally verified completely yet. We've verified the very simplest rules, and some of the newer complicated ones, but not systematically all of them. I plan to work on fully and automatically verifying all integer optimizations in the next year or so. But we'll see, I'll need to find students and/or money.