Where do I start? What do I do?

So you have to start defining what your system is or what your solution is in some formal language, right, if you're going to use formal methods.

And then in order to understand things, you start running or model checking your specification, right? So first of all, if you just have your model, you can get some random execution of your model.

That's the best thing you can get, and that can give you some insight, right? You see some random behavior of your model.

Start in this initial state and you go here, go there.

And then you are going to look at that and say, "Hmm, I don't like this.

I actually don't think I can go from this state to that state.

What's the relationship between the model and my code base?