David Lazar on his open source base64 encoding:
The C code in base64encode.c is a fast implementation of Base64 encoding. It is based on libb64, which uses coroutines to achieve speed. The nontrivial control-flow of this code makes proving it correct more challenging.
The writeup includes background information on “the proof” verifying the C implementation.
The code is available on github.