I'm sure there are edge cases for stuff I haven't tested, but I've written many lines of TLA+ with the generated bindings and it seems to work fine as far as I

I'm sure there are edge cases for stuff I haven't tested, but I've written many lines of TLA+ with the generated bindings and it seems to work fine as far as I can tell. The model-checker appears to work as expected. Granted, I suspect part of it is that they are cribbing pretty heavily from the official VSCode TLA+ bindings, so it probably gets a lot for free.