Jeg er med i et pågående prosjekt på universitetet der vi bruker Rocq, en interaktiv teorembeviser, til å mekanisk verifisere korrektheten til Temporal forslaget til ECMAScript, også kjent som JavaScript. Under mekaniseringen har vi funnet flere inkonsistenser i spesifikasjonen til forslaget, som vi har fått rettet opp i.