現代社會是一臺龐大的機器。它讓我們每個人都從事精細化分工的工作。於是「專業」越來越像一個黑盒，人們可以通過黑盒的 API 與不同專業的人進行合作，卻很難了解黑盒內部到底是怎樣運作的。

正因爲如此，區塊鏈對我而言是一個有意思的領域。因爲這裏學科交叉的現象非常普遍。你不僅會遇到計算機行業裏的人，還會遇到經濟、金融、政治與社會學的人。和這些人聊天又是一種非常神祕的體驗。就好像，他們會爲你拆開一個陌生的玩具，展示其中的齒輪和零件。

大概一週前，我們約了一個區塊鏈安全團隊的創始人聊天。這位朋友之前在中科大研究了十幾年的「形式化驗證」，屬於非常冷門小衆的專業。機緣巧合，最近這個專業因爲區塊鏈的出現火了，就像「密碼學」那樣。我們和他聊了很久，他用兩個小時爲我們拆開了另一個陌生的玩具。這讓我們感到非常有趣。因此現在我們想把這個玩具也分享給橙皮書的讀者們。

如果你是一個好奇心很重的人，我們強烈推薦你閱讀這篇文章。它會用說人話的方式告訴你「形式化驗證」是用來幹嘛的，爲什麼區塊鏈安全的未來只有開源是不夠的，它還應該用去中心化的方式，由機器自己證明自己可信，而不是把信任寄託於一箇中心化的安全公司。

郭宇，從 05 年開始在中科大研究「形式化驗證」，現在是區塊鏈安全公司安比（SECBIT）實驗室創始人。

有人說，數學證明是特別純粹的，證出來是對就是對，是錯就是錯。其實這個說法是錯誤的。我們可能永遠都找不到聖盃。歸根到底，我們總要依賴於一點點其他的東西。你總需要一個小小的支點。這個支點已經是人類文明的精華了，但它永遠做不到 100% 可靠。

對很多沒聽說過「形式化驗證」的人，你可能暫時沒辦法理解它背後一些很美的東西。

沒關係，今天我想用一個故事向你們介紹這種美。如果你覺得有意思的話，可能也會順帶理解區塊鏈美的地方在哪。

1

對我來說，形式化驗證是在追尋計算機領域裏的聖盃。它要解決的問題，是怎麼保證軟件裏沒有 bug 。你肯定會很驚訝，軟件有 bug 這件事幾乎是一定的。只要涉及到複雜代碼，就很難避免出錯。

怎麼保證它沒有 bug 呢？

從計算機出現開始就有很多人在研究這個問題，但一直沒人能給出答案。所以，它是一個聖盃。就像一本誰都沒看過的武林祕籍。

我大概是 05 年開始搞這個東西的。形式化驗證是一個非常小衆的研究方向。當時我在安徽的中國科學技術大學裏，我們實驗室想招研究生，非常難招。因爲同學們都跑去研究人工智能了。而形式化驗證他們很多人壓根就沒聽說過。

但最近兩年，這個非常冷門的研究方向突然火了。主要還是因爲區塊鏈橫空出世，吸引了很多人進來研究。就像密碼學跟着區塊鏈火起來一樣。以太坊創始人 V 神一定程度上也助推了「形式化驗證」的發展。

那麼，到底什麼是形式化驗證？

我們都知道，代碼和程序是邏輯性很強的東西。既然邏輯性很強，那我們當然也可以用邏輯來推理它，論證這個軟件到底安不安全、有沒有 bug。只不過平常我們所理解的推理，可能都是在自己的大腦裏進行的。像柯南破案那樣，一步步地推演。但現在我們需要把這個推理的過程，用更嚴謹、更標準的數學和數理邏輯的方式表達出來，讓計算機能夠看懂——這個東西就叫形式化驗證。

2

爲什麼形式化驗證會非常小衆？

除了因爲本身在尋找聖盃外，還有一個原因是它對技術門檻的要求比較高。

如果你想研究形式化驗證，首先需要先弄懂這套邏輯系統的語言。人們平常溝通的時候，講話用的是自然語言和文字，很直接，很簡單，彼此也很容易聽懂。但邏輯語言全部都是符號。你必須先弄懂符號是什麼意思。然後，你還要理解怎麼把你平常說的話，用這些符號表達出來。這個東西是最花時間的。

