There's a lot of claim and so little technical details on that page.

How was the formalization of Python accomplished? What formal proof framework do you use?

How do you reproduce the optimizations across several instances / runs of the program? (since the source code doesn't change... assuming you don't redo the same work over and over?)

What visibility, tracking and logging is there into the actual code running? Debugging is an extremely important part of building software, especially if there's a demon switching out binary code constantly underneath. Even if the recompiler is perfect (it won't be), user code never is.

Why is the superoptimization and visibility into the data not surfaced back to the level of the source code? This seems like a waste.