Prove with SPARK: No Math, Just Code How to prove key properties of Tetris and run it on ARM Cortex…