タグ: 形式検証

情報 2026年11月10日 21:13

Signal の暗号を DeepMind が形式検証、AlphaProof Code

Google DeepMind が AlphaProof Code で Signal の libsignal（PQXDH と Triple Ratchet）を Lean で形式検証。何を証明し何は対象外か、利用者への意味をまとめる。