  We report on our formalization of matrix-interpretation in Isabelle/HOL.
Matrices are required to certify termination proofs and we wish to utilize them
for complexity proofs, too. For the latter aim, only basic methods have already
been integrated, and we discuss some upcoming problems which arise when
formalizing more complicated results on matrix-interpretations, which are based
on Cayley-Hamilton's theorem or joint-spectral radius theory.
