[Haskell-cafe] Proof of a multi-threaded application

Hello, I am very new to Haskell, this is my first day, and I wanted to know if it is possible to prove correctness of a multi-threaded application written in Haskell. Basically, I want to check that a multi-threaded implementation of an algorithm that detects cycles in a dynamically changing graph, actually detects the cycles. Also, the algorithm prevents previously detected cycles from happening by not allowing certain edges to be added. And I want to check that this property also holds. Thank you and I hope you can help me, Silviu ANDRICA.