[maradydd]

Thanks! Those are all excellent papers. I am actually looking into formally verifying Hammer using Frama-C, but haven't gotten too far yet.

[nickpsecurity]

Smart move. It's a good default far as work vs results tradeoff. I'll try to keep your project in mind when I review my collection of verification papers in case I see any little-known, C verification methods that might help.