[randomvisitor]

It's pretty impressive that this can be done completely automatically (model checking), although the price to pay is that he can only prove the implementation for a fixed input size.

I'm very curious about what would happen if he dropped the safety check in base64_encode_value(). It would probably speed things up a little, but would the proof fail?

[cbsmith]

Yeah, I thought the safety check was rather curious really. It was also odd to use a NULL terminated string for the encoding set instead of a straight 64-byte array (sure, you only save 1 byte, and most compilers will no doubt waste that byte ANYWAY just for memory alignment reasons, but it still struck me as surprisingly... imprecise).