形式手法とは，数学を基盤とした言語・技術・ツールを用いてソフトウェア/ハードウェアの仕様記述・開発・検証を行う手法群です．
数学を基盤としていることから安全性・信頼性を厳密に保証することができ，自動車・航空機・宇宙機の制御ユニットやOS，航空・鉄道管制系，CPU，暗号・通信プロトコル，医療機器などの高安全・高信頼が求められるシステムの開発・検証にしばしば適用されています．
しかし，基盤技術に理論的限界（計算不能性や計算困難性）があるため，実践応用のためには抽象化・近似・緩和等の技法を利用することや複数技術を組み合わせることなど，様々な工夫が必要です．
そのため，我々は形式手法の適用範囲を広げるための基礎技術開発や実製品の開発・検証への応用，他分野への応用の研究を行っています．
より広範に形式手法を適用できるように，システムの仕様記述・開発・検証の基礎技術/アルゴリズムの提案・拡張等を行っています．
企業との共同研究を通して，形式手法の理論と実応用の間のギャップを埋める技法・手法を開発し，産業界に展開可能な実践的な形式手法の確立を目指します．
また，AIシステムやブロックチェーン，生命システム等の記述・検証についても取り扱います．