[mratsim]

Yes I'm in the middle of many Microsoft papers[1] to add model checking to Nim, in particular CHESS.[2]

[1]: https://github.com/mratsim/weave/issues/18

[2]: Finding and Reproducing Heisenbugs in Concurrent Programs, http://www.cs.ucr.edu/~neamtiu/pubs/osdi08musuvathi.pdf