RAHD (Real Algebra in High Dimensions) is a proof assistant and decision procedure framework for the existential theory of real closed fields. RAHD provides as inferential primitives a family of combinable automatic proof procedures for nonlinear real arithmetic. The system can be used to decide the satisfiability of purely conjunctive systems of nonlinear polynomial equations and inequalities over the real numbers.

Using RAHD's interactive top-level, the real solution space of a polynomial system may be explored (including the interactive construction of proofs regarding the satisfiability of the system in question), and users may build their own ``proof strategies'' targeted to structural properties of their problems of interest. These custom proof strategies then become primitive RAHD inference mechanisms and may, e.g., be made available on the command-line for use in domain-specific formal verification tool-chains.