There is also SSProve which has similar goal to CryptHOL: https://dl.acm.org/doi...

		nioj 7 months ago \| parent \| context \| favorite \| on: There Is No Diffie-Hellman but Elliptic Curve Diff... There is also SSProve which has similar goal to CryptHOL: https://dl.acm.org/doi/full/10.1145/3594735 https://github.com/SSProve/ssprove