copilot-verifier is an add-on to the Copilot Stream DSL for verifying the correctness of C code generated by the copilot-c99 package. copilot-verifier uses the Crucible symbolic simulator to interpret the semantics of the generated C program and and to produce verification conditions sufficient to guarantee that the meaning of the generated program corresponds in a precise way to the meaning of the original stream specification. The generated verification conditions are then dispatched to SMT solvers to be automatically solved.