Elixir with static typing would be an absolute dream. I know there's https://gleam.run/
https://elixir-lang.org/blog/2023/06/22/type-system-updates-...
Formal attempts have repeatedly failed, even when they exclude message passing, which is the most difficult (and most useful) aspect. If Wadler cannot do it, I'm sure I (or you) cannot.
A typesafe concurrent language is possible, but only a new language layer on top of E/E and the BEAM.
There is the set theoretic types work [1] lead by Jose and a couple of PhDs and also eqwalizer by WhatsApp [2]
[1] https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi... [2] https://github.com/WhatsApp/eqwalizer