In order to ensure idiomatic quint specs can be verified in Apalache effectively, we need to be able to rewrite idiomatic quintified-TLA into correct and performant TLA (as the ApalacheIR). However, the current state of our internal rewriting libraries is too burdened by tech debt to make this feasible.

Thankfully, a design that will enable us to program these rewrites with greater velocity and correctness has been developed by @Kukovec in #2447 . This will have many side benefits to the maintainability and extensibility of Apalache, but the critical need driving this work is the support for idiomatic quint.