Alerus: Rust'ta Olasılıksal Programları Formel Doğrulama
Alerus, Verus tabanlı yeni bir çerçeveyle gerçek Rust kodundaki olasılıksal algoritmaları formel olarak doğruluyor; ispat Rocq'ta mekanize edildi.
Yeni bir araştırma, gerçek dünya Rust kodundaki olasılıksal (randomize) algoritmaları formel olarak doğrulamayı mümkün kılan Alerus adlı bir çerçeve sunuyor. Mevcut olasılıksal doğrulama araçları genellikle sadece akademik amaçlı idealize dillerle sınırlıydı; Alerus ise SMT tabanlı otomasyon ve separation-logic çıkarımı sunan Verus aracını temel alarak bu sınırı aşıyor.
Alerus, Eris mantığından uyarlanan 'hata kredisi' (error credit) adlı hafif bir ghost state mekanizmasıyla Verus'u genişletiyor. Bu sayede ayrık Gauss dağılımı örnekleyicileri, alias method ve fast loaded dice roller gibi gerçek örnekleme algoritmalarının doğruluğu ispatlanabiliyor.
Çerçevenin sağlamlığı, Verus'un Iris separation logic üzerinden modellendiği VerusBelt çalışmasının olasılıksal weakest precondition ile uyarlanmasıyla kanıtlanıyor; tüm ispat Rocq'ta mekanize edilmiş durumda. Bu, güvenlik kritik randomize sistem kodunun (kriptografi, örnekleme, diferansiyel gizlilik gibi) production dillerinde doğrulanabilirliğini pratik hale getiriyor.