一般一個 PHD 剛入門，需要先花上很長的時間，不斷看東西，培養這種用符號表達的感覺。像小時候剛開始學造句一樣。等你會造句了，最後一步纔是開始寫作文。也就是把整個推理的邏輯論證出來。推理本身又會涉及到很多理論深度的東西。所以總結起來，它對門檻的要求確實比較高。

我研究這個東西十幾年了。我是 01 年在科大讀研，05 開始研究，07 年 PHD 畢業，然後留在科大當老師。讀研的時候，最開始一段時期做的是網絡研究，後來才做的形式化驗證。做了之後我發現，形式化驗證裏面有很多特別美的東西。它背後有很多特別美的數學理論。但很少有人能觸及到這種美。因爲你在觸及到這種美之前，需要花費非常多的時間來琢磨。

這點感覺跟區塊鏈挺像的。區塊鏈初看很簡單，但是你深入研究，反覆去做、去試驗，花上一些時間，你才能慢慢領略到區塊鏈背後美妙的地方在哪。

3

當時研究形式化驗證，我最大的苦惱是一直沒能找到合適的應用場景。

我們嘗試過很多方向的應用，大多數是操作系統內核的驗證，包括很多實時性的內核，比如工業控制、醫療設備、專用芯片這些東西。

我們還嘗試過存儲芯片方面的應用。閃存芯片上有一層很薄的軟件，這層軟件非常關鍵，不能有 bug，因爲它要用來確保存儲和讀取時候不會出錯。你平常用 u 盤如果沒有在操作系統裏退出直接硬拔出來，它就有可能會觸及到這層軟件的 bug，導致數據丟失。

我們希望把形式化驗證那套東西拿過來用，確保這些軟件代碼裏沒有 bug。這些應用場景的代碼量比較短又足夠複雜，所以適合拿來做驗證。

只有代碼足夠複雜才值得做形式化驗證，如果代碼太簡單就不需要了，你讓程序員肉眼看一下就能判斷有沒有 bug 了。

但即使是這樣，我們仍然覺得形式化驗證在工業應用上的性價比很低。因爲工程的變化速度太快了，理論距離實際使用，其實還是有不少的差距。

4

這個讓人苦惱的現象一直持續到 16 年。那時我開始研究區塊鏈的底層技術。

我看了比特幣和以太坊。當以太坊出現後，智能合約冒出水面。我很敏銳地察覺到，這裏面其實有一些很適合我們的新機會。智能合約是形式化驗證非常理想的一個應用場景。

我馬上就和一位朋友商量，要不要一起出來幹這件事：用形式化驗證的方式搞區塊鏈安全。那個朋友之前在 360 工作，他跟我說，要幹，不干你將來一定後悔。他本身也有連續創業的經驗，所以我當時就決定：出來創業。

於是今年 4 月份，我們拿了一點錢，就組建了一個團隊開始搞。這個團隊也是以我之前在中科大的幾個學弟爲主，還有一些早期就對區塊鏈非常感興趣的 90 後的小朋友。

5

現在很多形式化驗證慣用的方法是：弄一個黑盒，然後丟一段代碼進去，黑盒再吐出來一個結果：yes or no。

如果是 yes，那就說明丟進去的這段代碼沒有問題。如果是 no ，就說明代碼裏有 bug。但這種方式的問題在於，這個盒子本身是個黑盒。你沒辦法證明黑盒的正確性。所以這種方式更多還是用來找 bug。

比如芯片上的形式化驗證就是用「黑盒模式」找漏洞。你把芯片設計圖丟進黑盒裏，它儘可能去遍歷所有的狀態，然後找出一個反例，告訴你這裏有 bug，在某種情況下可能會出現什麼問題等等——但如果找不出來 bug 呢？是代碼本身沒有 bug 嗎？還是黑盒的能力不夠，找不出 bug？

所以這一類形式化驗證，你需要依賴於黑盒本身的正確性。當然你可以把這個黑盒開源，讓全世界的人幫你檢查看有沒有錯誤。但很少人有人能這麼做。因爲這塊技術目前還沒有做到那麼好。

6

我們從 05 年開始研究時，採用的是另一種最古老、最傳統、也是最笨的辦法。但這種方式有一個好處是，當它回答 yes 的時候，它會給出一個證據。這個證據是一個數學證明。就像你小時候在黑板上證數學題那樣，把證明過程寫出來就沒辦法造假。老師和同學都可以看到。所有人都可以檢查。

