The goal of this project is to formally prove a lower bound on the time it takes to beat the game Dragster.

So far, I have implemented a specification of the Atari 2600 console, and used it to state the theorem. Now I just have to prove it!

Of course, that's easier said than done.


  • coq 8.13.2
  • coq-record-update 0.3.0
  • coq-mathcomp-ssreflect 1.14.0
  • coq-mathcomp-algebra 1.14.0