Real Arithmetic in TLAPM

\(\textsf {TLA}^+\)  is a formal specification language for modelling systems and programs. While \(\textsf {TLA}^+\)  allows writing specifications involving real numbers, its existing tool support does not currently extend to automating real arithmetic proofs. This functionality is crucial for proving properties of hybrid systems, which may exhibit both continuous and discrete behaviours. In this paper, we address this limitation by enabling support for deciding first-order real arithmetic formulas (involving only polynomials). Specifically, we update the \(\textsf {TLA}^+\)  Proof System (TLAPS) to support reals and basic real arithmetic operations and implement them in the \(\textsf {TLA}^+\)  Proof Manager. The latter generates assertions in SMT-LIB and directs them to a selected backend (currently the Z3 SMT solver, which supports the theory of nonlinear real arithmetic). We motivate this functionality with problems arising in safety verification.