A formal proof for the fpcmp module can be found here: https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/fpcmp/formal/proof_fpcmp_mod.py;h=4f3d273ebbff4ea2c5133134383600d14e8c2683;hb=HEAD