Since real analysis is arguably the core of mathematics and of applications of mathematics, it has been formalised in many ways. See [1] for an overview of the state of the art.

[1] S. Boldo, C. Lelay, G. Melquiond, Formalization of Real Analysis: A Survey of Proof Assistants and Libraries., https://hal.inria.fr/hal-00806920v1/document