All Posts

This Lean 4 formalization machine-checks that if AI governance requires judgment grounds to remain distinguishable, then a faithful evidence layer is structurally necessary. — - The Intuition A medical AI recommends “prioritize this drug.” Only the result is recorded. But was the decision based on blood test values, prior conditions, or a physician’s override? If that information is gone, safety verification after the fact is impossible. This Lean formalization says: the prob

一番シンプルに言うと 冷蔵薬を運ぶAIが「この道で運べ」と決めた。でも薬がダメになった。 このとき、「温度を見て決めたのか、渋滞を見て決めたのか、誰が確認したのか」が残っていなければ、原因も責任者もわからない。 だから命や安全に関わる場所では、AIの「答え」だけでなく「理由・証拠・確認者」まで一緒に残す仕組みが必要になる。 このLeanは、その仕組みが数学的に意味のある骨格を持つことを、機械検証したものです。 リポジトリ： https://github.com/GhostDriftTheory/adic-ai-assurance-lean 何を前提にしたか 前提の大枠は一つですが、その中にいくつかの構造を置いています。 「AIの動きだけを見るのではなく、その判断理由・証拠・責任記録も一緒に追える世界を考える」 具体的には次の構造を置いています。 O：AIが実際にやる操作の世界（「この道で運べ」「この薬を優先」といった判断） F：その操作に紐づく証跡のまとまり（温度センサーの値、血液検査の結果、確認した担当者など） E = ∫_O...

The Core Problem When AI is deployed in society, performance is not the only question. What conditions did the decision pass through? What evidence did it leave behind? Who can verify it afterward? The essence of AI assurance is whether we can say not “please trust us,” but “this can be checked.” Yet there is a deeper question. AI is a technology that can turn human beings into “data, scores, thresholds, and optimization targets.” Once an objective function such as “because i

問題の核心 AIが社会に実装されるとき、問われるのは性能だけではない。その判断が、どの条件を通り、何を証跡として残し、後から誰が検証できるのか。「信じてください」ではなく「確かめられます」と言えるか。これがAIアシュアランスの本質だ。しかしもっと深い問いがある。AIは、人間を「データ・スコア・閾値・最適化対象」へと変換しうる技術だ。「便利だから使う」「精度が高いから通す」という目的関数が成立した瞬間、その外にある尊厳・例外者・説明不能な痛み・未来世代が、判断構造の外へ落ちていく。核兵器とAIは同じ技術ではない。しかし両者は同じ層にある――人類が初めて、自分の存続条件を自分の技術で壊しうると自覚した層として。強い技術が人間を目的関数の中の対象へ変換し、その外にある尊厳・例外者・未来世代を判断構造の外へ落としうる、という構造的な接続がそこにある。核は都市と人間を「威力・半径・戦略効果」へ変換した。AIが人間を計算対象へ変換するとき、同じ構造が別の文脈で現れる可能性がある。 ▼リーン証明 👉 https://github.com/GhostDrift

日本企業の99.7%を占める中小企業。そのサイバーセキュリティ対策は、個社が自助努力のみで対応できる範疇を大きく超えつつある。資金や専門人材が限られる中小企業に対し、高度なゼロトラストアーキテクチャの構築・運用を求めるのは、構造的に極めて困難である。実際にSophosの調査（2025年版）では、サイバー被害の要因として「スタッフや技術・スキル不足」を挙げた企業が63%に達している。経済産業省の「サプライチェーン強化に向けたセキュリティ対策評価制度」は、中小企業が限られたリソースの中で必要な対策を判断しやすくする制度として設計されている。これは、個社の努力だけで高度な対策を完結させることの難しさを、公的制度側も前提にし始めていることを示している。では、日本の中小企業、ひいては日本の産業基盤の実効的な防衛力をいかに高べきか。 解決策の一つとして、中小企業が依存するシステムやITツールを提供する「システムベンダー」側が、致命的な破壊操作を実行前に止めるゲートを標準機能として装備することの必然性が高まっている。 ▼ADICサイバーアシュアランスのプレスリ

GhostDrift数理研究所では、金融機関向けの ADIC Cyber Assurance Demo を公開しました。 ▼デモ https://ghostdrifttheory.github.io/adic-cyber-assurance-demo/ ▼プレスリリース https://prtimes.jp/main/html/rd/p/000000003.000182721.html 何を見せるデモか このデモの主眼は、AIエージェントが出した指示を、そのまま金融システムの実行権限にしないことです。たとえば、攻撃者に操作された金融AIが、 外部口座を追加する 送金限度額を引き上げる 高額送金を実行する といった連鎖的な操作を試みた場合でも、ADIC Cyber Assurance は、実行前に証拠チェーンを検証します。証拠が揃わなければ、そのAI指示は銀行操作として実行できません。 Compromised AI Instruction -> ADIC Execution Gate -> NOT EXECUTABLE copy 普通のログ監視

Note: This article is a strategic and technical supplementary commentary on the recently published Lean 4 formal proof of the ADIC Cyber Assurance Extension by the GhostDrift Mathematical Institute. Please note that the official press release has been issued in Japanese only. You can access the Japanese press release here: [Insert Link to Japanese Press Release] Japan is a nation that has historically built global trust on its relentless commitment to the "quality of infrastr

