Is there a formalization of the computational model for quantum computers?
Yes.  The quantum Turing machine is a mathematical formalization of a computation model for a quantum computer.

See also https://en.wikipedia.org/wiki/Quantum_computing#Developments and https://en.wikipedia.org/wiki/Quantum_complexity_theory and https://en.wikipedia.org/wiki/BQP.