Ok, nice. Quint caught a design bug. Not a huge one, but at least the agent was able to use it to change its design.

The general thesis, I think is right. You can use formal methods as guardrails for agents to steer a design, in part, by themselves.