Downthread tptacek talks about how his company does verification of binary images. I assume there are limits to what is possible, but that's really the same as any verification approach.

I do agree that 'who is verifying' is a valid way of looking at it too.

Regardless, it's pretty clear that tptacek means formal verification.

Edit: see http://arieg.bitbucket.org/pdf/seahorn.pdf