I have dabbled with Verus in rust. I found that if you leave the agent to its own devices it will produce a spec that just restates the existing implementation. It took a lot of work to arrive at specs that were plausibly accurate and complete statements of what the code was supposed to do.

But once you got there, Claude had no trouble proving the code satisfied the spec, and I uncovered a few interesting bugs this way.