这个领域很新，收集了一些资料。
静态分析工具：
1 . M a n t i c o r e - 二进制符号执行工具， 支持E V M ，
获取地址： h t t p s : / / g i t h u b . c o m / t r a i l o f b i t s / m a n t i c o r e
2 . M y t h r i l - 以太坊智能合约逆向和安全分析工具，
获取地址： h t t p s : / / g i t h u b . c o m / C o n s e n S y s / m y t h r i l
3 . O y e n t e - 基于新加坡国立大学学者们的研究论文《M a k i n g S m a r t
Contracts Smarter》开发的智能合约安全分析工具，
获取地址： h t t p s : / / g i t h u b . c o m / m e l o n p r o j e c t / o y e n t e
4 . S o l g r a p h - 生成D O T 格式的图来可视化S o l i d i t y 智能合约的函数
控制流程并且显示可能的安全漏洞，
获取地址： h t t p s : / / g i t h u b . c o m / r a i n e o r s h i n e / s o l g r a p h
5 . S m a r t C h e c k - S o l i d i t y 代码静态分析工具， 可自动检测安全漏洞
和不安全的代码，
获取地址： h t t p s : / / t o o l . s m a r t d e c . n e t /
测试覆盖工具：
s o l i d i t y - c o v e r a g e ，
获取地址： h t t p s : / / g i t h u b . c o m / s c - f o r k s / s o l i d i t y - c o v e r a g e
这是几个学生做的形式化检查项目（论文，工具也开源了）：
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale
MAIAN
某个链请了下面这家公司做了智能合约的检查
CertiK是一家用形式化验证为智能合约和区块链应用提供最先进安全性服务的公司。形式化验证（Formal Verification）又是什么？用 CertiK联合创始人顾荣辉的话来说就是：用逻辑语言来描述规范，通过严谨的数学推演来检查给定的系统是否满足要求。
打开 CertiK 的系统，上传要检测的智能合约，用 CertiK 提供的标记语言，标注好要进行测试的代码部分，按下检测按钮。
检测完毕后， CertiK 会提供这份智能合约的安全系数，并告诉你哪一块程序存在着错误，并提供详细的解决方案。
2016 年10月，国家互联网应急中心发布《开源软件源代码安全漏洞分析报告——区块链专题》，针对区块链领域的知名开源软件，结合漏洞扫描工具和人工审计的方式，在代码层面发现高危安全漏洞746 个，中危漏洞3497 个，数量较多的高危漏洞有不安全的随机数、不安全的JNI、空指针解引用等
----2018年中国区块链产业白皮书【终版】
成都链安科技有限公司对区块链智能合约进行形式化验证，开发了面向区块链智能合约安全性和功能正确性验证平台VaaS。
厦门慢雾科技有限公司 -- 这家基本是人工分析
关于智能合约的重大漏洞有： TheDAO, MBC, EDU。
