Comment by ahelwer

That's very neat! I will look at Truffle. The TLA+ interpreter is definitely "weird" in that it does this double duty of both evaluating a predicate while also using that same predicate to extract hints about possible next states. I wonder how well this highly unusual side-effectful pattern can be captured in Truffle.

Edit: okay the more I look into GraalVM the more impressed I am. I will have to sit down and really go through their docs. Oracle was actually cooking here.