Yes, any analysis after an incident has the benefit, and bias, of hindsight.

But I see this post less as an incident analysis and more as an experiment in learning from hindsight. The goal, it seems, isn’t to replay what happened, but to show how formal methods let us model a complex system at a conceptual level, without access to every internal detail, and still reason about where races or inconsistencies could emerge.

As I read it, it felt more like an exploration from state space stand point (and not an example of model checking) which to me sounded quite reasonable. Unusual and intuitive I'd say.

The author does start talking about model checking in the third paragraph and go on using "SPIN", so there's a significant part that is interested in model checking, anyway.

I can see where the parent is coming from.

I think you can both be right - it can be valuable in any case.

Thanks for sharing. Is the code still running on Python 2.x or planning on transitioning to Python 3?

It is just that I have a job and a family to support. So I want to create something in whatever time I have. The prospect of engaging myself in myriad of courses sounds dull.

Maybe it's a folly but I am just intrigued by how they work and want to be able to develop them without committing to taking lot of courses.

maybe you could look into LLVM's Kaleidoscope tutorial..

Does it require any background in CS?

You can probably pick the CS and math up as you go. I haven’t gone through that resource but it looks interesting and useful.