To put my oar in, and this is purely based on what I've read about spin, spin can verify 100% for 'small' models. If larger models are checked, it will run out of memory so you put it in a probabilistic mode which gives probabilistic assurances, still 'good' but less than 100%. In that respect I suppose it's degenerated to rather posh fuzzing.

I think the difference between small and large is down to how long you're prepared to let it run, but even more fundamentally, how much memory you can give it.

I'd agree that if the model matches the code and you successfully check the entire state space then it's a proof.