Comment by mmalone

The docs are sparse... but it looks like the answer is that it depends on what you mean by "correct." It doesn't look like it's a general purpose theorem prover, but it does appear to be model/spec-driven and the linked article says that the system can prove safety and liveness. I'm guessing they mean "type safety" but they may be using the term in the broader distributed system sense. In any case, it does look like it gives you certain "proofs for free" if your definition of correct is "eventually converges on a consistent state." I don't think you can prove arbitrary properties like you can with Coq or with a dependent type system. Still, very cool.