<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">So far I've been reading <a href="https://www.cs.purdue.edu/homes/bendy/Fiat/FiatByteString.pdf">https://www.cs.purdue.edu/homes/bendy/Fiat/FiatByteString.pdf</a>. I'm interested in the ideas presented in <a href="https://github.com/DistributedComponents/verdi-runtime">https://github.com/DistributedComponents/verdi-runtime</a>, which is OCaml based.</div><div dir="ltr"><br></div><div>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.</div><div><br></div><div>Any pointers to research or prior art would be greatly appreciated.</div><div><br></div><div>Cheers,</div><div>Tim Watson </div><div><br></div></div></div></div>