[arpinum]

I found Quint to be a good pairing with LLM. Easier syntax to learn so you are actually collaborating instead of relying on hope.

[oa335]

What are the downsides as compared to TLA+?

[mavelikara]

Everything that can be expressed in TLA+ can’t be expressed in Quint. But everything useful for specifying programs, I believe, can be expressed in both languages.

[esafak]

What are you doing with it? Any write up?

[mavelikara]

Not the person you asked, but here are some real world examples: https://www.linkedin.com/posts/quint-co_community-spotlight-...

(One of the entries cited is something I worked on).

[arpinum]

data pipelines and data repair.