When publishing algorithms for others' consumption either for a paper or blog, please post the source code.<p>This post is a follow up of <a href="https://ahelwer.ca/post/2023-03-30-pseudocode/" rel="nofollow">https://ahelwer.ca/post/2023-03-30-pseudocode/</a><p>Where Andrew pointed compared executable Python code vs executable model checker PlusCal.<p>In this blog, I'm showing how to model check Python code with minor changes.<p>For the curious, model checking is the formal methods technique that explores every possible path to ensure the invariants are met in every case.