Comment by stefan_

Have you tried it for Rust, arguably a much lower bar than actually fully formally verifiable? Sorry to say but AI can't figure out the borrow checker. I'd speculate it does poor on a lot of things that are sort of implicit in the code / properties of the grand structure rather than incremental text things.