形式検証によりインターネットの安全を確保するプロジェクト＜起業家：Aqua-218さんの投資募集＞

自己PR

小峯（こみね）。15歳。日本在住。
私がプログラミングを始めたのは、ちょうどChatGPT（GPT-3.5）が登場した時期だった。つまり、私にとってプログラミングとは最初からAIと一緒にやるものだった。AIをペアプログラマーとして使い、AIに教わり、AIと議論しながらコードを書く。それが私の「普通」である。
しかし、AIと日常的にコードを書く中で、ある問題に気づいた。AIはハルシネーションを起こす。見た目は正しいがバグがあるコードを、自信満々に生成する。テストを書いても、テスト自体が間違っている可能性がある。AIが生成するコードの量が増えるほど、この問題は深刻になる。
この問題に対する私の答えは、形式検証だった。テストではなく、数学的な証明によってソフトウェアの正しさを保証する。AIが書いたコードであろうと人間が書いたコードであろうと、証明が通れば正しい。証明が通らなければ正しくない。これ以上にシンプルで強力な品質保証の方法は存在しない。
形式検証の道具としてLean 4を選んだ。SPARK/Adaも検討したが実務寄りすぎた。Coq/Isabelleも検討したが汎用プログラミング言語としての能力が不足していた。Lean 4は定理証明器と実用的なプログラミング言語を兼ね備えた唯一のシステムであり、Apache 2.0ライセンスで、ネイティブコンパイルが可能で、Mathlibという巨大な数学ライブラリを持つ。
2ヶ月前に開発を開始し、現在までに以下を達成した。
・Veriwasm：WebAssembly 3.0の全520+命令のAST定義、完全な型チェッカ（GC型・recursive subtyping・polymorphic stack typing対応）、バイナリパーサの実装。Lean 4コード約5,000行、テスト273件全パス、失敗ゼロ。全てのコア関数がpartial defを排除した完全な全域関数（total functions）として実装されており、将来の定理証明に耐えうる品質を確保している。
・CryptoLib：153暗号アルゴリズムのアーキテクチャ設計、依存関係グラフの完全な定義、リファインメント鎖の設計を完了。
これらは全て、学校に通いながらほぼフルタイムで開発している成果である。
私が作っているものは、世界に存在しない。形式検証済みのWasm 3.0ランタイムは世界にゼロ。153アルゴリズムを網羅する形式検証済み暗号ライブラリも世界にゼロ。私はこれを、世界で誰もやっていない方法で、世界で最も若い年齢層から始めている。
形式検証はAIの進歩とともに主流になると確信している。AIが書くコードが増えるほど、そのコードの正しさを保証する手段の需要が増す。今この基盤を作っておかなければ、未検証のソフトウェアが世界中のインフラに定着し、後から置き換えることは指数関数的に困難になる。だから今やる。

事業計画・事業内容

