Input Output が 9 月 4 日の週次開発レポートを公開しました。並んでいるのは、Hydra の仕様が Agda で形式化されたこと、Cardano node v.11.1.0 のベンチマークが済んでパッチ版の作業に入っていること、そして IO Research がデータ可用性のワークショップを開いたことの 3 点です。地味な週報に見えますが、前の 2 つはどちらも「動いているものを、外から確かめられる形にする」という同じ方向を向いています。SPO の手元に関わる話も含まれているので、順に見ていきます。
初期報: Hydra仕様がAgdaで形式化、Cardano node v.11.1.0ベンチマーク実施
■ 仕様書が「読み物」から「型検査を通るもの」へ
Hydra チームは、仕様書の組版を LaTeX から Typst へ移したうえで、その中身を Agda で形式化した、とレポートに書かれています。文書のフォーマットを変えた、という話ではありません。
Hydra のリポジトリにある spec/ を見ると、構成が具体的に分かります。置かれているのは .lagda.typ、つまり Typst の文章の中に Agda のコードを埋め込んだファイルです。Agda は証明支援系の言語で、書かれた定義や補題は型検査を通らなければそもそもビルドが失敗します。README の説明によれば、コードブロックは PDF に出力されるものと、表示せず型検査だけ受けるものに分かれていて、仕様の PDF は nix build .#spec で生成されます。ディレクトリには hydra-protocol.agda-lib という Agda のライブラリ定義も置かれています。
加えて今週は、Hydra ノードとバリデータの間で差分テストを入れた、とあります。リポジトリ側の説明では、仕様と実装の同期を、機械検査されたバリデータ、そこから抽出した Haskell のチェッカー、そして実際のノードの挙動に対する差分テストで保つ、という組み立てになっています。
ここが効いてくるのは、仕様と実装がずれたときです。人間が読む仕様書は、実装が先に進んでも黙って古びていきます。型検査を通る仕様と差分テストを挟むと、ずれたところでビルドかテストが落ちる。仕様書が、確認の対象から確認の道具に変わるということです。L2 の設計を外部が検証しようとしたとき、参照できるものが PDF だけなのか、型検査を通ったソースなのかは、かなり違います。
■ node 11.1.0 は CPU が下がり、メモリが増えました
もう一方はノード本体です。パフォーマンス＆トレーシングのチームが v.11.1.0 のベンチマークを行い、リリース版とプレリリース版を比較しています。
出た結果は素直に良い話ばかりではありませんでした。レポートの表現は「プロセスの CPU 使用率がはっきり下がった一方で、常駐メモリ（resident set size）が増えた」というものです。メモリ増加のほうは調査に回され、修正は v.11.1.1 のパッチリリースに入る予定だと書かれています。
測り方の側も細かくなっています。ベンチマークツール beacon に、UTxO 参照のディスクアクセス時間を捉える指標が追加されました。レポートによれば、これまで totalTime の外れ値としてまとめて見えていたものを、台帳の tick 処理にかかった時間と、テーブル読み出しにかかった時間に分解できるようになっています。後者が、オンディスクの保管先に対する UTxO 参照のコストを実際に捉えている部分です。
このほか、作図の裏側を Cairo から gnuplot に置き換えて可搬性を上げたこと、Leios 向けにオンディスク LedgerDB のトランザクション検証ベンチマーク（ディスク I/O とメモリの計測を含む）を出したこと、cardano-tracer のアラートマネージャの実装に着手したことが挙げられています。
■ SPO の手元で、同じ測り方ができるようにする
今回のレポートで SPO に直接関わるのは、この一行です。Nix もネットワーク接続も要らない、自己完結型のベンチマークパッケージを開発中で、対象は SPO のハードウェアだとされています。
意味するところははっきりしています。いまノードの性能数値は、専用の計測環境で出たものを外から読むしかありません。手元のマシンが同じ傾向を示すかどうかは、各自の体感に頼ることになります。Nix を用意しなくても走る計測パッケージが配られれば、「11.1.0 に上げたらメモリが増えた」を、自分のノードで確かめられるようになります。上の CPU とメモリの話は、まさにその種の確認が要る内容でした。
なお、このチームについては 8 月末の更新で、パフォーマンス＆トレーシングのチーム全体が IOG から ICAN Group へ移ったことが公表されています。同じ更新には、Cardano Maintenance & Support の提案に対する成果物の提供は移行期間を通じて途切れていない、と書かれています。ノードを測る役割がどこに属しているかは、SPO にとっては数値の出どころの話でもあるので、押さえておく価値はあります。
■ 3 点目のワークショップと、次に見るもの
3 点目のデータ可用性ワークショップは、Cardano Vision 26 の下での 2 回目の技術ワークショップとして開かれました。扱ったのはデータ可用性の要件、ユースケース、仕様で、Cardano Problem Statement（CPS）の準備とロードマップの議論、実装への引き継ぎが含まれています。進行は Fergie Miller 氏（director of research partnerships）と Giorgos Panagiotakos 氏（Input Output Group リサーチフェロー）です。開催予定については、SIPO でも先週の記事で扱いました。
- v.11.1.1 がいつ出るか。常駐メモリの増加は 11.1.0 を入れた環境に現に乗っているものなので、パッチの登場はそのまま運用上の判断材料になります。
- 自己完結型ベンチマークパッケージの配布形態。Nix なし・ネットワークなしという条件をどこまで満たして出てくるか。実際に手元で走らなければ、意味は半分になります。
- Hydra の仕様 PDF と Agda ソースの公開のされ方。型検査を通した仕様が、外部の実装者や監査する側からどれだけ参照しやすい形で置かれるか。
週次開発レポートは、1 週間ぶんの作業を淡々と並べる文書です。ただ今回は、仕様の側も計測の側も「外から確かめられるようにする」方向に一歩ずつ動いていました。確かめられる形が増えるほど、判断は個人の勘から離れていきます。
一次ソース / 関連リンク
- Input Output「In this week’s development report」（2026年9月4日・X）
https://x.com/IOGroup/status/2095809421184012547 - Weekly development report as of 2026-09-04（Essential Cardano）— Core technology / Scaling / Research の各節
https://www.essentialcardano.io/development-update/weekly-development-report-as-of-2026-09-04 - Performance & Tracing team update（2026年8月28日）— 11.1.0 のベンチマーク結果、11.1.1 パッチ、beacon の新指標、ICAN Group への移管
https://updates.cardano.intersectmbo.org/2026-08-28-performance-and-tracing/ - cardano-scaling/hydra リポジトリ
spec/— literate-Agda + Typst の構成と README
https://github.com/cardano-scaling/hydra/tree/master/spec - SIPO「L2 が増えるほど、データの置き場が問題になります——IOR がデータ可用性のワークショップを開き、CPS の材料を集めます」
https://sipo.tokyo/signal-20260829-366b1936/ - SIPO「Hydra のコスト表が訂正されました——最低手数料が実際より低く出ていた件と、Leios の攻撃修正」
https://sipo.tokyo/signal-20260828-85500b43/