未踏IT人材発掘・育成事業：2025年度採択プロジェクト概要（戸田PJ）

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

• 曾川 景介（newmo株式会社 CTO）

2．採択者氏名

• 戸田 朋花（株式会社サイバーエージェント／株式会社AbemaTV）

3．採択金額

• 2,000,000円

4．プロジェクト名

• ソフトウェア設計のコード化と数学的検証を実現するGoフレームワークの開発

5．関連Webサイト

• goatx/goat

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

ソフトウェア開発では、設計と実装の乖離はシステムの品質低下や開発コストの増大を招く要因となっている。設計はMicrosoft PowerPointやMicrosoft Excelなどで管理されることが多く、それでは実装のコードと管理場所もライフサイクルも異なるため、実装との整合性の確認や維持は極めて困難である。その結果、仕様の不整合や論理的矛盾が後から発覚し、手戻りや障害につながるケースも少なくない。さらに、ITゼネコン構造の影響で、設計と実装の担当者が分断されてエンジニアが設計に主体的に関与しにくい状況を生み出し、この問題をさらに悪化させている。
この課題を解決するために、本プロジェクトでは「Design as Code」の概念を導入した、設計をコードとして記述し検証可能にする論理設計ツールを開発する。かつてDevOpsの思想に基づき「Infrastructure as Code」の導入が開発と運用の在り方を大きく変えたように、本ツールは「Design as Code」の思想により、開発における設計と実装の在り方を根本から変革することを目指す。
本ツールはGo言語を用いた論理設計ツールであり、システムの動作をステートマシンとイベントのやり取りとして定義し、数学的なモデル検査を適用することで、設計の妥当性を保証する。Goを活用することで直感的に設計を記述でき、学習コストを抑えつつ高度な検証を可能にする。また、設計がコードとして一元管理されることで、設計と実装の統合が進み、設計プロセスへのエンジニアの主体的な関与を実現する。
本ツールにより、単なる設計の自動検証の実現にとどまらず、設計と実装の統合、設計プロセスの標準化、エンジニアの設計スキル向上を果たすことを目指す。

7．採択理由

本提案は、Go言語による設計記述とモデル検証を可能にするソフトウェアを開発し、設計と実装の乖離や属人的な品質管理といったソフトウェア開発の構造的課題に対する実践的な解決策を目指すものである。設計をコードとして記述し、ソフトウェア的に検証可能にする「Design as Code」の思想により、設計の標準化・再利用性・検証性を同時に実現しようとしている。従来の形式手法の高い学習コストや特殊環境依存を、Goによる実装を用いて回避することで、現場に適用しやすくなると提案者は述べている。PoCではすでに非決定性や競合状態の検出も可能であることが示されていた。
初期的な構想自体はGoに特化しているが、将来的には他の言語による実装を用いることで、より広範な開発環境に適用が可能になると考えられる。本プロジェクトはいかにソフトウェア開発現場に浸透させるかという点も課題であるが、高い熱量をもつ提案者なら解決可能であると評価し採択とした。