Pretend model checking is an exciting new field born from frustrations with actually model checking large amounts of code that accepts somewhat arbitrary inputs and uses (large) loops. After enough neologisms like 'symbolic execution' and 'program synthesis' the distinctions between the various terms-of-art break down for laymen like myself and it all blurs together into some vague guarantee about software behavior.

In Aggelos Giantsios's (CUTER's) case, this means writing your own stuff. Everywhere else, this means writing a TLA+ specification for your favorite component of the term protocol, some implementation environment and "slapping on the TLAPS".

This has the unfortunate property of only model checking a model that the implementer THINKS the program behaves in (many 'model checking' efforts fit into this camp). Those who are truly serious about verification have a Maude<->ACL2 of the resulting assembly or try to check for symbolic constraints with KLEE.

Those who are even MORE serious (usually on philosophical grounds) have a host of approaches I couldn't even tell you about.