>>307
有名なんで紹介するのも気が引けるんだけど、Coqっていうソフトやら、証明
を形式的に記述して検証するものっていろいろあるよね。
その手のソフトの下地の理論を探れば、検証する方法の勉強はできそうだが。