I am part of an ongoing project at the university where we use Rocq, an interactive theorem prover, to mechanically verify the correctness of the Temporal proposal of ECMAScript, also known as JavaScript. During the mechanization we have found several inconsistencies in the specification of the proposal, that we have now had corrected.