In this paper, we present HELIX, a formally verified operator language and rewriting engine for generation of high-performance implementation for a variety of linear algebra algorithms. Based on the existing SPIRAL system, HELIX adds the rigor of formal verification of its correctness using Coq proof assistant. It formally defines two domain-specific languages: HCOL, which represents a computation data flow and Sigma-HCOL, which extends HCOL with iterative computations. A framework for automatically proving \textit{semantic preservation} of expression rewriting for both languages is presented. The structural properties of the dataflow graph which allow efficient compilation are formalized, and a monadic approach to tracking them and to reasoning about \textit{structural correctness} of Sigma-HCOL expressions is presented.