本日公開した、GhostDrift数理研究所のADICサイバーアシュアランス拡張に関する発表が、PR TIMES配信後、朝日新聞デジタル系、産経系ニュース、時事通信社系ニュースサイト、日経コンパス等の複数媒体に掲載されました。 掲載先の一部は以下です。 日経コンパス https://www.nikkei.com/compass/content/PRTKDB000000003_000182721/preview 産経ニュース https://www.sankei.com/pressrelease/prtimes/BL5RA4CL6NIDPIRIFF5CEXYUK4/ 朝日新聞デジタル系媒体 https://www.asahi.com/and/pressrelease/16594078?msockid=0a6c6954f1ea63861acd7bfaf0c8620a 時事通信社系ニュースサイト https://www.jiji.com/jc/article?k=000000003.000182721&g=prt 今回の発表では、AI自律実行の時代にお

※本稿は、GhostDrift数理研究所が公開したADICサイバーアシュアランス拡張のLean形式証明に関するプレスリリースを踏まえた、技術・国家戦略的な補足解説記事です。日本は、食品、物流、製造、医療、インフラなど、社会を支える「基盤の品質」に強いこだわりと信頼を築いてきた国です。 AI自律実行の時代、日本が勝つ道は巨大モデルの開発競争ではなく、「安心してシステムを任せられる品質」を共通基盤として保証する「AIアシュアランス」にあります。 ▼プレスリリースはこちら https://prtimes.jp/main/html/rd/p/000000003.000182721.html 1. 巨大AI開発競争への不参加と「今そこにある危機」 米中が主導する巨大モデルの限界なき量的拡大に、日本が資金力だけで挑み続けるのは困難です。日本が狙うべきは、AIを社会システムへ安全に組み込むための「品質保証基盤」です。2026年4月、片山さつき金融担当相は日銀や3メガバンク等の金融首脳を集めた緊急会議において、高度AIによるサイバー脅威を「今そこにある危機」と表

2026年5月、Googleで「Claude Mythos ADIC」と検索したところ、GoogleのAI概要上において、ADICが「実行判断の再検証」という文脈で表示される事例を確認しました。 本記事は、この表示をもって、GoogleやAnthropicがADICを公式に評価・承認したと主張するものではありません。Google AI概要は生成AIによる検索補助機能であり、表示内容やリンクは検索条件・時点・環境によって変動します。Google自身も、AI概要やAI Modeでは表示される回答やリンクが変わり得ると説明しています。(Google サポート) それでも、今回の観測には重要な意味があります。 重要なのは、当社の記事が検索結果に表示されたこと自体ではありません。Google AI概要上で、「Claude Mythos」という高度なAIサイバーリスクの文脈に対して、ADICが「AI実行判断を後から再検証するための証拠インフラ」として意味的に接続されていた点です。 Claude Mythos Previewは、AnthropicがProjec

Extending the AI × Formal Proof Paradigm to the Post-Hoc Replayability of Autonomous Decisions 1. Introduction: Security in the AI Era Demands More Than Just "Explanations" The rapid evolution of Artificial Intelligence (AI) is fundamentally reshaping the landscape of software engineering. Today, AI models can generate code at unprecedented speeds while autonomously identifying latent vulnerabilities and edge-case bugs that often elude human reviewers. However, this rapid adv

AI×形式証明の潮流を、AI判断の再検証可能性へ拡張する 1. 導入：AI時代の安全性は「説明」だけでは足りない AI（人工知能）の進化は、ソフトウェア開発のあり方を根本から変革しつつあります。現在、AIは驚異的な速度でコードを生成し、人間が見落としていたシステムの脆弱性やバグを自律的に探索・発見する能力を持ちつつあります。 しかし、この急速な進歩は、防御側（サイバーセキュリティやシステム運用側）に対して、これまでにない速度での対応を要求しています。AIによるコード生成が加速すれば、品質管理の対象となるコード量が増え、潜在的な脆弱性を見落とすリスクも高まります。同時に、攻撃者側のAIによるバグ探索能力も向上していくと推測されるためです。 このような「AIがコードを生成し、AIが脆弱性を探す」という時代において、システムの安全性をどのように担保すべきでしょうか。 開発者が仕様を記述し、手動のテストケースに沿って「人間が安全性を説明（監査）する」という従来のアプローチだけでは、AIがもたらす速度と複雑さに対抗することは困難です。今まさに必要とされてい

Transitioning from Reactive Defense to Deterministic Execution Re-verification The emergence of Claude Mythos marks a structural shift in cybersecurity governance. The threat landscape is no longer bounded by external adversarial exploitation. Today, enterprise AI agents are increasingly deployed with authorized privileges to manipulate internal systems, autonomously deciding on access controls and exception handling. The core verification constraint is no longer merely, "Cou

