[hacs] hacspec

[Franziskus Kiefer]

Hi all,

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).

There are spec examples in F*, Fiat-Crypto, Cryptol, and VST as well as an
experimental spec checker from Aaron [2].

Thanks to Trevor we now have a mailing list as well [3] to keep the
discussion going.
Everyone interested in hacspec should subscribe.

Cheers,
Franziskus

[1] https://github.com/HACS-workshop/hacspec
[2] https://github.com/HACS-workshop/hacspec/tree/master/spec-checker
[3] https://moderncrypto.org/mailman/listinfo/hacspec
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://moderncrypto.org/mail-archive/hacs/attachments/20180123/5eb48c15/attachment.html>