形式検証済みソフトウェア基盤の開発および商用ライセンス販売事業。
本事業は、定理証明器Lean 4を用いて、数学的にバグがないことが機械証明されたミッションクリティカルソフトウェアを開発し、企業向けに商用ライセンスとして提供するものである。
現在、以下の2つのコアプロダクトを開発中。
【プロダクト1：Veriwasm — 形式検証済みWebAssembly 3.0ランタイム】
WebAssembly（Wasm）は、Cloudflare Workers、Fastly Compute、Google Sheetsなど、クラウド・エッジ・ブラウザの基盤技術として急速に普及している。2025年9月にW3C標準としてWasm 3.0が正式リリースされ、GC、例外処理、tail calls、64-bitメモリ等の機能が追加された。しかし、現存するスタンドアロンランタイム（Wasmtime、Wasmer等）はいずれも形式検証されていない。WasmCert-Isabelleが型健全性の証明を達成しているが、実用的な性能を持つランタイムではない。
Veriwasmは、Lean 4で記述され、Wasm 3.0仕様に完全準拠し、検証済みAOT（事前コンパイル）コンパイラによりネイティブコード性能を達成する、世界初の形式検証済み本番用Wasmランタイムである。x86-64、AArch64、RISC-Vの3アーキテクチャをターゲットとし、Linux、Windows、ベアメタル環境で動作する。コンパイラの各変換パスはCompCert/CakeMLスタイルの多段パイプラインで構成され、各パスの意味論保存が個別に証明される。
現在の開発状況：Wasm 3.0の全520+命令のAST定義、完全な型チェッカ（GC型・recursive subtyping・polymorphic stack typing対応）、バイナリパーサを実装済み。Lean 4コード約5,000行、テスト273件全パス。Phase 2（バイナリパーサ）を進行中。
【プロダクト2：CryptoLib — 形式検証済み暗号ライブラリ】
153の暗号アルゴリズムを網羅する、世界最大規模の形式検証済み暗号ライブラリ。SHA-2/SHA-3、AES、ChaCha20等の対称暗号から、RSA、楕円曲線（Curve25519、P-256、BLS12-381等）、そしてML-KEM、ML-DSA、SLH-DSA等のポスト量子暗号まで、現代の暗号基盤を完全にカバーする。
数学的仕様（Mathlib上の有限体・楕円曲線理論）から、安全性証明（ゲームベース証明）、純粋関数仕様、最適化仕様、Jasminアセンブリ実装まで、単一の論理体系（Lean 4 CIC）内で一本道のリファインメント鎖として構成する。サイドチャネル耐性（定数時間実行・投機的定数時間）も形式的に証明される。
既存の形式検証暗号ライブラリ（HACL*、Fiat-Crypto、EverCrypt等）はいずれもアルゴリズムのサブセットしかカバーしていない。CryptoLibは153アルゴリズムの完全な網羅と、仕様からアセンブリまでのend-to-end検証を両立する世界初のライブラリとなる。
【派生プロダクト・将来展開】
上記2プロダクトを基盤として、以下の派生プロダクトを段階的に展開する。
・形式検証済みTLS実装（CryptoLibの暗号プリミティブを使用）
・形式検証済みネットワークプロトコルスタック（OSI全レイヤーの150+プロトコル）
・匿名通信プロトコル
・Veriwasm上で動作する検証済みアプリケーション実行基盤
最終的には、CPUが実行する暗号命令からアプリケーションランタイムまで、全レイヤーが数学的に証明された世界初の完全検証済みソフトウェアスタックの実現を目指す。
【ターゲット市場・顧客】
・クラウド事業者（Cloudflare、Fastly、AWS、Google Cloud、Azure）
・金融機関（銀行、証券、暗号資産取引所）
・防衛・政府機関（CRYPTREC関連、防衛省、DARPA、NSA、NCSC）
・セキュリティ企業（Trail of Bits、NCC Group、Galois）
・半導体企業（Intel、Arm、RISC-V関連）
・通信キャリア（NTT、ソフトバンク）
・自動車（車載ソフトウェアの安全性要件）
・医療機器（FDA認証におけるソフトウェア検証要件）
形式検証済みソフトウェアは世界的に希少であり、高いプレミアム価格での提供が可能。競合が事実上存在しないブルーオーシャン市場である。

投資の内訳・起業の際の必要物

