> model checking doesn't fare well with data structures, algorithms, and cryptography

To the contrary, that's what I'm using it for in most of my projects. It found interesting algorithmic bugs in my ctl find function (3-way comparison callback missing cases), is used to crack poor hashes. Also my tiny-regex matcher profited from it.

Also a lot of baremetal firmware.