I am new to TLA+ and got a bit handy with LLMs so I wrote this script (if it is of any use for someone) https://github.com/kerberosmansour/TLA_AutoRepair
- TLA+ has a steep learning curve so it's handy to have something that can help generate and fix some of the problems (with or without human intervention).
- I found TLA+ might make a useful sandbox for enforcement learning, in combination with LLMs this *might add value down the line(?) This is more a hypothesis really.
As always, constructive feedback, bug reports, feature requests or code contributions are always welcome.