@Zcash hatası, Orchard ödeme devresinin formel doğrulamasına yol açtı. Bu projeyi seviyorum ve destekliyorum. Ayrıca @Starknet'in bu işi — formel doğrulama — daha fazla 5 yıldır yaptığını vurgulamak istiyorum. Zcash gibi projelerin, bu durumda olduğu gibi, hızlı tepki vermesini desteklemek önemlidir. Aynı zamanda, Starknet gibi geleceğe dayanıklı ve öncü projeleri tanımak da önemlidir. (Ayrıntılar aşağıda yer alan makalede) Sık sık şunu söyledim: Starknet, diğer zincirlerin yakında yapacağını iddia ettikleri şeylere zaten sahip olan sistemdir. Bu, birçok alanda doğru oldu. Şimdi herkesin önemli olduğunu kabul ettiği, ancak önce popüler olmayan birçok seçimi biz ilk olarak yaptık: post-kuantum güvenli ZK-STARK'lar, en iyi ölçeklendirme ve gizlilik çözümü; hafif zkVM'ler (Cairo en iyisi); Validium veri erişilebilirliği ve formel doğrulama. Formel doğrulama, kodunuzun güvenli olduğunu matematiksel olarak kanıtlamak için Lean gibi otomatik araçları kullanmak anlamına gelir. Kodun güvenli olmasının her bir yönünü yakalamak çok zordur, ancak CTO'muz @LiorGoldberg2 (Cairo zkVM ve diliyle ortak kurucu) öncülüğünde, daha fazla 5 yıldır bu işi yapıyoruz. ZK ile ilgili iddiaların formel doğrulamasına dair ilk makale (Profesör Jeremy Avigad, Yoav Seginer ve diğerleri), Cairo VM'yi tanımlayan polinom kısıtlamalar kümesinin doğru olduğunu gösterdi. Son zamanlarda haberi takip edenler için, son zamanlarda AI tarafından keşfedilen ve şimdi Zcash için düzeltilen hata, eksik bir kısıtlama ile ilgiliydi. Bu tür hataları ortadan kaldırmak için kodlarını doğrulama kararı doğru bir adımdır. Cairo temel VM için bu tür bir doğrulama yapmak, StarkWare ekibine Cairo VM'mizde eksik bir kısıtlama olmadığını matematiksel olarak garanti etti. Dolayısıyla, Cairo'nun temel VM'sini kanıtlamakla kalmadık, aynı zamanda derleyicinin bir parçası olan S-two STARK sistemini ve standart Cairo kütüphanesindeki birçok fonksiyonu da kanıtladık. İş tamam mı? Hayır. Formel olarak kanıtlanabilecek çok daha birçok şey var. Ancak sistemlerimizin tutarlılık ve güvenliğiyle ilgili tüm temel özelliklerin formel olarak kanıtlanmaya devam etmeye kararlıyız. Başka projelerin formel doğrulamayı önemli bir araç olarak benimsemesini görmek harika. StarkWare'nin bu alanda da yol gösterici olduğunu söylemekten gurur duyuyorum. Bu, bize göre "geleceğe dayanıklı blok zinciri" demektir. Daha fazla bilgi edinmek istiyor musunuz? Aşağıda son birkaç yıldır Lean kanıt çabalarımızın ayrıntılı bir açıklaması yer alıyor.