Nice. I am going to write a blog post about async/await highlighting some features and asking for feedback from the public. It will be similar to this one: https://groovy.apache.org/blog/loop-invariants The loop invariant blog is currently draft (so not publicly advertised or in the index). I will likely do some minor polish and then publish. I will do async/await next (probably tomorrow) and will also make it draft and give you a chance to read before publishing.

It might be a bit confusing that you say it is

res

in dafny but

result

in Groovy, but then use

res

in the Groovy invariant part.

hmm, true ... I can tweak that