Current state-of-the-art multi-stage languages provide no guarantees beyond the well-typedness of the generated code. For safety- and security-critical systems, formal proofs of correctness establish confidence in the system. This work uses a novel approach to embed a fragment of C in dependently-typed Agda, enabling mechanised proof over staged C code. This work uses this embedding to reimplement Strymonas with proofs of correctness. This reimplementation achieves 4–140x the performance of Haskell’s stream-fusion library.