Yeah! Formal methods are super interesting. I'm actually going to not take the auto-generate code approach and instead hand write all the code. Eventually I'll take another crack at modeling it with ProVerif... or better yet, Tamarin. Those tools can at least give us confidence that the cryptographic design is correct... but of course my code could be bad and those tools won't help with that unlike the tooling you suggested.
Looks like your constatine library has almost every cryptographic primitive function that I need! A NIKE like X25519 is essential. And like I demonstrated, it can easily be made to act like a KEM. I maintain a post quantum cryptography library in golang which features a NIKE to KEM adapter which is very useful for making your own hybrid post quantum KEMs: <https://github.com/katzenpost/hpqc> for a PRP i'd just go with AES 256 since i say someone made that available from bearssl or something. and then the PRF could be keccak or blake2 or whatever.
