I have something to contribute to the implementation question. I have done some experimentation with code generation from TLA+ to Elixir for my bachelor thesis years ago [1], and there were two main challenges in getting the code to be useful (as a basis for some actual implementation):
1. Non-determinism and how to take inputs for it
2. How to split the naturally global state and transitions of the TLA+ spec into local processes
For (1), I defined an oracle interface which can be used to gather inputs for all non-determinism present in the spec (and therefore the code). I wrote a prototype [2] for a real pump-station controller that used MQTT for gathering sensor data and forwarding it to the oracle to drive the state machine.
For (2), I meant to have some sort of configuration that allowed users to define how the state would be divided, but this was kinda rushed and I'm sure we could have a more elegant interface - see an example in [3].
In my masters, I continued this work and included unit test generation from the spec, which is a much more trivial problem than MBT since I can generate the test harness to fit exactly the structure of the code I also generated. My master thesis [4] is in English and it covers a bit of the initial work too, in case you want to learn more, and I also wrote a paper [5].
Great job on TLX btw! I don't mean to hijack the conversation fully into code generation as that can spark lot's of debate, I just wanted to share something I tried in the past that was also in the TLA+ and Elixir combination!
[1]:
https://github.com/bugarela/tla-transmutation[2]:
https://github.com/bugarela/pump-station[3]:
https://github.com/bugarela/tla-transmutation/blob/master/tla_specifications/ewd840/config.json[4]:
https://github.com/bugarela/masters-dissertation[5]:
https://dl.acm.org/doi/10.1145/3559744.3559747