atari-proofs

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.

Dependencies

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