RMM and RMMD have been formally verified, as shown in a paper published to Usenix. The proofs should be checked in CI to ensure that they remain valid and are updated as needed.