As others have mentioned, it's possible and has been done in the FlocQ library. I don't have personal experience using them. I would expect proving properties t

As others have mentioned, it's possible and has been done in the FlocQ library. I don't have personal experience using them. I would expect proving properties to be somewhat challenging. There is a book available https://www.elsevier.com/books/computer-arithmetic-and-formal-proofs/boldo/978-1-78548-112-3 https://www.elsevier.com/books/computer-arithmetic-and-forma... You may also want to look at this thesis https://www.lri.fr/~melquion/doc/19-hdr.pdf https://www.lri.fr/~melquion/doc/19-hdr.pdf