理論上這套方法是可以這樣做的，但實際上我們還做不到自動化。你肯定希望最理想的情況是直接把代碼扔進盒子裏，然後就能自動吐出來一個證明。但現在還做不到。這是理論的天花板。

我們現在是半自動化來做這件事。你想象下這個盒子上有一些輔助的把手，當你發現盒子轉不動的時候，就需要人工手動去搖一搖，丟進一段代碼，吐出來一段證明。這是一個通過人操控的盒子。

其實這個盒子是非常複雜的，上面有很多的把手，需要大量做研究的人不停地搖，而且需要搖上好幾年。我們當時跟很多國內的團隊聊，他們稱我們是原教旨主義。因爲像我們這樣乾的人很少。這種傳統的做法沒法工業化應用。懂得怎麼搖盒子把手的人其實很少很少。但我當時就很堅信，這個看似傳統的方法纔是未來。

這裏面很多人誤解了，覺得由人去搖把手很累，但這其實是人類體現自我價值的意義。就像證明「哥德巴赫猜想」是人應該要做的事情，不可能讓機器來做。人存在的意義就是在盒子卡住的關鍵時候去推動一下。

從一開始我就很接受這種哲學觀。它就應該這麼做。但另一方面，你搖上那麼幾年這個問題怎麼解決？當時我認爲，人搖的時間一定是越來越快的。把手會越來越少，盒子會越來越簡單。

事實也的確如此。經過十幾年的發展，這個方法反而被越來越多的人接納。因爲這個東西跟其他計算機技術的發展是一樣的。人們寫軟件是用一層一層的 stack ，「堆棧」，不斷壘起來。這種傳統的證明方式之所以低效，是因爲它沒有軟件棧，用的全部是最底層的技術，類似 if、else、and、or 這種非常底層的證明語言，那當然會很累。

但如果你有對應的軟件堆棧，有相應的框架和工具，你在很高的抽象層上去做證明，那就不會很累了。你不能因爲現在還沒有這種技術棧，就說這條方向沒有前途。這是我從一開始就非常相信的。事實也驗證了是正確的。現在很多人都在往這個方向走。

7

爲什麼智能合約出現後我會非常激動呢？

因爲智能合約的代碼量也是比較短的，但它對安全性的要求更高。智能合約一旦部署到區塊鏈上就不能再修改，所以它一定不能出錯。這些基本的特性就決定了它對形式化驗證是有需求的。

再加上區塊鏈的設計哲學是去中心化的，所以想要保證「智能合約的代碼裏沒有 bug」 ，這件事必須用一種去中心化的方式去證明。

也就是說，智能合約發佈到網上，如果它能自帶一個證明，就是最好的。

我們研究的那套形式化驗證的方法，移植到智能合約上就是要去琢磨，怎麼做出一些自帶數學證明的智能合約模版。

這種自帶證明的方式，跟「一箇中心化的黑盒直接吐出 yes or no 的結果」相比，它跟區塊鏈的思想是一致的。通過某一個機構爲智能合約做安全審計也不是未來。因爲它仍然依賴於機構的中心化的權威，無法確保智能合約可信。

而從另一方面來說，這種去中心化的方式效率上會更高。因爲生成證明是非常難的，需要大量人類的智慧，但檢驗證明是很簡單的。機器非常容易做。檢驗的難度，跟代碼的行數成正比。哪怕要驗證的代碼有一億行，用機器來做檢查仍然會非常快，因爲可以並行做。

所以我非常堅信，智能合約是我們這種傳統的形式化驗證方法一個絕佳應用場景。它去中心化的精神也和區塊鏈很像。

8

在我的腦海裏，未來所有的智能合約發佈到網上都必須帶一個自己的數學證明，

這個證明用來：

證明你幹了什麼事
證明你的管理員權限
證明你的合約對參與各方都是公平的
證明你沒有後門、你的分紅、鎖倉機制到底是什麼樣的
……

這是讓智能合約更可信必須要做的事情。

帶了這個數學證明，對於用戶來說，哪怕你看不懂證明過程到底是怎麼樣的，你也可以隨時就用另外的工具去檢查這個證明是否正確。

這套檢查的工具可以由其他不同的人提供，所有人都可以來做這樣的工具。這樣就給了用戶一個選擇，讓發佈智能合約的人，和負責審計的人，都沒辦法作弊。

9

很多人聽到這裏肯定會有一個疑問：這樣是不是就解決了我們一開始提到的「聖盃」問題？

其實遠遠不是。

