Tüm kodların 2 yıl içinde biçimsel doğrulamadan geçmesi bekleniyor: Robinhood CEO'su

Robinhood (HOOD) CEO'su Vlad Tenev, tüm kodların iki yıl içinde biçimsel doğrulamadan geçeceğini öngördü. Tenev, ayın 4'ünde (yerel saatle) X'te “Tüm kodlar iki yıl içinde biçimsel doğrulamadan geçecek” diye yazdı. Uygulamanın önce güvenlik açısından kritik kodlarla başlayıp kapsamının zamanla genişleyeceğini de ekledi.

İlgili paylaşım, açık paylaşım dizininde yer alıyor. Tenev uygulama sırasını açıkladı, ancak belirli bir şirketin ne zaman başlayacağını belirtmedi.

Robinhood'un resmî yönetim sayfası, Tenev'i şirketin CEO'su ve Harmonic'in kurucu ortağı ile icra kurulu başkanı olarak tanıtıyor. Tenev'in biçimsel doğrulama araçları geliştiren Harmonic ile ilişkisi, bu öngörünün bağlamını oluşturuyor.

Harmonic, 27 Ekim tarihli açıklamasında biçimsel doğrulama aracı Aristotle'ın yazılım ve donanım desteğini genişleterek C ve Verilog'u desteklemeye başladığını duyurdu. Şirket, Aristotle'ın şu anda kullanılabilir olduğunu da bildirdi. Harmonic'in resmî açıklaması

Biçimsel doğrulama, bir programa önceden tanımlanmış özelliklerin, belirli bir sistem kapsamındaki tüm olası girdiler için geçerli olduğunun matematiksel olarak kanıtlanmasıdır. Bazı çalıştırma örneklerini inceleyen testlerden farklı olarak bu yöntem, tanımlanmış kapsam içindeki özellikleri kanıtlar.

Harmonic, Aristotle'ın kodda doğrulanacak özellikleri önerdiği, geliştiricinin bunları inceleyip depoya eklediği bir iş akışı tarif ediyor. Geliştiriciler, kod her değiştiğinde doğrulamayı yeniden çalıştırabiliyor.

C doğrulaması, belirtilen gereksinimlere göre işlevlerin doğruluğunu ve tanımsız davranışların bir bölümünün bulunmadığını ele alıyor. Aristotle'ın yazılım doğrulama belgeleri, varsayılan çıktı olarak bellek güvenliği kanıtını gösteriyor.

Bellek güvenliği kanıtı, işlevi çağıran tarafın belirtilen ön koşulları karşılaması hâlinde sınır dışı okuma ve yazma, boş veya serbest bırakılmış bir işaretçinin çözümlenmesi, başlatılmamış bir değerin okunması ve işaretli tam sayı taşması gibi sorunları inceliyor. Sonuç, yalnızca belirtilen koşulları karşılayan çalıştırma kapsamı için geçerli.

Doğrulama belgeleri, her işlev için kanıtlananları ve çağıranın uyması gereken koşulları sonuçlarda gösteriyor. Harici kütüphaneler gibi doğrulanmadan davranışı varsayılan bölümler de ayrıca belirtiliyor.

Verilog tasarımlarında kontrol yolunun güvenliği ve işlemlerin devamlılığı inceleniyor; veri yolunun matematiksel özellikleri de doğrulanıyor. Bunlar, Harmonic'in Aristotle için duyurduğu biçimsel doğrulama kapsamına giriyor.

Kanıt sonucu, geliştiricinin amacını değil, belgelenmiş bir özelliği yanıtlıyor. Gereksinimler gerçek amacı doğru yansıtmıyorsa bu koşulların kanıtlanması, programın amaçlandığı gibi çalıştığı anlamına gelmiyor.

Harmonic, yapay zekâ sistemlerinin ürettiği kod miktarı arttıkça kod incelemesinin önemli bir hata noktası hâline geldiğini belirtiyor. Şirket, biçimsel doğrulamayı tanımlanmış özellikleri daha geniş bir girdi aralığında inceleme yöntemi olarak sunuyor.

Kod yazımı hızlansa bile ürünün piyasaya çıkış sürecinin aynı ölçüde hızlanmayabileceğine dair bir örnek de bulunuyor. TokenPost, daha önce Oracle'ın üretken yapay zekâyla kod yazma süresini kısalttığı, ancak test, doğrulama ve dağıtım adımlarının devam ettiği bir vakayı haberleştirmişti.

ABD'deki Sandia Ulusal Laboratuvarları tarafından yayımlanan biçimsel doğrulama çalıştayı raporu, araçların kullanılabilirliğini ve sonuçların yorumlanmasını yaygın uygulamanın önündeki zorluklar arasında saydı. Raporda, araçların yalnızca uzmanların kullanabildiği zor araçlar olarak kalabileceği uyarısı yer aldı.

Raporda, doğrulama hedefinin aracın işlem kapasitesine göre daraltıldığı örnekler de bulunuyor. Büyük ölçekli kanıtlar mevcut araçların sınırlarını aşarak iş yükünü artırabildiği için ölçeklenebilirlik de çözülmesi gereken konular arasında gösterildi.