You can prove all sorts of properties about a program. Sometimes the compiler produces bad code, but that is really not the fault of the formal verification, bu

You can prove all sorts of properties about a program. Sometimes the compiler produces bad code, but that is really not the fault of the formal verification, but a compiler bug. Try writing some moderately complex progra. in C, then a formally verified version in SPARK and fuzz them. That is usually quite confidence-inspiring :)