I'm not sure why the example used for formal verification is Z3, and not proof assistants like Coq or Agda. SMT solvers have made verification a lot more accessible, but Coq is strictly more expressive than Z3.