NEO recently partnered with CertiK, an American-based formal verification company for smart contracts and blockchain ecosystems. CertiK is comprised of PhD’s from Yale and Columbia, as well as engineers who’ve worked at Google, Facebook, and Freewheel, amongst other Silicon Valley-based companies. Key features of the formal verification company include a “layer-based decomposition approach, pluggable proof engine, machine-checkable proof objects, certified decentralized application (dApp) libraries, and smart labelling.”
Beyond smart contract verification, CertiK also seeks to apply a specially tailored ‘formal verification’ to substantiate NEO’s digital assets and digital identity. When ‘logical languages’ are used to induce a function, CertiK’s formal verification will apply a ‘rigorous mathematical deduction’ to audit whether or not the function meets the system’s code requirements.
CertiK’s formal verification strives to ‘mathematically prove that smart contracts and blockchain ecosystems are bug-free and hacker-resistant.’ As a majority of the decentralized applications (dApps) built on the NEO blockchain have been developed by individuals, the formal verification aims to ‘rule out potential loopholes.’
On the partnership, NEO Global Development (NGD) manager Zhao Chen stated, “NEO is a high-speed autonomous public chain. With more developers building layers on top of it, this added security layer will expedite the prosperity of the ecosystem.”