Determinizm bir özellik değil, mimari ilkedir
Kayan-nokta dünyasında aynı senaryo her işlemcide farklı sonuç verir; model hatası ile arıza veya siber saldırı birbirinden ayrılamaz. Biz tüm yığını tek ilkeyle kurduk: aynı girdi → her makinede bit-aynı sonuç.
Dört katmanlı güvence
Dilde denetlenen garantiler
16 etki (saf, deterministik, sınırlı/WCET, tahsis_yok, panik_yok…) BERK dilinde makineyle denetlenir; saflık çağrı grafiğinde geçişlidir. İhlal edilen kontrat programı çalışmadan durur — berk kontrol aynı kapıyı CI için sunar.
Kapsamlı otomatik test
280+ çekirdek dil denetimi, 1.642 imzalı paket testi (BerkROS/AI/Finance/Bio/RTOS), ~1050 dijital ikiz testi ve 681 dds:: güvenlik-matematiği testi — her değişiklikte, her platformda yeniden koşar.
Formal doğrulama (TLA+)
Eşzamanlılık, kilitlenme ve zamanlama; olası tüm durumları tek tek gezen TLC model denetçisine verildi: Hard RT Core'da 18,4M durum, Berk DT'de 5,1M+ durum — sıfır ihlal.
Diferansiyel denklik kapısı
Sahaya giden .berk kaynağı ile Rust aynası ortak vektörlerle her CI koşusunda karşılaştırılır; tamsayı/mantıksal çıktılar bit-özdeş olmak zorundadır. Sapma = kırmızı test.
Float dünyasının görünmez maliyeti
| Kayan-nokta dünyası | LL BERK yaklaşımı | |
|---|---|---|
| Aynı senaryo, farklı makine | Farklı sonuç — işlemci/derleyiciye bağlı | Bit-aynı state_hash |
| Arıza vs. siber saldırı | Ayrıştırılamaz; eşikler gevşetilir | İlk karede net kırılma sinyali |
| Olay sonrası analiz | "Yeniden üretilemedi" | Tek komutla birebir replay |
| Denetim / sertifikasyon | Kanıt üretimi ayrı, pahalı iş | Hash günlükleri, replay sertifikası, sapma raporu üretimde |
| Kurcalama (tampering) | Fark edilmeyebilir | Hash zinciri anında kırılır |