Erlang / Elixir formal verification

[michallepicki]

I just listened to a new ElixirTalk podcast episode where @josevalim mentioned formal verification (I linked to that exact part). This topic sounds very interesting to me, and I wonder:

Have anyone used formal verification methods for Erlang / Elixir systems? Which ones? Which tools did you use?

What is your experience with formal methods in general?

To describe the topic better I’ll throw in some random links:

• Formal methods on WIkipedia
• Model Checking and a List of model checking tools on Wikipedia
• What is Coq?
• TLA+ Video Course (temporal logic) by Leslie Lamport (his wiki page)
• Concuerror for Erlang
• McErlang
• Petri net on Wikipedia

[josevalim]

I believe I talked about μ-calculus too. One tool is mcrl2 with an accompanying Coursera course. There are also some papers that translate some of Erlang semantics to mcrl2.