TLA+ With Elixir

Has anyone working with Elixir used TLA+ to model their code? It seems as if it’d be a very natural fit and I am curious if anyone has any feedback on that combination.


I did quite a lot in JavaScript based on →
But never had the desire to try within Elixir.

So I’m also curious if anyone does?

I guess there are two of us interested in the topic. I’ve been tweeting with @QuinnWilton on the subject.

I haven’t yet but Hillel Wayne’s Twitter feed is full of bits and bobs about formal verification, as is his blog. I’m frequently tempted, and if I ever contribute to serious distributed-systems work again I will probably dabble a little. IIRC Quinn used Alloy recently rather than TLA, though?

There’s also Quickstrom as a very recent release that is frontend-focused but quite interesting.

1 Like

Ah–thanks for the pointer Shane!

I am not, but this an area that I am interested in! Just haven’t had enough time to dig into it yet.


I’m in the same boat, definitely a field I’m interested in but never had the use-case where I thought: now I’m gonna dig in!


I am interested in this subject.
have anyone try this library tla-transmutation before?