When publishing algorithms for others' consumption either for a paper or blog, please post the source code.

This post is a follow up of https://ahelwer.ca/post/2023-03-30-pseudocode/

Where Andrew pointed compared executable Python code vs executable model checker PlusCal.

In this blog, I'm showing how to model check Python code with minor changes.

For the curious, model checking is the formal methods technique that explores every possible path to ensure the invariants are met in every case.