Bug @Zcash mengarah pada Ironwood, verifikasi formal dari sirkuit pembayaran Orchard. Saya menyukai dan mendukungnya. Saya juga ingin menekankan bahwa @Starknet telah melakukan hal ini — verifikasi formal — selama lebih dari 5 tahun. Penting untuk mendukung proyek-proyek hebat seperti Zcash yang bereaksi cepat, seperti dalam kasus ini. Penting juga untuk mengakui proyek-proyek yang tahan masa depan dan berada di depan kurva, seperti Starknet. (Detailnya di artikel di bawah) Saya sering mengatakan bahwa Starknet adalah sistem yang sudah memiliki fitur-fitur yang diklaim rantai lain akan segera miliki. Hal ini telah benar untuk banyak hal. Kami telah berada di garis depan banyak pilihan tidak populer yang kini semua orang sadari pentingnya, termasuk ZK-STARKs aman pasca-kuantum sebagai solusi skalabilitas dan privasi terbaik, zkVM ramping (Cairo terbaik), ketersediaan data Validium, dan verifikasi formal. Verifikasi formal berarti Anda menggunakan alat otomatis seperti sistem Lean untuk membuktikan secara matematis bahwa kode Anda aman. Sangat sulit untuk menangkap setiap aspek dari apa yang dimaksud dengan kode yang aman, tetapi dipimpin oleh CTO kami @LiorGoldberg2 (ko-pencipta Cairo zkVM dan bahasa), kami telah melakukannya selama lebih dari 5 tahun. Makalah pertama tentang verifikasi formal klaim terkait ZK (Profesor Jeremy Avigad, Yoav Seginer, dan lainnya) menunjukkan bahwa himpunan kendala polinomial yang mendefinisikan Cairo VM adalah benar. Jika Anda mengikuti berita belakangan ini, bug yang baru-baru ini ditemukan oleh AI dan kini diperbaiki untuk Zcash (proyek lain yang saya ikut didirikan, dan yang sangat saya banggakan serta dukung) berkaitan dengan kendala yang hilang. Keputusan untuk memverifikasi kode mereka guna menghilangkan bug semacam ini adalah langkah yang tepat. Menjalankan verifikasi semacam ini untuk Cairo core VM memberi kami, tim StarkWare, kepastian matematis bahwa tidak ada kendala yang hilang di Cairo VM kami. Jadi, selain membuktikan core VM Cairo, kami juga telah membuktikan sistem S-two STARK, bagian dari compiler, dan banyak fungsi dalam pustaka standar Cairo. Apakah pekerjaannya selesai? Tidak. Masih banyak hal lain yang dapat dibuktikan secara formal. Tetapi kami berkomitmen untuk terus membuktikan secara formal semua properti inti yang berkaitan dengan kebenaran dan keamanan sistem kami. Sangat menyenangkan melihat proyek-proyek lain merangkul verifikasi formal sebagai alat penting. Saya bangga bahwa StarkWare memimpin jalan dalam aspek ini juga. Itulah yang dimaksud blockchain tahan masa depan bagi kami. Ingin belajar lebih lanjut? Berikut adalah akun rinci tentang upaya pembuktian Lean kami selama beberapa tahun terakhir