So far I've been reading https://www.cs.purdue.edu/homes/bendy/Fiat/FiatByteString.pdf. I'm interested in the ideas presented in https://github.com/DistributedComponents/verdi-runtime, which is OCaml based. My goal is to provide building blocks for verifying and testing Cloud Haskell programs. I've been looking at existing frameworks (such as quickcheck-state-machine/-distributed and hedgehog) for model based testing, and ways of injecting an application layer scheduler for detecting race conditions. The final bit of the puzzle is being able to apply formal methods to verify concurrent/distributed algorithms, and generate some (if not all) of the required implementation code. Any pointers to research or prior art would be greatly appreciated. Cheers, Tim Watson