This was a lot more exciting than I expected.

The homepage does not do a very good job of explaining what we're looking at:

It appears to be a combination of two things:

1) A formalization of the Python language

2) An LLM which hooks into running programs and hot-swaps code with verifiably-equivalent behavior but better runtime performance, found via superoptimization and then verified via the formalization rules

This is brilliant, and in hindsight one of those "I can't believe nobody had thought of this yet" sort of things.