圖靈獎得主Lesslie Lamport近年來一直在推崇Formal Verification工具
TLA Plus
基本概念就是把軟體架構寫成數學狀態機定義
然後透過Temporal Logic的理論來做到100%的正確性驗證
但是TLA Plus沒有辦法直接轉換成應用程式 所以用的人一直不多
基於這個概念微軟又開發出了P語言
號稱可以兼顧Formal Verification和應用程式開發
https://github.com/p-org/P