That sounds pretty awesome. So, are these only instruction-level optimizations or is there a good toolkit for doing it SSA level as well? My idea being combining it with formal, equivalence checks in certified compilers so we get optimizations plus ensure correctness given original version was correct via certified transform. Certified to v1 -> superoptimize to v2 -> certified checker (v1, v2) -> rinse repeat.