> Does he mean doing what Galois did [1][2] with tools like CRYPTOL [3][4]? Or something more like this [5] with EasyCrypt and CompCert? Or something simpler like Altran's SPARK crypto [6]? And maybe with protocol-level verification like miTLS [7]?

Yes.

> I don't think there's a question about whether the goals can be met so much as a lack of uptake of methods and tools that meet them.

I agree. And, that's a big part of the reason I didn't spend a lot of time on formal verification when I wrote what I wrote. The target audience of my writing is people think that the result must be as fast as the fastest implementation, but that only think that formal verification of correctness is nice to have and/or impractical to the point of not being worth trying. That isn't my own personal prioritization, but I think that actually describes the prioritization of almost everybody deploying open source crypto software today.

Anyway, I hope to have more to say about formal verification of ECC implementations later.