图灵奖得主Lesslie Lamport近年来一直在推崇Formal Verification工具
TLA Plus
基本概念就是把软件架构写成数学状态机定义
然后透过Temporal Logic的理论来做到100%的正确性验证
但是TLA Plus没有办法直接转换成应用程式 所以用的人一直不多
基于这个概念微软又开发出了P语言
号称可以兼顾Formal Verification和应用程式开发
https://github.com/p-org/P