Demanding an absolute proof of correctness about a program is a noble but pointless exercise.

All you can prove is that a program adheres to a specification. Now what you have achieved is a shift of responsibility from the program to the spec.

And who’s going to prove your spec correct? The more you streamline and automate this process, the more your spec becomes your program. You just invented a DSL, nice job.

This is not to say that formal proofs or reasoning about correctness are entirely worthless. Just that we should not expect them to do more than they are capable of.