I'm curious what the verification and proof stages offer beyond automated PR checks. The verification example looks rather standard.

To me, the biggest bottleneck is the fact that automated checks don't catch everything. I still need to read through the code myself before I trust it.

e.g. understanding the code probably takes 30-200% of the effort of writing it!

It does seem to do something though about the situation where, occasionally, an AI just goes and vandalizes 3000 lines of code across your whole code base.