I wrote a finite model checker in C#, which I used to exhaustively check reads/writes against some complicated serialization code (serializing a bunch of differ

I wrote a finite model checker in C#, which I used to exhaustively check reads/writes against some complicated serialization code (serializing a bunch of different types into the blob, updating existing objects, ensuring values of all objects were as expected). Used during some tricky memory footprint reduction stuff inside Microsoft, I'll see whether I can open source it. Other than that, integrating TLA+ with your dev workflow is very straightforward if you're dealing with concurrency or distributed systems. In other domains its value is less obvious. You might also take a look at the P language, which will model-check your code if you add the right hooks.