C言語によるCBMC(有界モデル検査技術)を使用したPDD(証明駆動開発)を藤倉さんが提唱されている。 http://tfujikura.blogspot.com/search/label/PDD OCaml似の文法を使用するCoqによる証明駆動開発に比べて、c(c++)言語で仕様を書けるのでとてもわかりやすい…