Full verification is extremely expensive, not just to create the proofs, but also to maintain them as the software evolves. Telling C programmers to go directly

Full verification is extremely expensive, not just to create the proofs, but also to maintain them as the software evolves. Telling C programmers to go directly to full verification is, indeed, making the perfect the enemy of the good. And you are missing an important point here. Once you have a reasonably sound and rich type system, you can leverage the type system in library API design to eliminate classes of higher-level bugs. For example, Rust crypto libraries can leverage Rust's affine type system to ensure you don't use a nonce more than once. The Apache Struts vulnerability was about failing to distinguish trusted vs untrusted input; that distinction can be expressed and checked in type systems.