【合計：1億円】
以下、詳細な内訳を示す。
■ 開発用ハードウェア：2,500万円
本事業では、x86-64、AArch64、RISC-Vの3アーキテクチャ向けにネイティブコードを生成・検証する必要があるため、各アーキテクチャの実機が不可欠である。
(1) メイン開発・ビルドサーバ：800万円
・AMD Threadripper PRO 7995WX（96コア）ワークステーション
・メモリ512GB ECC（Lean 4の大規模証明チェックおよびMathlib並列ビルドに必要）
・NVMe SSD 8TB（高速ビルドキャッシュ）
・Lean 4のMathlibフルビルドは単体で数十分〜数時間を要し、大容量メモリと多コアCPUが証明開発の生産性に直結する
(2) ARM開発環境：500万円
・Ampere Altra Max（128コア）ARMサーバ 1台 — AArch64バックエンドのネイティブテスト・ベンチマーク用
・Apple MacBook Pro M4 Max — macOS/Apple Silicon環境でのクロスプラットフォーム開発・テスト
・Raspberry Pi 5、NVIDIA Jetson Orin等のARMボード各種 — 組み込み・エッジ環境テスト
(3) RISC-V開発環境：200万円
・StarFive VisionFive 2、SiFive HiFive Unmatched等のRISC-Vボード
・将来的なRISC-Vサーバ（市場投入時に調達）
・FPGA開発ボード（RISC-Vソフトコアでのテスト用）
(4) ネットワーク・インフラ機器：200万円
・10GbE/25GbEスイッチ、サーバラック
・UPS（無停電電源装置）
・開発環境の冗長化構成
(5) 開発用PC・周辺機器：300万円
・メイン開発用ノートPC（MacBook Pro）
・外部モニタ、キーボード等
・予備機
(6) CIサーバ・テスト環境：500万円
・専用CIサーバ（Threadripper搭載、各プッシュ時に全証明の自動チェックを実行）
・x86-64 / AArch64 / RISC-V の各アーキテクチャ向けテストランナー
・W3C公式テストスイート実行環境
・暗号アルゴリズムのテストベクトル検証環境（NIST CAVP対応）
■ 人件費：5,000万円（2年分）
(1) 主要開発者（自分）報酬：2,000万円（2年分）
・フルタイムに近い形での開発を継続するための生活費・活動費
(2) 追加開発者採用：3,000万円（2年分、1〜2名）
・形式検証またはコンパイラ開発の経験を持つ開発者の採用
・特にJasmin（検証済みアセンブリ言語）の専門家、またはLean 4/Coqの証明エンジニア
・プロジェクト規模（153暗号アルゴリズム + Wasmランタイム）を考慮すると、1人での開発には限界がある段階で追加人員が必要
■ 法人設立・法務・知財：1,000万円
(1) 法人設立費用：100万円
・株式会社設立（出資実行時）
(2) 知的財産権：500万円
・特許出願（国内+PCT国際出願）— 形式検証手法、コンパイラパイプライン、暗号実装手法等
・商標登録（Veriwasm、CryptoLib等のブランド保護）
・ソフトウェアライセンス契約書の整備（商用ライセンス、評価版ライセンス等）
(3) 法務顧問・契約書整備：400万円
・顧問弁護士（IT/知財専門）の継続契約
・海外企業との英文ライセンス契約書作成
・OSS関連ライセンスコンプライアンス確認
・輸出管理規制対応（暗号ソフトウェアのEAR/外為法対応）
■ マーケティング・営業・渡航：1,000万円（2年分）
(1) 国際カンファレンス参加・登壇：600万円
・USENIX Security、ACM CCS、IEEE S&P等のセキュリティ系トップカンファレンス
・POPL、ICFP、CPP等のプログラミング言語・形式検証系カンファレンス
・WebAssembly Summit、Wasm I/O等のWasm系カンファレンス
・渡航費・宿泊費・参加費（年6〜8回の海外渡航を想定）
(2) 営業活動：200万円
・スポンサー企業候補への営業（渡航費、資料作成費）
・デモ環境構築
・技術文書の英語ネイティブ校正
(3) Web・広報：200万円
・プロジェクトWebサイト構築・運用
・技術ブログ・ホワイトペーパー作成
・ブランディング（ロゴ、デザイン）
■ 予備費：500万円
・為替変動、機材故障、想定外の技術的課題への対応
・追加ソフトウェアライセンス（必要に応じて）
・セキュリティ監査費用（第三者による暗号実装のレビュー）

予想収益

【収益モデル：企業向け商用ライセンス（年間サブスクリプション）】
形式検証済みソフトウェアは世界的に極めて希少であり、未検証の代替品とは本質的に異なるカテゴリの製品である。数学的にバグがないことが証明されたソフトウェアに対して、企業は大きなプレミアムを支払う合理的理由がある。特に金融・防衛・医療等の領域では、ソフトウェアの欠陥が直接的に人命・資産・国家安全保障に影響するため、検証済みソフトウェアの需要は構造的に存在する。
【価格設定】
■ Veriwasm 商用ライセンス
・Standard：年額3,000万円/社（単一プロダクト利用、標準サポート）
・Enterprise：年額5,000万円〜1億円/社（全社利用、優先サポート、カスタム機能開発、SLA保証）
・価格根拠：Wasmtime/Wasmerは無償OSSだが形式検証されていない。Veriwasmは「数学的に正しいことが証明された唯一のWasm 3.0ランタイム」という独占的ポジションを持つ。クラウド事業者にとって、ランタイムの脆弱性による顧客データ漏洩・サービス停止の損害額は年間数億〜数十億円規模であり、それを排除する検証済みランタイムの年額3,000万〜1億円は十分に合理的な投資である。
■ CryptoLib 商用ライセンス
・Standard：年額2,000万円/社（全アルゴリズム利用、標準サポート）
・Enterprise：年額3,000万〜5,000万円/社（全社利用、優先サポート、カスタムアルゴリズム追加、FIPS認証支援）
・価格根拠：暗号ライブラリの脆弱性（Heartbleed等）による被害は全世界で数兆円規模に及んだ。153アルゴリズムが仕様からアセンブリまで形式検証されたライブラリは世界に存在せず、その希少性に見合うプレミアム価格が正当化される。
■ 派生プロダクト（将来）
・検証済みTLS実装ライセンス：年額1,000万〜3,000万円/社
・検証済みプロトコルスタック：年額2,000万〜5,000万円/社
・カスタム検証サービス（顧客固有の暗号プロトコルの形式検証受託）：案件あたり1,000万〜5,000万円
【収益予測（保守的シナリオ）】
■ 1年目（開発期間）：売上ゼロ
・Veriwasm MVP（Wasm 1.0コア + x86-64）完成
・CryptoLib Phase 1（共通鍵暗号、ハッシュ関数）完成
・評価版ライセンスの提供開始、スポンサー企業の獲得
■ 2年目：売上5,000万円
・Veriwasm正式リリース
・CryptoLib主要アルゴリズム完成
・初期顧客2〜3社獲得（セキュリティ企業、クラウド事業者）
■ 3年目：売上2億円
・顧客数5〜8社
・CryptoLib全153アルゴリズム完成
・TLS実装のベータ版提供開始
・防衛・金融領域への営業本格化
■ 5年目：売上10〜20億円
・顧客数20〜30社
・完全検証済みソフトウェアスタック（暗号→TLS→ランタイム）の提供
・グローバル展開（米国・欧州・アジア太平洋）
・IPOまたはM&Aの検討開始
【市場規模の参考】
・暗号ソフトウェア市場：2025年時点で約500億ドル（年率10%成長）
・WebAssemblyランタイム市場：急成長中（Cloudflare、Fastly、Fermyon等が数十億ドル規模の投資）
・形式検証サービス市場：まだ小さいが、AI普及に伴うソフトウェア品質への要求増大で急拡大が見込まれる

