I am not aware of a credible alternative to operational or axiomatic semantics. (There is denotational semantics of course but that's not what we are discussing here.)
One of the fundamental goals of a specification is to allow users to reason about their programs. There must be a way of proving a bunch of theorems and then concluding that all valid compilations of a program will do the right thing. A spec that does not achieve this goal is not worth calling a spec. Both axiomatic and operational semantics have extensive lines of work demonstrating their ability to achieve this.
Listing allowed optimizations has not been demonstrated to achieve that goal. I am not aware of a single work that would even properly formalize such a specification, let alone for any non-trivial language, let alone provide the tools needed to perform rigorous reasoning about programs written in such a language.
Even a C-style axiomatic spec is better, by orders of magnitude, than having to reason about the combinatorial explosion of a set of optimizations being applied in any order.
rather than try to reverse engineer operational semantics that justify X.
This "reverse engineering" provides deep insights into what the suggested transformations entail and how they interact with other transformations. This is not some grunt work we do to handle some deficiency of operational semantics; it is part of understanding whether that transformation makes any sense and whether programmers can be reasonably expected to be able to deal with it. Any optimization that does not have such a justification should be treated with suspicion; it may cause surprising actions at a distance (such as accidentally introducing pointer provenance as a concept programmers have to care about without people even realizing that that is what they were doing).