2026年度未踏ターゲット事業(量子コンピューティング技術を活用したソフトウェア開発分野)採択プロジェクト概要（佐藤・名越・髙木PJ）

1．担当プロジェクトマネージャー

• 藤井 啓祐（京都大学 大学院情報学研究科 教授）

2．採択者氏名

• 佐藤 直人（StarWorks合同会社/北陸先端科学技術大学院大学）
• 名越 龍一（北陸先端科学技術大学院大学）
• 髙木 翼（北陸先端科学技術大学院大学 准教授）

3．採択金額

• 3,960,000円

4．プロジェクト名

• 高信頼量子通信のための形式検証ツールの開発

5．応募部門

• ベーシック部門

6．応募枠

• 通常枠

7．関連Webサイト

• なし

8．申請プロジェクト概要

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

9．採択理由

量子通信プロトコルの形式検証は、将来的な量子ネットワーク社会において重要な基盤技術である一方、現状では専門性が高く、一部の研究者しか扱えない状況にある。本提案は、Maude を用いた高度な形式検証技術をベースにしつつ、DSL やユーザーインターフェースを整備することで、その利用を広い技術者・研究者層へ開こうとしている点を高く評価した。特に、量子通信プロトコルに対する代数的仕様記述ベースの形式検証ツール開発は世界的にも前例が少なく、挑戦的なテーマである。提案者らは既に関連する研究実績と実装経験を有しており、理論と実装の両面から高い遂行能力を備えたチームであり、将来世界で広く使われる基盤的なソフトウェアとなることを期待したい。