jasongross

What does "out of bounds" mean at the ISA level? By the time you have a binary, you've lost all the information about which memory is which.

But you're right that don't need ASan at all if you've encoded semantically meaningful properties. E.g., if you assert(decompress(compress(x)) == x), proving that you don't crash requires proving that compression round-trips. (Similarly if you have a reference implementation.)

The upshot is that the spec doesn't need to be written in a proof assistant and can instead be encoded as an end-to-end test.

Especially when "this one weird special case" pulls in the entire binary layout because your code has a hole that allows an attacker to jump to a specified address

You make a compelling argument, but, empirically, when you optimize code for performance, you end up with an unreadable mess that breaks all abstractions; but every time I've substantially optimized a proof for performance [of proof checking], I've ended up with better abstractions and more modularity.

The difference between math and software verification: in math, the convex hull hypothesis implies that you don't go far beyond human capability, because the bottleneck is out of distribution generalization. In software verification, you can verify just about all the software that exists despite the convex hull hypothesis, because the bottleneck is just scale.