AlphaProof Code: DeepMind, Signal’in Kriptografi Kodunu Makine Kodu Düzeyinde Doğruladı

Google DeepMind, 10 Kasım 2026’da birden fazla yapay zekâ ajanının birlikte çalıştığı biçimsel doğrulama çerçevesi AlphaProof Code’u tanıttı ve sistemin, Signal’in libsignal kütüphanesindeki birebir oturum protokolünü ARM64 (AArch64) makine kodu düzeyinde, makine tarafından denetlenen Lean ispatlarıyla yaklaşık dört haftada doğruladığını açıkladı.

Künye

Ne Doğrulandı?

DeepMind’ın blog yazısına ve çalışmanın yayımlanan çıktılarına göre doğrulanan bileşenler arasında oturum açılışındaki PQXDH el sıkışması, Double Ratchet ile kuantum sonrası SPQR’nin birleşiminden oluşan Triple Ratchet ve ML-KEM-768 bulunuyor. Kyber1024, X25519, XEdDSA, HKDF, HMAC-SHA256 ve AES-256-CBC gibi kriptografik yapı taşları da kapsamda. Kanıtlanan güvenlik özellikleri ileri gizlilik (forward secrecy), ele geçirme sonrası güvenlik, kimlik doğrulama, el sıkışma gizliliği ile mesaj gizliliği ve bütünlüğü.

Doğrulama, kaynak kod yerine derlenmiş makine kodu üzerinde yapıldı. Test düzeni libsignal-cli ile kuruldu; derleyici rustc 1.98.1, bağlama musl ile statik. Hedef mimari x86 değil, AArch64.

Sistem Nasıl Çalışıyor?

DeepMind’a göre ispatları Gemini Carbon tabanlı ajanlar üretti. Tipik bir ajan ekibi 40 ile 80 ajandan oluşuyor ve tek bir makinede 24 ile 72 saat çalışıyor. Güvenilmeyen kısmı oluşturan makine denetimli Lean ispatları altı milyon satırı aşıyor; güvenilen spesifikasyon ve anlambilim yaklaşık 26.000 satır. Bunun 7.578 satırı, 467 işlemci komutu ve 31 sistem çağrısını tanımlayan AArch64 anlambilimi.

Sistemin gerçekten hata yakalayıp yakalamadığını sınamak için daha önce düzeltilmiş iki gerçek hata, izole bir kopyaya yeniden eklendi. DeepMind’a göre iki durumda da sistem, hatalı sürümün güvensiz olduğunu gösteren makine denetimli bir ispat üretti. Şirket bu çalışmayı, yaygın kullanılan bir kriptografik protokol uygulamasının yapay zekâ ile bu derinlikte doğrulandığı ilk örnek olarak tanımlıyor; bu bir şirket değerlendirmesidir.

Biçimsel Doğrulama Nedir?

Biçimsel doğrulama, bir yazılımın belirli bir matematiksel tanıma uyduğunun ispatla gösterilmesidir. Test yalnızca denenen girdiler için güvence verirken biçimsel ispat, tanımlanan koşullar altında bütün olası durumları kapsar. Ancak ispat yalnızca yazılan spesifikasyon kadar güçlüdür: spesifikasyonda yer almayan bir davranış ispatın da dışında kalır. Bu yüzden DeepMind spesifikasyonların tamamının insan uzmanlarca incelendiğini vurguluyor. DeepMind’ın aynı hafta duyurduğu başka bir model için AlphaGenome 2 sayfamıza bakabilirsiniz.

Sınırlar

Çalışmanın kendi belirttiği sınırlar şunlar: anahtar üretimi doğrulanmadı; kriptografik yapı taşları dahil 37 rutin, davranışları sözleşme ile tanımlanarak ispatın dışında bırakıldı; iş parçacıkları, sinyaller, vDSO ve dinamik bağlama modellenmedi. Hesaplamalı model kuantum bilgisayarlı saldırganı ve çoklu cihaz kullanımını kapsamıyor. Grup mesajlaşması ise gelecek çalışma olarak bırakıldı.

Bu Sayfada Ne Yok?

• “Signal tamamen doğrulandı” ifadesi: kapsam birebir oturumlarla sınırlı, anahtar üretimi ve grup mesajlaşması dışarıda.
• AlphaProof Code aracının kendisinin yayımlanıp yayımlanmayacağı: duyuruda belirtilmemiş.
• Çıktıların lisans koşulları: doğrulanamadı.
• Lean ispatı için tek bir kesin satır sayısı: DeepMind’ın sayfaları farklı ifadeler kullandığından “altı milyonu aşkın” denmiştir.
• iOS ve Android uygulamalarının derlenmiş kodunun doğrulanması: hedef yalnızca AArch64 Linux kullanıcı modu.
• Bağımsız bir kurumun değerlendirmesi: sayfadaki nitelendirmeler DeepMind’ın açıklamasıdır.
• Bulunan hata ödülleri veya yeni güvenlik açığı: duyuruda böyle bir bilgi yok.

Sık Sorulan Sorular

AlphaProof Code nedir?

Google DeepMind’ın, yazılımın güvenlik özelliklerini Lean ispatlarıyla doğrulayan çoklu ajan tabanlı biçimsel doğrulama çerçevesidir.

Signal’in hangi kısmı doğrulandı?

libsignal v0.105.4 ve spqr v1.6.0’daki birebir oturum protokolü: PQXDH el sıkışması ve Triple Ratchet.

Doğrulama ne kadar sürdü?

DeepMind’a göre yaklaşık dört hafta.

Grup sohbetleri de doğrulandı mı?

Hayır. Grup mesajlaşması gelecek çalışma olarak bırakıldı.

İnsanlar sürece katıldı mı?

Evet. Spesifikasyonların tamamını insan uzmanlar inceledi; kodun yaklaşık yüzde 1’i insan incelemesi için işaretlendi.

Doğrulama hangi işlemci mimarisinde yapıldı?

AArch64 (ARM64) Linux kullanıcı modu makine kodunda; x86 kapsamda değil.

Kaynak ve kapsam: Bilgiler Google DeepMind’ın 10 Kasım 2026 tarihli Introducing AlphaProof Code yazısından ve çalışmanın çıktı sayfasından okunmuştur. Aracın yayım planı ve lisans bilgisi kaynaklarda bulunmadığından yazılmamıştır. Veri tarihi: 13 Kasım 2026.