I've just taken a quick glance at this, and will explore further -- but at first, it seems like it's really a good application of ad-hoc proofs to assembly code; which is a subset of what I'm interested in, but for me the more interesting thing about the paper was the structured safety proofs for things like memory safety, no read-before-write, no overflow, etc., and thinking about how this can be expanded and generalized. While for something like a bignum library (or a heap) the actual conformance to the behavioral contract will be somewhat ad-hoc, having a lot of safety contracts also proved along the way "for free" (or at slightly reduced cost, anyway) is what really draws my attention. I can see spending 2x the time writing the code, and 10x the time proving things about it, in exchange for not having to spend the 100x (DAL B) or 1000x (DAL A) time testing it.