[randomvisitor]

> they are using unsigned 64-bit values (which conveniently have defined overflow semantics) for the lengths of the input buffer.

Yes, if you examine the code you can manually prove that it's safe: but that's not proven by their formal computer-checked proof.

As for the rest of your post: you seem to be assuming that what they proved is that b64enc.c behaves correctly. This is not true at all: they just proved that the helper function base64_encode() works correctly for a specific size (this is done in proof/sym_encode.c). This helper function never calls base64_encode_update() twice and is not used by b64enc.c, and that's why we don't know if the multiple-block implementation from b64enc.c actually behaves correctly.