l1c is a simple formally verified compiler for a while language - View it on GitHub