一觉醒来，朋友圈被某位币圈大佬录音泄露事件刷屏，在这位被称为“比特币首富”、“区块链布道者”的大佬看来，区块链项目最重要的是流量和炒作，关于技术，录音中鲜少提及，这是被奉为“行业意见领袖”的人士对于区块链行业的最真实想法。这份录音像一记猛拳，打碎了“韭菜们”的心，也将行业的浮躁混乱暴露无遗。
在尚处于野蛮生长阶段的区块链行业，无法避免大量投机者涌入，他们在币圈混得风生水起，一个个创富神话吸引更多非理性投资者入局，大家对于币的关注度远远大于关注区块链技术本身。庆幸的是，无论环境多么浮躁，总有一些团队在默默耕耘技术，而未来的区块链行业，一定是属于这些深耕技术的人和团队的。
最近智链财经接触到的电子科技大学副教授杨霞和她创办的链安科技就是这样一支深耕区块链技术的团队。
来自成都的链安科技是专注区块链安全的公司，也是国内最早做区块链安全的，他们的VaaS平台通过形式化验证方法有效地提高了区块链生态系统的安全性。
从区块链诞生之日起，安全问题就像双生子，和技术演进的过程相伴相生。今年4月，BEC出现异常交易，黑客转出的代币数量超过发行数量，BEC市值几乎归零，就在前几天，Bithumb交易平台被盗3200万美元加密货币。交易所、钱包、智能合约等安全问题变得前所未有的重要。用杨霞的话说就是：区块链安全不亚于军事安全。
高精尖的人才和高精尖的技术
链安科技的创始人杨霞拥有博士后、电子科技大学副教授、最早研究区块链形式化验证的专家、主持国家核高基、十三五装发重大课题等近10项国家课题、发表学术论文30多篇、申请20多项专利等一系列头衔和经历，但是，与一般学者更倾向于在高校、科学院等“象牙塔”内专注科研和学术不同，杨霞表示自己最大的兴趣是把自己的研究成果应用到实际中，让它产生更大的价值。她一直在不断地尝试，把研究成果拿来去做成果转化，创办链安科技，已经是杨霞的第三次创业了。
杨霞原来主要做军事领域的安全关键系统的安全方面的研究，2016年以太坊第一个安全漏洞的发生把她的兴趣逐步转移到区块链中，这个事件让杨霞感觉到区块链智能合约安全是非常关键的问题，也需要有这方面的技术人员来提供一些安全保障。所以，从2016年下半年开始，杨霞面向区块链，尤其是智能合约的安全性展开研究。
目前，链安科技采用多种形式化验证技术做了VaaS平台，研发了第一套针对多个区块链智能合约的高度智能化的形式化验证工具，给区块链平台和智能合约提供军事级安全验证，杜绝逻辑漏洞和安全漏洞，确保系统安全性。杨霞介绍，形式化验证这套方法原来一直在军事领域，或者是比较尖端的安全管理软件里应用，比如导弹控制、战斗机的控制系统。所以它对代码自身的安全性和正确性的保障是非常好的一种手段。链安科技将这套方法移植到区块链中，杨霞认为区块链安全的重要程度不亚于传统的安全攻坚系统。
形式化验证：用数学手段证明代码刚好满足期待，不多也不少
杨霞介绍，形式化验证的目标就是证明这个代码是达到我所期待的，它实现的功能不能多也不能少，正是我想要的。但证明它没有多也没有少比证明达到我的期望更难，这要求列出举出所有导致故障的可能。形式化验证弥补了测试不能穷举的缺陷，用数学手段证明的方法去证明它刚好满足期待，不多也不少。如何做到这一点，链安科技有一套自己的方法。
首先，为了证明这个系统建立一个形式化模型和描述，再进行形式化验证，最后得到一个想要的系统，从设计到实现的整个流程都会引入形式化验证方法，这样的系统正好满足期待。
其次，所写代码究竟应该有什么功能，是否要给这个系统有一个功能描述的文档，对这些进行形式化的建模，这个是第一步，叫做形式化规格，就是对代码所要达到的用户功能需求设计文档，然后对代码的实现、代码的变量、代码的函数和私有进行形式化描述，给出前置条件、后置条件，这个函数在执行之前是什么样的状态条件，执行完这个函数以后能够得到什么结果，把这个设定好以后就进行证明。通过这样一种严格的数学证明手段，把代码编成数学模型，再通过证明手段证明这个代码是完备的、安全的。
VaaS ——支持以太坊、EOS等多个区块链智能合约的形式化验证平台
链安科技研制的形式化验证平台VaaS 平台已支持主流区块链平台（如以太坊、EOS等）智能合约的形式化验证，并且已与国内10多家区块链行业的知名企业建立了合作关系。
杨霞介绍，VaaS形式化验证平台，采用了多种形式化验证方法，具有验证效率高、自动化程度高、人工参与度低、易于使用、支持多个合约开发语言、可支持大容量区块链底层平台的形式化验证等优点。VaaS提供了针对智能合约的形式化验证工具，极大提高了智能合约的安全性与可靠性。产品通过对合约代码进行严格的安全验证，杜绝逻辑漏洞，确保合约安全，在满足实际应用效率需求的同时，达到有效控制漏洞风险的目的。
迅猛发展的链安，未来可期
杨霞2016年下半年开始研究智能合约的形式化验证，今年3月创办链安科技，获得分布式资本投资，是其投资的唯一一个从事区块链安全的公司。5月，链安科技入选工信部2018年区块链白皮书，入选的区块链安全公司仅有两家，链安是其中一家。同样在5月，链安和全球最顶级的形式化验证团队建立了合作，同时成为火币、OKex和KuCoin等交易所指定智能合约安全审计单位。
作为国内最早做区块链安全的公司，链安成立仅3个月成果不断，被问到是否当心被抄袭，杨霞自信地说：“我们是第一个做区块链形式化验证的公司，之后可能会有别的人也想进来，我觉得这也是一种很好的现象，至少说明大家在关注这件事，也都想在里边做点自己的贡献。我不担心别人的抄袭，首先有我们的技术壁垒，我们的核心成果有专利保护；其次，形式化验证这个方法的门槛很高，能做的人非常少，再者像我们这样又懂区块链、又懂形式化验证的人就更少了。所以我认为我们短时间内应该是很难被超越，当他们再进来的时候，我们也在更快速的前进。我们会不断地前进，把握我们的优势。”
最近，杨霞参与火币公链技术领袖的竞选，因为是第一个参选的女性而颇受关注，谈及参选的原因，杨霞表示，这是偶然，也与公司规划有关。杨霞有一个理想，做一条安全的链。因为链安现在做的形式化验证主要解决了智能合约的安全问题，之后希望可以对于区块链平台的安全做一套完善的解决方案。杨霞认为火币的全球公链与自己的设想契合，于是两者合作完成这样一件事情，可以把现在的技术优势发挥得更好。
行业过于浮躁 呼吁区块链爱好者多关注技术
“我感觉目前区块链还是比较浮躁，对于币的涨跌的关注度远远大于关注区块链技术本身，我觉得这是一种很不健康的状态……”杨霞对于区块链行业的现状表示忧虑，她说自己不参与虚拟币的炒作，自己也不买币。进入区块链行业是因为看好这个技术，并不打算投机赚快钱。
尽管深处浮躁的行业环境之中，杨霞依然坚持踏踏实实做事。链安科技的总部设在成都，杨霞形容成都是整个大的浮躁环境中的一片净土。她认为，成都虽然在区块链产业发展上落后于一线城市，但成都有技术上的优势，且成都提供了区块链创业者安静的环境，大家可以踏踏实实地做事情。
忧虑的同时杨霞对未来区块链行业的发展保持乐观的态度，她说：“至少今年相对去年，关注技术人更多了，投资人也希望看一些更实在的，关注技术的人和团队。所以我觉得未来的一到两年，关注区块链技术的人会越来越多，落地应用也会越来越多。区块链安全作为这个行业的一个刚需，我们觉得也就更加有信心。”