今日の注目トピック

nested inductive typeのparameter検査漏れでFalseを受理。frontendでは防げるがkernel直送で到達し、報告1時間後に修正された
LeanFormal VerificationKernelIncident Postmortem

Leanカーネルの健全性バグは修正済み、独立チェッカーも最新版が必要

これは何?Leanは、証明項を小さな信頼済みカーネルで型検査する定理証明支援系です。

入れ子の帰納型でphantom parameterが補助型から消え、metaprogrammingから不正な宣言を直接渡すとLeanカーネルがFalseの証明を受理する実装バグが報告されました。Issue #14576はopenから1時間で修正PRが作られ、merge済みでpatch releaseも公開されています。通常のfrontendは不正項を拒否し、Leanのmeta-theoryの穴ではありません。

なぜ重要か

proof checkerの信頼境界はelaboratorの制限では代替できず、kernel自身が不正な項を拒否する必要があります。独立実装も同じ入力群による継続的な差分検査と迅速な更新がなければ、二重化だけでは十分ではありません。

読むべき人
形式手法・定理証明の利用者、compiler・kernel開発者、AI生成証明を検証する研究者
HN
114 points / 40 comments
initializeとsession IDを廃止し、各requestを自己完結化。round-robin routing、header認可、cacheが標準HTTP基盤に乗る
MCPAI AgentsProtocolAuthorization

MCP 2026-07-28はsessionを廃止し、各requestを自己完結させる

これは何?MCPは、LLMを使うagentへtoolやresourceを公開するためのopen protocolです。

MCP 2026-07-28はinitialize exchangeとMcp-Session-Idを廃止し、protocol version、client identity、capabilityを各requestへ載せるstateless coreへ移行しました。server-to-client処理はMulti Round-Trip Requests、routingはHTTP header、list結果はcache hintで扱い、authorization server mix-up対策も追加されます。Simon Willison氏は新仕様でmcp-explorer、datasette-mcp、LLM client pluginを実装し、session管理が消えた効果を確認しました。

なぜ重要か

session affinityと共有stateが消えることで、標準的なload balancer、gateway、WAFへ載せやすくなります。一方でbreaking changeなので、旧SSE transport、Roots、Sampling、Loggingを使う実装は最低12か月の移行期間内に見直しが必要です。

読むべき人
AI agent・MCP client/server開発者、platform engineer、認可とgateway運用の担当者
Bluesky
103 engagement / 4 replies
TLS 1.2のfinite-field DHとRSA鍵交換をdeprecatedへ。static RSAとephemeral DHはMUST NOTに強化された
TLSIETFCryptographyDeprecation

RFC 10015はTLS 1.2のfinite-field DHとRSA鍵交換を非推奨化

これは何?RFC 10015は、TLS 1.2とDTLS 1.2で使う鍵交換方式の推奨状態を更新するIETF Standards Track文書です。

RFC 10015はfinite-field DHとRSAのkey exchangeをdeprecatedにし、static ECDHもdiscourageします。RFC 9325の記述はstatic RSAとephemeral finite-field DHをSHOULD NOTからMUST NOTへ強化し、IANA registryの該当cipher suiteも非推奨へ更新されました。TLS 1.3は該当方式や設定を共有しないため対象外です。

なぜ重要か

TLS 1.2互換性のため残したcipher suiteが標準上の明確な廃止対象になりました。endpointとclient双方で実際のnegotiationを観測し、ECDHEまたはTLS 1.3へ移せないlegacy dependencyを特定する必要があります。

読むべき人
TLS・PKI運用者、security engineer、load balancer・embedded systemの保守担当者
HN
18 points / 1 comments
Rockwell系4,148台の59%が主要cellular carrier 3社へ集中。露出台数であり侵害確認数ではない
OT SecurityPLCCISAAttack Surface

水道PLCのinternet露出は携帯回線へ集中、Censysは侵害件数と区別して報告

これは何?Censys ARCが、CISAの水道・下水分野向け警告を受けてinternet-facing PLCの観測状況を集計した調査です。

Censysは2026-07-30時点で、Rockwell/Allen-Bradley EtherNet/IP hostを4,148台、Siemens S7-1200を4,117台観測し、前者の59%は米国の主要cellular carrier 3社に集中していました。CISAはpassword変更によるoperator lockoutやIP変更による切断を警告しています。ただしCensysの数値はexposureの観測で個別hostの侵害を示さず、Schneider Electricの2,072台もPLC限定ではありません。

なぜ重要か

OT asset inventoryが固定回線やdatacenter scanだけなら、vendorやintegratorが追加したcellular modemを見落とします。観測された露出と確認済み侵害を区別しつつ、全通信経路からの到達性を継続監査する必要があります。

読むべき人
OT・critical infrastructureのsecurity担当、network operator、asset management・incident response担当者
HN
70 points / 46 comments
JAX tracingからStableHLO、standard MLIR、LLVMへ直結。XLA runtimeなしのAOT binaryとdynamic shapeを実現する
JAXLLVMMLIRQuantum Computing

CatalystはJAXをXLAなしでMLIRからLLVMへ下ろし、standalone binaryを作る

これは何?Catalystは、量子・古典処理が混ざるPennyLane workflowをcompileするXanaduのcompilerです。

CatalystはJAXが作るStableHLOをXLAへ渡さず、standard MLIR dialectからLLVMとEnzymeへ下ろすため、量子命令のないJAX codeもstandalone AOT binaryにできます。native Python control flow、dynamic-shaped array、autodiffを扱い、外部ML runtimeを外せます。著者は標準的なdeep learningでXLAを上回るものではなく、edge、custom hardware、hybrid quantum-classical処理が主な可能性だと明記しています。

なぜ重要か

frontendのJAX tracingとbackend実行を分離したことで、量子向け投資がedgeやcustom acceleratorへ再利用できました。compiler pipelineではdomain固有処理を標準IRへ接続すると、想定外のdeployment targetを開けることを示します。

読むべき人
compiler・MLIR・JAX開発者、edge ML・custom hardware・quantum softwareの担当者
HN
6 points / 0 comments