投資家への還元方法

【基本方針】
株式（エクイティ）による還元を基本とする。出資者には、出資額に応じた株式を発行し、事業成長に伴う企業価値の増大を通じて還元する。
【還元の具体的経路】
■ 経路1：配当
・事業が安定的な収益を生み出す段階（3年目以降を想定）で、利益の一部を配当として還元する。
・形式検証済みソフトウェアのライセンス事業は、一度完成すれば限界費用が極めて低い（追加コピーのコストがほぼゼロ）ため、高い利益率が期待できる。ソフトウェアライセンス事業の営業利益率は一般的に60〜80%であり、検証済みソフトウェアのプレミアム価格を考慮すると、さらに高い利益率が見込まれる。
■ 経路2：M&A（バイアウト）
・形式検証済みソフトウェア基盤は、大手テクノロジー企業にとって極めて高い戦略的価値を持つ。
・想定される買収候補：Cloudflare（Wasm基盤の強化）、AWS/Google Cloud/Microsoft Azure（クラウドセキュリティの差別化）、Intel/Arm（ハードウェアとの統合検証）、大手セキュリティ企業
・暗号・セキュリティ領域のM&A事例：Thales社によるnCipher買収（約100億円）、Palo Alto社による複数のセキュリティ企業買収（数百億〜数千億円規模）
・5年以内のバイアウトの場合、企業価値50〜200億円規模を想定。
■ 経路3：IPO
・形式検証済みソフトウェアのプラットフォーム企業として、独立した上場企業を目指す経路。
・日本市場（東証グロース）または米国市場（NASDAQ）への上場を検討。
・形式検証技術のAI領域への展開（AI生成コードの自動検証等）により、さらなる成長ストーリーを構築可能。
【株式条件に関する方針】
・現時点では法人未設立のため、出資実行時に株式会社を設立する。
・出資条件（バリュエーション、株式比率、優先株/普通株、希薄化防止条項等）は投資家との協議により決定する。
・創業者（小峯）の持株比率は過半数を維持する方針。技術的判断の独立性を確保するため。
・投資家に対しては、四半期ごとの開発進捗レポートおよび財務報告を提供する。
【リスクとリターンの関係】
本事業はアーリーステージの技術開発であり、高いリスクと高いリターンの双方が存在する。
リスク要因：開発の技術的難度が高い、市場がまだ成熟していない、創業者が若年であること。
リターン要因：競合が事実上ゼロ、形式検証済みソフトウェアの需要は構造的に増大、一度完成すれば極めて高い参入障壁（同等の検証を再現するには数年と数十億円が必要）。
形式検証済みソフトウェアの再現コストが極めて高いことが、本事業の最大の堀（moat）である。仮に大企業が同等のライブラリを内製しようとした場合、Lean 4の証明エンジニアリングに精通した人材の確保だけでも困難を極め、完成までに3〜5年と数十億円の投資が必要になる。この参入障壁が、先行者としての本事業の価値を長期的に保護する。

メッセージを送る