I've been fascinated with recent advances in compiler optimization. The article mentioned superoptimization. Google's Souper uses an SMT solver (like Z3) to ma

I've been fascinated with recent advances in compiler optimization. The article mentioned superoptimization. Google's Souper uses an SMT solver (like Z3) to make LLVM peephole optimizations. https://github.com/google/souper https://github.com/google/souper Alternatively, Alive allows users to specify rewrite rules for peephole optimizations. The rules are verified with Z3 and then compiled into an LLVM pass. If the rewrite can't be verified, then Alive won't allow it. https://github.com/nunoplopes/alive https://github.com/nunoplopes/alive And then there's STOKE, which uses stochastic search to investigate possible program transformations of x86 to find non-obvious code sequences. STOKE also verifies the resulting transformation with Z3. https://github.com/StanfordPL/stoke https://github.com/StanfordPL/stoke