Quantum error correction (QEC) is fundamental for suppressing noise and implementing fault-tolerant quantum computation in quantum hardware. We propose an efficient framework for verifying the correctness of QEC programs. An assertion logic is defined for specifying properties of Pauli operators and stabilizers, and it is interpreted as an extension of Birkhoff-von Neumann quantum logic with classical variables. This aids us in verifying more errors such as non-Pauli errors, while incorporating classical variables provides an interface for employing existing classical tools such as SMT solvers. The program logic is built for reasoning about the hybrid classical-quantum nature of QEC programs. An example of 7-qubit Steane code is presented, where both Pauli and non-Pauli errors are taken into account. At last, we discuss the future work, including: (i) formalization of the assertion logic and program logic in Coq; and (ii) a practical and efficient tool implementing the logic with Python libraries is under development.