The other approach, which has been quite successful, by the penn team, is using hs-to-coq to extract coq from haskell and _then_ verify: https://github.com/antalsz/hs-to-coq -g On Sat, Dec 8, 2018 at 7:05 AM Tim Watson wrote:

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

-- You received this message because you are subscribed to the Google Groups "cloud-haskell-developers" group. To unsubscribe from this group and stop receiving emails from it, send an email to cloud-haskell-developers+unsubscribe@googlegroups.com. To post to this group, send email to cloud-haskell-developers@googlegroups.com. Visit this group at https://groups.google.com/group/cloud-haskell-developers. For more options, visit https://groups.google.com/d/optout.