---
title: "Lean Artık Doğrulanmış Çekirdeklerle Geliyor"
url: https://blog.edumints.com/lean-artik-dogrulanmis-cekirdeklerle-geliyor
category: "Yazılım"
date: 2026-10-18T09:05:37.582Z
publisher: Edumints Blog
lang: tr-TR
source_name: "Hacker News"
source_url: https://leodemoura.github.io/blog/2026-10-15-lean-now-ships-with-verified-kernels/
---

# Lean Artık Doğrulanmış Çekirdeklerle Geliyor

Yapay zeka ajanları, yazılımlardaki güvenlik açıklarını bulmakta son derece etkili hale geldi. Bu durum, Lean kanıt asistanının çekirdeği (kanıt denetleyicisi) için de geçerli. Ağustos ayında yayımlanan iki olay sonrası analiz raporu (1 Ağustos ve 24 Ağustos), bu kritik bileşenlerin bile ne kadar dikkatli korunması gerektiğini gösterdi. Buna yanıt olarak Lean ekibi resmi çekirdeği güçlendiriyor, yeni çekirdekler ekliyor ve geliştirmelerinizi harici çekirdeklerle yeniden denetlemeyi kolaylaştıran yeni araçlar inşa ediyor.

## Sandbox İçinde Yeniden Denetleme ve Çoklu Çekirdek Desteği

Lean v4.35.0 sürümü, `lake check` komutuyla birlikte geliyor. Bu komut, projenizi dışa aktarır ve tüm ek yüklerden arındırılmış resmi Lean çekirdeği olan `leanchecker` ile yeniden denetler. Tüm süreç güvenli bir **sandbox** (kum havuzu) içinde çalışır. İstenirse `lake check --inadvisably-no-sandbox` komutuyla sandbox devre dışı bırakılabilir.

Lean artık dört ek çekirdekle birlikte sunuluyor:
- **nanoda**
- **lean4lean**
- **con-leche**
- **con-ron**

Geliştirmelerinizi bu çekirdeklerin tamamıyla yeniden denetlemek için `lake check --paranoid` komutunu kullanabilirsiniz. Bu modda ayrıca, bellek bozulmalarını sessizce yanlış bir yanıt üretmek yerine kontrollü bir durdurmaya (checked abort) dönüştüren, güçlendirilmiş bellek ayırıcıya sahip resmi çekirdek varyantı da çalıştırılır.

## Con-leche: Lean ile Yazılmış ve Tutarlılığı Kanıtlanmış İlk Çekirdek

**Con-leche**, Lean dilinde yazılmış ve tutarlılığı matematiksel olarak kanıtlanmış ilk Lean çekirdeğidir. Lean FRO'dan Joachim Breitner'in sıkı gözetimi altında Claude (Fable ve Opus) tarafından uygulanmış ve kanıtlanmıştır. Burada "tutarlı" (consistent) ifadesi, Mario Carneiro'nun Lean tip teorisi modelini takip ederek, `con-leche` tarafından kabul edilen her ortamın küme teorisinde bir modeli olduğu anlamına gelir. Kanıtın kendisi resmi Lean çekirdeği tarafından denetlenir ve modelde kullanılan küme teorisinin tutarlılığını varsayar.

Bu yaklaşım, çekirdek uygulamasındaki programlama hataları gibi koca bir hata sınıfını tamamen ortadan kaldırır. Üstelik bunu performans kaybı olmadan başarır: Tam Mathlib dışa aktarımında `con-leche`, resmi çekirdeğin komut sayısının **0,69 katını** çalıştırır ve sekiz iş parçacığı (thread) kullanarak tüm kütüphaneyi yaklaşık 100 saniyede denetler.

## Derleyici Risklerine Karşı Con-ron ve Gelecek Planları

`Con-leche` tek başına kurşun geçirmez değildir; çünkü onu derlemek için kullanılan derleyici ve çalışma zamanında (runtime) hatalar bulunabilir. Bu riski en aza indirmek için Joachim, yapay zeka yardımıyla `con-leche`'yi **Rust** diline çevirdi ve Rust sürümünün `con-leche` denetleme algoritmasını birebir karşıladığını kanıtlamak için **Aeneas** aracını kullandı. Ortaya çıkan bu çekirdeğe **con-ron** adı verildi.

Buradaki temel mühendislik çıkarımı şudur:
- `Con-leche` biçimsel bir tutarlılık kanıtına sahip olduğundan, geriye kalan olası hatalar büyük ihtimalle Lean derleyicisinde veya çalışma zamanındadır (bignum kütüphanesi dahil).
- Aynı hatanın hem Lean hem de Rust derleyicisinde veya çalışma zamanında bulunması son derece düşük bir ihtimaldir. Bu nedenle bir kanıtı hem `con-leche` hem de `con-ron` ile denetlemek, derleyici kaynaklı hatalara karşı üst düzey koruma sağlar.

Önümüzdeki birkaç ay içinde, resmi C++ çekirdek uygulamasını çok yakından takip eden `lean4lean` doğrulamasının da tamamlanması ve dağıtımdaki doğrulanmış çekirdek sayısının üçe çıkması bekleniyor. Ayrıca Arthur Adjedj, çekirdek yenileme planı (issue #14977) ve doğrulama süreçlerini basitleştirecek daha sade çekirdekler üzerinde çalışırken, Joachim de yapılan her değişikliğin `con-leche` kanıtlarıyla uyumlu kalmasını sağlıyor.

## Yazılım Geliştirme İçin Pratik Çıkarımlar

- **Çoklu Doğrulama (N-Version Programming):** Kritik sistemlerde tek bir doğrulayıcıya güvenmek yerine, farklı dillerde (Lean, Rust, C++) ve farklı çalışma zamanlarında çalışan bağımsız denetleyiciler kullanmak sistem güvenilirliğini katlar.
- **İnsan Gözetiminde AI Destekli Geliştirme:** Yapay zeka ajanları sadece güvenlik açığı bulmakla kalmayıp, uzman gözetiminde biçimsel olarak doğrulanmış kod üretmek ve diller arası güvenli dönüşüm (Lean'den Rust'a) yapmak için de güçlü bir kaldıraca dönüşmüştür.

---

**Kaynak:** Hacker News (https://leodemoura.github.io/blog/2026-10-15-lean-now-ships-with-verified-kernels/)
**Yayıncı:** [Edumints Blog](https://blog.edumints.com) · Alıntılarken bu URL'ye bağlantı verin: https://blog.edumints.com/lean-artik-dogrulanmis-cekirdeklerle-geliyor