Very nice discussion there. It surprises me that a non-trivial piece of code written in C can be verified.

It might be of interest that BitC http://www.bitc-lang.org/ is being developed as a flexible system programming language that supports verification.

  It seeks to combine the flexibility, safety, and richness
  of Standard ML or Haskell with the low-level expressiveness of C....

  ...it is possible to write a MPEG decoder or SHA-1 hash algorithm
  in BitC that is fully safe, but performs competatively with the
  C implementation. Today, that can't be done in SML, O'Caml, or Haskell.