Dungeons & Dragons rules are a spec spanning thousands of pages, not formalized, but thoroughly tested by the community. Moving them to a formal specification language (Quint) was an obvious next step. It worked and proved to also be a great LLM self-checker.

Fantastic, I'd been daydreaming about doing similar for a while!

Do I understand correctly that the Quint code is not needed 'at runtime', that it's there for model-based testing of the XState implementation?