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.
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.