> You typically can't "raise an error" in such contexts in formal reasoning tools.

You could write all your formulas in the Maybe / Option monad (which I guess is the same as 'introducing a "special" value') but that sounds painful...