Very cool project with a great name!

If you haven't looked at it already, you may be interested in Arthur Charguéraud's work on program verification using characteristic formulas (http://www.chargueraud.org/softs/cfml). CFML is a similar tool for ocaml verification using Coq.