I think it's a really illustrative example of how to play to AI's strengths. No human would dream of writing 600,000 lines of Rocq to verify one binary. The whole approach is so insane that it probably wouldn't even occur to them. But Claude has no concept of tedium, and will happily fill out lemmas all day long until the job is done. To me that's what's significant about this result: it's not about scaling up an existing technique, it's about using scale itself as the basis of a new technique.

I believe that they chose assembly in order to diff against real projects and then see if those real projects have bugs.