学生の佐藤直人さん（博士前期課程2年、コンピューティング科学研究領域、髙木研究室）、名越龍一さん（博士後期課程1年、コンピューティング科学研究領域、髙木研究室）およびコンピューティング科学研究領域の髙木翼准教授の提案プロジェクト「高信頼量子通信のための形式検証ツールの開発」が、独立行政法人情報処理推進機構（IPA）の2026年度未踏ターゲット事業（量子コンピューティング技術を活用したソフトウェア開発分野）に採択されました。

　未踏ターゲット事業は、革新的な次世代IT技術を活用し、社会を大きく変える可能性のある先進分野において、基礎技術や領域横断的な技術革新に取り組むIT人材を支援する事業です。事前に設定されたテーマに基づき提案を募集し、採択者はプロジェクトマネージャーや企業・大学等の支援を受けながら、自らのテーマの実現に向けたプロジェクトを推進します。

■プロジェクトの概要
　本プロジェクトは、量子通信プロトコルの正しさと安全性を数学的に保証するための自動形式検証ツールを開発するプロジェクトである。中核には代数的仕様記述言語Maudeを用い、量子通信に特化したDSL（ドメイン特化言語）とユーザーインターフェースを整備することで、形式手法の専門家でなくても検証を実行できる環境を実現する。既存プロトコルだけでなく新規設計にも適用し、仕様充足、バグの有無、第三者攻撃への耐性を自動的に確認することで、人手検証に伴う見落としやバグの見逃しを防ぐ。量子テレポーテーション系を含む代表的な量子通信プロトコル群でツールの効果を実証し、高信頼な量子通信基盤の社会実装を加速させることを目指す。さらに、検証結果の再利用性と拡張性を高めることで、将来的な標準化や産学連携での実運用にもつながる基盤技術としての価値を提供する。

＊詳細は独立行政法人情報処理推進機構のホームページをご覧ください。

令和8年6月2日