I've been building a TLA style Temporal Logic library for Verus (using LLMs). My experience so far is that LLMs are surprisingly useful at generating the mechan

I've been building a TLA style Temporal Logic library for Verus (using LLMs). My experience so far is that LLMs are surprisingly useful at generating the mechanical proof scaffolding (when they're not occasionally trying to cheat with `assume(false)` statements), but they are not a substitute for knowing what property you actually want.