You typically can't "raise an error" in such contexts in formal reasoning tools. There's no "runtime" per se to raise an error from -- the expressions themselves are manipulated to derive truths -- the division by zero may simply be implicit e.g. in a statement about division by some arbitrary number.

Trying to solve the problem with e.g. dependent typechecking quickly gets complicated (both implementation and theory). And adding a concept such as infinity may complicate proofs which now need to deal with infinity being a "number" but which behaves differently from other numbers.

Thankfully mathematics has the nice property that you can define concepts any way you want so long as they're self-consistent and match one's expectations. So rather than treating division by zero as an exceptional case -- either by disallowing it in the typesystem, "raising an error", or by introducing a "special" value -- some (most?) verification languages simply define division by zero to have a numeric value, and make it known that this is the case. Users know that they must then write expressions to be explicit about division by zero if they care about that case. (This turns out to be not much different than having to write expressions to satisfy a dependent type system.)