When I wrote this, I had tried getting help from several different chat models. None of them produced anything remotely useful—but they did help me learn formal verification, as well as syntax when writing in PlusCal