Today I ran a model checker (cbmc) on a sudoko solver to prove memory safety. Certainly a toy problem. But now I know my sudoko solver is verified to be written in memory safe C. Who knew this can be so simply? (I do not expect it to be that simple for real programs, but the underlying technology for sure is mature enough).