形式証明とは
形式証明とは、状態機械を出力関数と状態関数によって記述し、そのどの状態であろうとも期待する性質を満たすことを計算機を用いて証明することを目指す手法です。
今回は、 +INDAO (Identified Nested DAO) とその派生実装である +OpenTEE や +Decentralized Autonomous Deliberative Democratic States に関して、それらを「民意健全性というStateを持つ状態機械」と見做して、その状態機械への状態遷移のsafetyやlivenessのようなpropertyを常に満たすことを示そうと考えています。