防御・検知の時代から、AI実行判断を再検証する時代へ Claude Mythosの登場は、サイバー対策の論点を一段進めました。 問題は、攻撃者がAIを悪用することだけではありません。企業側のAIエージェントもまた、正規の権限を持ってシステムを操作し、アクセス許可や例外処理を自律的に判断するようになります。 そのとき問われるのは、「攻撃を検知できたか」だけではなく、「そのAI実行は、当時の条件・入力・承認に照らして、本当に許可されるべきだったのか」を後から客観的に検証できるかです。本稿では、AI時代のガバナンスに不可欠な「実行判断の再検証」と、それを支える技術「ADIC（Advanced Data Integrity by Ledger of Computation）」の核心に迫ります。 ▼ADICサイバーアシュアランス技術はこちら https://github.com/GhostDriftTheory/adic-cyber-assurance-gateway 1. Claude Mythosが示したこと：自律実行の衝撃 2026年、Anthrop

Modern cybersecurity is undergoing a massive paradigm shift. Traditional perimeter defense and continuous monitoring—which focus purely on preventing intrusion or detecting active threats—are no longer sufficient in an era of sophisticated supply chain attacks, autonomous decisions by AI agents, and a rapidly tightening global regulatory landscape. Against this backdrop, we propose "Cyber Assurance by Replayable Decision Evidence," as a novel approach applying ADIC (Advanced

現代のサイバーセキュリティは、大きな転換点を迎えています。これまで主流だった「いかに侵入を防ぐか」「いかに脅威を検知するか」という境界防御モデルや監視体制だけでは、巧妙化するサプライチェーン攻撃や、自律的に動くAIエージェントによる意思決定、さらには厳格化するグローバルな法規制に対応しきれなくなっているからです。 このような背景から、私たちは、ADIC（Advanced Data Integrity by Ledger of Computation）をサイバー領域へ適用した新たなアプローチとして、「Cyber Assurance by Replayable Decision Evidence（再実行可能な判断証拠によるサイバーアシュアランス）」を提唱します。これは、従来の防御・監視・監査に偏ってきたサイバーセキュリティのパラダイムを、AIやシステムの実行判断そのものを後から再実行・再検証できる証拠インフラへと拡張する考え方です。 ADICのサイバーアシュアランスとは、AIやシステムによる実行判断について、条件・証拠・承認・検証義務を計算台帳として

Moving from Technical Defense to Replayable and Verifiable Decisions Introduction: The Era of “Verifiability” in Cyber Assurance The paradigm of cybersecurity is undergoing a massive tectonic shift. Traditionally, the industry’s focus has been concentrated on technical defense — how to protect the perimeter and block attacks. Today, however, our attention has clearly shifted toward cyber assurance: how an organization can objectively prove, report, and verify to third parties

防御から、再検証可能な実行判断へ はじめに：サイバーアシュアランスは「検証可能性」の時代へ サイバーセキュリティのパラダイムは、大きな地殻変動を迎えています。これまで業界の関心は「いかに境界を守り、攻撃を防ぐか」という技術的防御に集中していました。しかし現在、私たちの関心は「自社のセキュリティ対策が適切であることを、いかに第三者に証明・報告・検証できるか」という、サイバーアシュアランス（確証・保証）へと明確に移り変わっています。 世界的な地政学的リスクの高まりやサプライチェーン攻撃の巧妙化、そして急速に進むAIの社会実装を背景に、各国政府や規制当局は「結果としての防御」だけでなく「プロセスの透明性と説明責任」を厳格に求めるようになりました。 ここで極めて重要なのは、現代のガバナンスが求めているのは、単なる主観的な「説明可能性（Explainability）」ではなく、「客観的な検証可能性（Verifiability）および再実行可能性（Replayability）」であるという点です。 本稿では、2026年現在におけるサイバーアシュアランスの「到

1. Introduction: AI Shifting from "Decision-Making" to "Execution" The rapid evolution of Artificial Intelligence (AI), particularly Large Language Models (LLMs) and autonomous AI agents, is fundamentally reshaping the human-system interface. Traditionally, AI has been confined to cognitive decision support—providing suggestions, generating text, or analyzing data to deliver recommendations to human operators. Today, however, AI is entering the execution pathway. It now initi

1. 導入：AIは「判断」だけでなく「実行」に近づいています 人工知能（AI）、とりわけ大規模言語モデル（LLM）や自律的AIエージェントの進展は、人間とシステムのインタフェースを大きく変容させつつあります。従来のAIの役割は、文章の生成やデータの分析といった、人間に向けた「判断の提示（示唆やレコメンデーション）」にとどまっていました。しかし現在、AIはシステムAPIの呼び出し、クラウド環境の設定、コードのデプロイ、アクセス権限の変更といった、客観的な状態遷移を伴う「実行（アクション）」の領域へと進出し始めています。 この状況下で、従来のセキュリティモデルや監査フレームワークのあり方が改めて問われています。AIがシステムに直接干渉し得る時代において検証すべきは、「AIが何を考え、何を判断したか」というプロセスだけではありません。その判断の結果として引き起こされる「システムへの操作要求が、定められた安全基準の枠内で正当に許可されたものであるか」を、事後的に検証可能にすることです。 本稿では、AIの意思決定プロセスを検証可能にする「AI...