形式手法では、プログラム言語のような形式言語（VDMやAlloyなど）を使って設計対象を厳密に表現します。生成AIによるプログラミングが実現しつつある昨今、プログラムに求められる仕様を厳密に表現することが重要になっていくと考えられます。
形式手法の一つで、数学の定理を証明するようにシステムの正当性を証明します。本研究室では定理証明言語（CoqやAgda）を用いたシステム検証について研究を行っています。
SAT(Satisfiability problem: 充足可能性問題)は命題論理式の解の有無を判定する問題で、これを応用すると大量の組合せから求めるものを見つけることができます。本研究室ではSATを効率的に解く方法を探求しています。