I don't know very much about formal methods but I would assume the type system plays an important role for encoding that specific states can or cant exist.
But a high reading is a state that can exist. I don’t really see how formal methods would exclude a multiplication/unit error with respect to the displayed unit.