<div dir="ltr"><div>Hi all,</div><div><br></div><div>during the last HACS workshop we started working on a proposal for a new specification language for crypto primitives that 
is succinct, that is easy to read and implement, and that lends itself 
to formal verification. It lives on Github [1] (see the repo for more details).</div><div><br></div><div>There are spec examples in F*, Fiat-Crypto, Cryptol, and VST as well as an experimental spec checker from Aaron [2].</div><div><br></div><div>Thanks to Trevor we now have a mailing list as well [3] to keep the discussion going.</div><div>Everyone interested in hacspec should subscribe.</div><div><br></div><div>Cheers,</div><div>Franziskus<br></div><div><br></div><div>[1] <a href="https://github.com/HACS-workshop/hacspec">https://github.com/HACS-workshop/hacspec</a></div><div>[2] <a href="https://github.com/HACS-workshop/hacspec/tree/master/spec-checker">https://github.com/HACS-workshop/hacspec/tree/master/spec-checker</a></div><div>[3] <a href="https://moderncrypto.org/mailman/listinfo/hacspec">https://moderncrypto.org/mailman/listinfo/hacspec</a><br></div></div>