爲一個程序帶上一個證明，這個證明寫了數學推理的過程，用來論證程序自身沒有 bug——但我們都知道，數學推理需要有一些公理作爲前提，然後才能往後進行推導。

如果這個前提本身是錯誤的，推理是不是也就不成立了？

舉個例子：密碼學裏的加密問題。

橢圓曲線簽名算法裏有一個假設叫離散對數難題。加密算法的安全性依賴於這麼一件事：解離散域上的對數是非常非常難的，它的解空間非常大，最後解出來的概率，會遠小於一個非常非常小的數。就像在大海里撈針。但如果量子計算機造出來，這個問題就不存在了。所以，「基於這個假設去證明這套密碼學是安全的」這件事本身也不可靠了。

在程序裏面也是一樣的。

比如我想證明 EVM （以太坊虛擬機）裏面的一段代碼跑出來的返回結果是 1，那麼我需要先把程序的語義表達出來，而這就是代碼級的形式化驗證會遇到的一個問題：很多編程語言的手冊很不完善，因此程序的語義翻譯很難做到 100% 精準。

一套編程語言的設計，語義往往會存在模糊的地方。因此，形式化語義的時候就會遇到一個巨大的鴻溝。

EVM 的設計水平已經算是比較高的了，以太坊黃皮書對語義的描述寫得很清楚，所以它可能是有 99.99% 的準確度，但也不是 100%。最終翻譯到形式化驗證裏，理論上還是有可能存在問題。如果有問題，推理的過程和實際在 EVM 上跑的過程，二者就不一致了。這樣推理過程本身就不可靠，所有的證明就沒有意義了。這個偏差是一定存在的。

形式化驗證還有一個嚴重的依賴，是推理的邏輯本身。換句話說，就是推理的邏輯本身有沒有問題。這點也是有可能會受到質疑的。

邏輯學至今已經發展了好幾百年，有本神書叫 GEB ——《哥德爾、艾舍爾、巴赫》，裏面也談到了這個問題。哥德爾是個超級聰明的人，他在 1931 年提出一個定理叫「哥德爾第二不完備性定理」。這個定理在說一個什麼事情呢？給定一個邏輯推理系統，你需要證明這個系統自洽不自洽。

所謂的「自洽」是指在這個邏輯系統裏沒有前提的情況下無法推出 False。用人話來說，你的邏輯不能前後矛盾。所謂的自洽系統，就是你永遠不可能說出自相矛盾的話。但「自洽」是需要證明出來的。一旦你要證明這個邏輯系統是自洽的，你就必須用一個更復雜的邏輯系統來證明。這個更復雜的邏輯系統又需要一個超級複雜的邏輯系統來證明它的自洽。

哥德爾第二不完備性定理明確提出：不可能有一個系統能證明自己自洽。它甚至很明確的找到反例說，如果你找到了一個系統能證明自己的系統邏輯自洽，那麼你的邏輯就不自洽。GEB 這本神書就在談論這個問題背後的整套哲學系統，整本書大概七百多頁，非常長，也很深，到現在我也纔看了三分之一。

我們在形式化驗證裏用來推理程序所用的邏輯，它有沒有問題呢？其實它也是個黑盒。但這個黑盒跟我上面說的那個黑盒不太一樣。它相對比較穩定，不怎麼變化。但它背後依賴的數學理論，「自洽性」也還沒有人證明過。只是有幾個數學家說，這裏面大概是沒有問題的。

其實在邏輯學上，有很多公理是互相矛盾的。

嚴格來說，必須真的有人證出來兩個公理是不矛盾的、可以一起用，我們纔可以去使用這些公理。但這些東西太複雜了，很多至今都沒有人能搞懂。

有人說，數學證明是特別純粹的。證出來是對就是對，是錯就是錯。其實是因爲他可能不太理解這套東西。搞邏輯學的人都知道，很多公理單獨使用可能沒有問題，但你再加入一個公理，這個系統還能否自洽就是未知的了。因此，很多數學家會憑着自己的直覺加進去，覺得沒問題，但具體有沒有證明過呢？需要另一套更復雜的邏輯。

這裏面是有很多開放性的問題。有很多不同的選擇。我們在做的時候，傾向於不去輕易引入一些甚至很有名的公理。能不用就不用。比如反證法，反正法會跟很多公理髮生矛盾，如果用了，說不定哪天就出問題了。

10

所以，我們可能永遠都找不到聖盃。

