From fkiefer at mozilla.com Tue Jan 23 00:38:37 2018 From: fkiefer at mozilla.com (Franziskus Kiefer) Date: Tue, 23 Jan 2018 09:38:37 +0100 Subject: [hacs] hacspec Message-ID: 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: