Model checking is great! I, too wrote a simple C# model checker to test some tricky serialization code inside Microsoft. It's now open source: https://github.co

Model checking is great! I, too wrote a simple C# model checker to test some tricky serialization code inside Microsoft. It's now open source: https://github.com/ahelwer/FiniteModelChecker https://github.com/ahelwer/FiniteModelChecker It requires a fair amount of boilerplate (see the examples in the tests directory) but it is so, so much more powerful than manually coding a bunch of unit test cases that it was worth it (and it unearthed a tricky bug!) I think a great project would be to write a spec in TLA+, run its model checker in simulation mode, then use the generated event traces to execute corresponding event traces in this (or some other) model checker, all the while translating the program's state back into values understood by TLA+ for checking against the TLA+ spec's invariants. Would be a nice lightweight method of enforcing correspondence between spec and code.