首发|CertiK：蚂蚁集团即将上市“蚂蚁链”诞生与CertiK达成合作伙伴关系

这年头，出门可以不带钱，但是不能没有支付宝。

这时代，可以不申信用卡，但是不能没有花呗。

一个月前，蚂蚁换掉已沿用6年之久的“蚂蚁金服”简称，并将工商注册名变更为“蚂蚁科技集团股份有限公司”

北京时间7月20日，支付宝母公司蚂蚁集团宣布，将启动在上交所科创板和港交所主板寻求同步发行上市的计划。据媒体报道，蚂蚁集团寻求IPO估值至少2000亿美元（约1.4万亿元人民币）。

北京时间7月23日，蚂蚁集团举办“链接万物、无限未来”蚂蚁全新品牌发布会。“蚂蚁区块链”品牌正式更名为“蚂蚁链”。

蚂蚁的成长

2004年12月8日，支付宝正式注册成立。从支付宝到蚂蚁金服，再到今年更名为蚂蚁集团，有着16年岁月的蚂蚁集团逐渐有了吞噬大象的力量。

2009年11月11日，支付宝正式推出手机支付服务。

2013年6月17日，支付宝与天弘基金合作的货币基金产品余额宝上线。

2014年10月16日，起步于支付宝的蚂蚁金融服务集团（蚂蚁金服）正式宣告成立。

2019年2月25日上午，蚂蚁区块链科技（上海）有限公司在黄浦区揭牌成立。

直到2020年：

蚂蚁区块链每日上链超过1亿条

解决信任难题的场景已落地50余个

连续4年全球区块链专利申请数量第一位

每一年，它的估值都在增长，直到今天高达1.4万亿人民币。按照7月20日收盘价计算，蚂蚁集团上市后将跻身A股前四，港股前六，甚至可以挑战第一位的茅台。

蚂蚁的选择

人们常说，人生的选择没有对错，每一次的决策都是最好的决定。

而蚂蚁集团的每一次选择，恰好都是那真真正正最好的决定。每一次的决定，都是更上一层楼的成长与奠基。倘若有无数的平行宇宙，那么这个世界的蚂蚁一定是最出色的蚂蚁。

2020年，蚂蚁区块链选择与CertiK吞吴进行合作。作为全球领先的智能合约以及区块链生态的形式化验证平台，CertiK吞吴成为了蚂蚁联盟链首批入住节点合作方。在此次合作中，除了节点运营，CeritK还将利用自主研发的DeepSEA语言编译器在蚂蚁区块链EVM虚拟机上运行代码，为蚂蚁金服区块链平台提供定制化的安全保障，并为蚂蚁区块链的安全赋能。

一向做出正确选择的蚂蚁，是如何分析出CertiK吞吴是个绝佳选择的合作方呢？

蚂蚁的智慧

安全是任何区块链系统实现透明及信任的基础，蚂蚁区块链也不例外。正是因为蚂蚁区块链的安全要求如此之高，这些要求最终只可能被可机器检查的安全数学证明所满足。而形式化验证是当今检验代码无漏洞并对代码的数学事实进行验证的唯一可靠方法。因此，一向能做出最佳判断的蚂蚁，智慧地选择了以形式化验证为基础技术的CertiK吞吴。

今天，几乎所有的智能合约都是用未被设计支持形式化验证的语言写出来的。造成这种情况的一部分原因是因为缺乏编程语言的支持。现有的语言（例如C语言或OCaml或Solidity）都无法与验证工具很好地结合在一起，且需要大量时间来创建和验证人工证明。

DeepSEA——由耶鲁大学及哥伦比亚大学支持、开发的安全智能合约跨链编程语言以及编译器等工具，提供了这样一种方法。这种方法可保证编译过程不会引入错误，并且可以直接接入形式化验证引擎，生成合约正确性的可检验证明。可检验证明也可以存储在区块链上，保证运行的合约与验证的一致。

DeepSEA的研发目标

虽然程序漏洞的检测和验证已经被业界高度重视，但在区块链行业内的安全问题仍旧频繁发生。如果仅局限于检测已经存在的漏洞的话，永远有可能会被黑客抢先一步。因此，企业级区块链（比如蚂蚁区块链）需要支持能够直接开发可信智能合约的技术与工具。

众所周知，智能合约一旦部署，将无法进行修改。近日以来DeFi项目出事频频，想要高枕无忧而又不需额外开销进行安全审计，最好的办法就是把项目直接用DeepSEA搭建起来。这将大大降低未经验证的智能合约一旦被部署之后遭受黑客攻击的可能性。

DeepSEA的核心技术

DeepSEA是一个函数式编程语言，使得用其编写的智能合约能够在辅助证明工具（Coq）的帮助下被完全证明其安全性及正确性。DeepSEA能够让开发人员在智能合约中引入交互式形式化验证技术，并将智能合约100%正确地编译成以太坊虚拟机（EVM）等机器代码。DeepSEA可以帮助开发者抽象出智能合约所对应的数学模型，并导入到Coq辅助证明工具中。这样开发者就可以在Coq中对程序进行手动或者半自动证明。

DeepSEA核心技术结构

DeepSEA解决的问题

程序开发层面，DeepSEA框架致力于处理编程中的“固有冲突”。现今的主流操作系统和虚拟机管理程序仍然是用类似于C语言的语言编写的，我们发现，高级的形式化推理和低级的系统编程之间存在着一些固有冲突（Inherent Conflict），比如：前者是依赖于高抽象级别的丰富理论，后者却必须操控和管理低级别的硬件资源。

Solidity是一种高级编程语言，但是很难将其所有规范都纳入Coq证明辅助器中，如果某一规范中存在漏洞，那么整个程序则不可信。而以太坊虚拟机字节码（EVM Bytecode）是由低级语言开发完成的，若用人类的思维去演绎推理，则是一个非常艰难和繁琐的过程，所以这两个语言在转译时就容易出现错误、漏洞、或者规范不匹配的情况。

DeepSEA编译器的出现能够有效解决这个问题，并能保证程序语言安全、准确地从源代码级别被转译到字节码级别。无漏洞编译器是DeepSEA与其它区块链形式化验证技术的重大区别之一。

DeepSEA的应用

DeepSEA语言应用场景广泛，对于自带金融属性的智能合约比如供应链管理、货币交易平台、付款网络，多重签名钱包等都能提供安全壁垒加持，并有效保护用户的数字资产不受侵犯。

蚂蚁的助力

在未来，蚂蚁链将与CertiK吞吴进行更深入的合作。双方将通过领域内优势互补，资源共享、战略共赢，进一步提升双方在区块链和安全领域中的功能和作用，从而打造一个安全的区块链生态系统。

在今后合作过程中，CertiK也将开发出更多元的安全产品，为蚂蚁链提供更完善的安全保障。

官方网站：https://cn.certik.io/

安全合作邮箱：[email protected]

—-

编译者/作者：CertiK中文社区

玩币族申明：玩币族作为开放的资讯翻译/分享平台，所提供的所有资讯仅代表作者个人观点，与玩币族平台立场无关，且不构成任何投资理财建议。文章版权归原作者所有。