In one case I formalized the spec for a message decoder, then autonomously generated the entire decoder from that. The spec is essentially a very slow version of the decoder written for correctness and clarity, and the implementation became very complex as it went through multiple optimizations, but it was proved every step of the way to match the original spec.