I suspect the "verify" part of that is going to slam head-first into the Halting Problem, given that some of the quadratic behavior only happens (see the blog)

I suspect the "verify" part of that is going to slam head-first into the Halting Problem, given that some of the quadratic behavior only happens (see the blog) for particular patterns of use or input data. You'd also likely want to somehow encode space complexity as well, otherwise silly things like "precompute every possible result and put it in a giant lookup table" will register as "O(1)".