This extended abstract presents a the formally verification a subset of SPIRAL, an efficient code generation system for digital signal processing algorithms and related computations. SPIRAL represents algorithms for linear transforms as sparse matrix factorizations using a domain specific language called the Signal Processing Language (SPL). To produce an algorithm, SPL expressions representing a signal transform factorization are rewritten through repeated application of factorization and matrix identities. SPL expressions representing completely factorized transforms can be compiled to a target language. A subset of SPIRAL’s algorithm space as well as an SPL compiler targeting a simple imperative language with arrays and values from a commutative ring, IMP+V, are verified using the Coq proof assistant.