ConCert:Coq中的智能合约验证框架 源码

音乐会 Coq中的智能合约验证框架。 有关开发的详细信息,请参见。 演唱会能够找到真实世界的攻击作为解释和。 如何建造 我们的开发使用Coq 8.11.2。 并取决于从源代码,std ++和coq-bignums安装的MetaCoq。 测试取决于QuickChick。 大多数依赖项可以通过opam安装。 要设置具有必要依赖项的开关,请从项目的根目录运行以下命令: opam switch create . 4.07.1 eval $( opam env ) opam repo add coq-released https://coq.inria.fr/opam/released opam install -j 4 coq.8.11.2 coq-bignums coq-stdpp coq-quickchick opam pin -j 4 add https://github.com/Me