歸根到底，我們總要依賴於一點點其他的東西。你總需要一個小小的支點。而所依賴的這個支點，需要做到儘量可靠。但你永遠做不到 100% 可靠。

當然，我覺得這個支點已經是人類文明的精華了。因此還是比較可靠的。

這裏面還有很多非常有意思的故事。這也是爲什麼我會說它們背後有很多很美的東西。只是瞭解的人不多而已。

11

那麼，形式化驗證跟大家更熟悉的密碼學，他們之間有關係嗎？

有關係。

我個人覺得，密碼學這套歷史有一條線，可以把它分隔成兩半。在這條線之後，密碼學所有東西你要證明可靠；而在之前，你往往不需要證明，全靠經驗。

如果你現在隨便去買一本密碼學的書，大概率翻開，第一章會講「對稱加密」、第二章講「非對稱加密」、第三章講「哈希、隨機數」。這些東西都是沒有證明的，只是教你怎麼用而已。所以到頭來，你可能只是背了一堆的算法。這叫前密碼學。

但現在不一樣了。現在如果你自己想提出一個密碼學的東西，你必須先證明它的安全性。所以從某個時候開始，這在學術上稱作 Provable Security，「可證安全性」。如果現在新提出一個哈希函數是沒證明過的，那沒有人敢用。現代一點的密碼學的書，從一開始就要證明「爲什麼是安全的」。

所以就需要先定義什麼叫安全。

有很多不同種類的攻擊模型。「安全」指的是在某一種攻擊模型下的安全。也就是說，一個算法在某個攻擊模型下被證明是安全的了，那在現實生活中也不一定是安全的。因爲實際的安全環境，可能跟理論上的攻擊模型會不一樣。比如零知識證明、多方安全計算，都有他們各自的安全模型前提。你選了一個密碼學算法，你就要知道算法的安全模型是什麼。你必須搞懂每一種安全的前提和假設，才能不出錯。

每一個後現代密碼學書，英文書居多，一上來就要證明安全性。一直證明到，某個算法在某種攻擊模型下被攻破的機率，小於一個可忽略值，一般是 2 的 n 次方之一，纔可以。

近年來密碼學開始逐漸有了更多現代化的工具去做證明。這種證明不是寫在紙上那種，因爲裏面的邏輯是越來越複雜的，寫在紙上沒人看得懂，萬一跳步了怎麼辦呢？所以要用特殊的程序和工具去證明，保證每一步都執行。而且每一步的引理都必須寫得非常清楚，不能有模糊的地方。

密碼學現在幾乎都是這樣。你要提出新東西，都必須要證明。包括分佈式協議也要證明。如果不證，就說明它有的地方沒考慮清楚。有證明，才代表一個協議所有的角落都排查過了。

所以我認爲，未來在區塊鏈領域，證明也是會越來越重要的。

12

對區塊鏈行業來說，未來成熟的生態裏，智能合約必須具備三個關鍵要素：

1、安全。

保證代碼沒有漏洞。這是大部分搞安全的人正在做的事情，也是比較基礎的東西。但我個人覺得，這件事其實並沒有那麼有趣。

2、可信。

可信其實是目的。就是讓用戶信任某個智能合約。比如最近 fomo3d 很熱，但沒人知道這個合約對所有人是否都是公平的。它裏面部署了很多不同的合約，有的合約是不開源的。即使開源了，裏面的邏輯比較複雜也沒那麼容易能看懂。因此智能合約想要可信，最好合約作者的每個聲明都必須有配套的證明。這個證明必須和代碼掛鉤在一起，不管是源代碼還是編譯後的字節碼。

3、規範。

現在很多項目需要多個合約互相交互，所以不同合約之間就必須要有規範。比如，去中心化交易所其實就是一個智能合約。這個智能合約與其他 ERC20 代幣的合約進行交互，互相兌換。去中心化交易所要上幣的時候，審計智能合約有時候會重點去看，這個代幣的管理員有沒有權限凍結 token。如果有權限，那就很危險。

所以我們發現一個很有意思的現象，國外很多做金融 DApp 的公司，到最後都變成了一個合約審計的公司。因爲沒有審計公司能幫他們幹，他們自己審覈了一堆智能合約後，就有這個能力去幫別人審計合約，就可以去接這塊業務了。現在的智能合約本質上都不存在規範。ERC20、ERC721 這些標準都很粗糙。我們手上有形式化驗證的工具，也會幫去中心化交易所審計上幣的代碼，這樣效率會比較高。

