The PyPy project has recently merged a new DSL (Domain-Specific Language) for peephole transformation rules, designed to optimize runtime values. The DSL uses rply for parsing and Z3 for checking rule correctness. The implementation is relatively ad-hoc, with a small type checker and pattern matching RPython code generated using an approach inspired by Luc Maranget's paper.

The current status of the DSL has it being used in PyPy's main branch, with some integer rewrites already ported over from imperative style. However, there are still missing features and potential extensions planned for future development. These include support for overflow-checking variants and correctness proofs for operations like division.

Source: https://pypy.org/posts/2024/10/jit-peephole-dsl.html