これまで多くのオブジェクト指向モデルの検証法が提案されているが，その多くは状態遷移図に基づくものである．これらの手法の問題点として，複数のオブジェクトにまたがる性質の検証が困難であることが挙げられる．これは，複数の状態遷移図の合成による状態爆発が原因である．我々は，そのような性質をコラボレーションの視点から検証する方法を提案する．コラボレーションは，クラス構造に横断する概念であり，オブジェクト間の相互作用を直接捉えることが可能な側面である．我々は，検証の土台として，オブジェクト指向理論を定理証明システムHOLに定義した．本論文では，理論の定義とHOLへの実装法，及び，その理論を用いた検証例を述べる．