<div dir="ltr">
<div>Hi all,</div><br>let's get this mailing list started.<br><br>The 
goal of HacSpec is to define a new specification language for crypto 
primitives that is succinct, that is easy to read and implement, and 
that lends itself to formal verification.<br><br>During the recent HACS 
workshop we started working on HacSpec. Karthik and I improved a little 
on that over the last couple of weeks and we would like to get more of 
you involved.<br><br>HacSpec lives on Github [1].<br><br>There is a HacSpec demo of ChaCha20Poly1305 [2] and a very experimental HacSpec to F* compiler from Karthik [3]<br><br>There are also spec examples in F*,  coq, cryptol, and easycryp [4] as well as an experimental spec checker from Aaron [5].<br><br><br><div>We
 would like to invite anyone to contribute to any part of HacSpec. In 
particular we invite people to contribute specs, test-vectors, code, and
 translation tools.</div><div><br></div><div>Note
 that HacSpec does _not_ aim to be general enough to express protocols 
at this point. While this might be a target in the future the first 
iteration of HacSpec is only targeting crypto primitives.<br></div><div><br></div><div><br></div>Fore reference:<br><div>* The mailing list can be accessed at <a href="https://moderncrypto.org/mailman/listinfo/hacspec" target="_blank">https://moderncrypto.org/mailm<wbr>an/listinfo/hacspec</a><br></div><div>* I wrote a short blog post [6] about HacSpec and what we want to achieve.<br></div><br>Cheers,<br>Franziskus<br><br>[1] <a href="https://github.com/HACS-workshop/hacspec" target="_blank">https://github.com/HACS-worksh<wbr>op/hacspec</a><br>[2] <a href="https://github.com/HACS-workshop/hacspec/tree/master/specs" target="_blank">https://github.com/HACS-worksh<wbr>op/hacspec/tree/master/specs</a><br>[3] <a href="https://github.com/HACS-workshop/hacspec/tree/master/spec-compilers" target="_blank">https://github.com/HACS-worksh<wbr>op/hacspec/tree/master/spec-co<wbr>mpilers</a><br>[4] <a href="https://github.com/HACS-workshop/hacspec/tree/master/formal-models" target="_blank">https://github.com/HACS-worksh<wbr>op/hacspec/tree/master/formal-<wbr>models</a><br>[5] <a href="https://github.com/HACS-workshop/hacspec/tree/master/spec-checker" target="_blank">https://github.com/HACS-worksh<wbr>op/hacspec/tree/master/spec-ch<wbr>ecker</a><br>[6] <a href="https://www.franziskuskiefer.de/post/hacspec1/" target="_blank">https://www.franziskuskiefer.<wbr>de/post/hacspec1/</a><br>

<br></div>