我們發現規範性這個問題是很嚴重的。太多的智能合約缺少規範，因此很容易產生很多兼容性問題。比如我們都知道 ERC20 裏有一個變量叫 symbol，是用來表示代幣的名字，是叫比特幣還是以太幣。這個 symbol 的字母大小寫完全是混亂的，因爲它沒有具體的規範，規定必須怎麼寫。再比如函數執行失敗要不要 return false，還是不 return？這裏也有很多東西沒寫清楚。因爲沒寫清楚，大家就各做各的，導致最終的接口不一致。於是很多合約充值就會有漏洞。

我認爲合約只有規範了，DApp 才能真正繁榮起來。不僅僅只是 ERC20 這個合約標準，還有許多合約標準都有規範性問題。未來我們很有可能會在 ERC20 上面再搭一個棧，比如去中心化交易所，然後去中心化交易所上面再搭一個金融借貸類的棧，再往上還可以搭金融衍生品、資產管理——但你每往上搭一層，每一層都必須規範。只有每一層都打牢固了，才能造出高樓。

13

我個人相信，區塊鏈安全會是一個細分行業。而且它一定會不斷細分下去。

區塊鏈公司跟很多傳統公司不一樣。傳統公司一定要做大，要把很多業務進行整合，因爲只有整合才能發揮優勢。就像 BAT，每家都做外賣，每家都做支付，什麼業務都有。歸根到底，它只有把自己整合起來變成怪獸才能勝出。

但區塊鏈行業反而是，做好自己最擅長的事情就是最好的。因爲區塊鏈本來就是用來解決生產關係的。傳統公司需要有一個老闆發號施令讓員工往同一個方向走。區塊鏈行業是發現一個規律能掙錢，那大家就會自發往那走。

所以通過區塊鏈已經可以解決傳統公司的一些問題了。很多時候，你和別人之間是互惠關係。這種互惠關係加上 token 綁定，就會成爲一個小圈子。

就像現在的幣圈，它不是一個公司，就是一個小圈子，組織形式非常鬆散，但又有一致的利益綁定。這種運作方式遠比一個公司的效率來得高。爲什麼區塊鏈行業發展速度都很快也是因爲這個原因。沒有老闆，三人成軍。發展非常靈活。所以我認爲，區塊鏈公司不一定需要做大。

智能合約讓人們協作的成本變得很低。這也是我們選擇以智能合約爲中心做形式化驗證業務的一個原因。只不過現階段它還不掙錢。但這個方向，它跟傳統 BAT 的業務不太一樣。所以這些巨頭公司也沒辦法進來。

智能合約天生對協作就是友好的。而大公司想的是一定要把別人收購，這樣我們才能一條心。但同時，大公司各部門間的協作又會產生很多內耗。這是傳統公司不可避免的弊病。所以從這個角度來看，小公司也許更有優勢。未來我們認爲會出現越來越多的小公司。

14

公鏈的安全和智能合約底層的安全，其實僅僅只是區塊鏈安全領域的一小部分。未來更重要的部分也許是上層業務邏輯的安全。

現階段我們看到的大部分的漏洞是底層的漏洞，比如各種溢出。這是因爲現在大家還不瞭解區塊鏈技術，行業裏的程序員沒有經過行業的教育。但未來大家會變得越來越聰明，底層非常低級的安全漏洞會越來越少。

而上層業務會隨着整個行業的發展變得越來越複雜，可能出現的漏洞也會越來越多。代碼的行數在變大，智能合約的數量也在增加。而業務漏洞是安全審計公司做不來的，工具也做不到自動化檢查。因爲工具無法理解高層的業務意圖，傳統的安全公司也沒辦法解決這個問題。沒有完善的工具，配套人才非常稀缺。因此，區塊鏈安全是一片藍海。

今年 9 月初，我會在一個學術會議上做報告，給高校的人講「什麼是智能合約」。他們很多都沒聽說過智能合約，但一旦他們聽說了，很多人可能就會進來這個行業。因爲這些做形式化驗證研究的老師，他們會很敏感地察覺到，智能合約是一個大金礦。現在還沒有多少人在挖。我可能不需要跟他們講具體怎麼在智能合約上做形式化驗證，只需要給他們講智能合約現在面臨哪些問題，他們就能意識到這一點。因此，很多高校類的老師出來創業，這可能也會成爲區塊鏈的一個趨勢。