I have a skill for using Verus with Rust [1]. I think they found a nice way to integrate proofs with the language. The verify skill I use lists proofs as a possible technique [2] and the project instructions have instructions on using it, but only a very small fraction of the code base I am using this on has proofs. Anyone can now have an LLM write proofs but its still difficult to know when they are more productive than other techniques and to relay that advice to an LLM.
[1] https://github.com/gregwebs/skills-sdlc/blob/main/skills/rus... [2] https://github.com/gregwebs/skills-sdlc/blob/main/skills/ver...