Perhaps I am misreading the CEK spec, but I believe there are two small mistakes in the stepping rules.

Compute rule for constr

This rule creates a constr frame:

But the frame is missing its second argument (an empty stack of values).

Return rule for case

This rule selects the right branch to evaluate a case:

But the resulting application frames seem to be in the wrong order: suppose the constructor has two arguments $V_1$ and $V_2$, and branch $M_{i+1}$ is already a lambda, e.g. $\lambda x. (\lambda y. N)$. Then stepping the application frames would result in the substitution $x \mapsto V_2, y \mapsto V_1$.

The Haskell and Agda implementation maintain a reversed list of evaluated constructor arguments (stack), whereas the TeX spec just appends them at the end of a normal list (maintaining the original application order). The Haskell/Agda implementations then basically reverse that list again, which the spec shouldn't have to do.