Several industry-strength quantum compilers has been actively developed, e.g. Qiskit, \texttt{Q#} and \texttt{t\textbar ket\textgreater}. However, current verification options for them either demand heavy manual proofs or rely on solvers ill-suited for linear algebra formalism of quantum computing. In this work, we propose a novel verification framework for Qiskit compiler that couples Verus (for structural contracts over Rust implementations) with Coq (for mathematical semantics), joined by abstact functions \emph{topo} that turns imperative compiler artifacts into functional, verifiable interfaces. Thus, it is convenient to prove that Qiskit compiler preserve program semantics.