Bir Yabancının Uzlaşma Matematiğimizi Kontrol Etmesine Nasıl İzin Veriyoruz

Bu kapsam içinde, altındaki uzlaşma güvenliği iddiasının güvene dayanması gerekmiyor. Kontrol edilebilir ve 2026-07-14'te zaten edildi: Solidus'ta çalışmayan biri protokol deposunu klonladı, tek bir komut çalıştırdı ve projenin kendi günlüklerinin gösterdiği cevabın aynısını aldı.

O yeniden üretim ve test ettiği tasarımın ardındaki kapsamlı model kontrolü bu sayfanın konusudur. İkisi de herkes tarafından çalıştırılabilir ya da okunabilir; hesap yok, bekleme listesi yok, Solidus'tan iş birliği gerekmiyor.

Kendiniz çalıştırın

Bir yabancının çoktan çalıştırdığı komut, aynen, açık protokol deposunun temiz bir klonundan:

cargo test -p solidus-exec --release --test twolane_vs_oracle randomized

Onların sonucu:

test result: ok. 1 passed; 0 failed

3 akış ve 40 blok boyunca 1,344 işlem, sıfır sapma, derlemesi yaklaşık 1m09s. Hesap oluşturulmadı, yapılandırma paylaşılmadı, yardım verilmedi; temiz bir çekim ve tek bir cargo test çağrısı.

Aşağıdaki iddia bir okurun kendi iki dakikasına değiyorsa, düşük sürtünmeli yol budur. Rust araç zincirini ve açık depoyu gerektirir; başka hiçbir şeyi değil.

Test gerçekte neyi kontrol ediyor

twolane_vs_oracle bir fark testidir. Aynı işlemlere karşı iki bağımsız yürütme yolunu çalıştırır ve çıktılarını karşılaştırır: bir hızlı şerit ve bir referans kâhini, blok blok birbirine karşı kontrol edilir. "Sıfır sapma", iki yolun da işledikleri her işlemde, koşumun tamamı boyunca anlaştığı anlamına gelir.

Bunu tam olarak belirtmeye değer, çünkü fazla söylemek kolaydır. Tek bir makinede, tek bir rastgele koşum boyunca iki uygulamanın anlaşması, o iki kod yolunun bu sefer anlaşmazlığa düşmediğini ortaya koyar: iki yolun hiçbirinde hiçbir yerde bir hata bulunmadığına dair biçimsel bir garanti değildir ve koşumun sınamadığı koşullardaki davranış hakkında kanıt da değildir. Bir fark testinin işe yaradığı şey tam olarak budur: aynı cevabı hesaplaması gereken iki şeyin gerçekten öyle yaptığına dair ucuz ve tekrarlanabilir bir kontrol; ki herhangi bir okur onu farklı bir tohumla yeniden çalıştırıp kendi bağımsız sonucunu alabilir.

Projenin aynı test koşumundan gelen kendi daha büyük koşumu, 1,000 akış ve 100 blok boyunca 2,186,046 işlem işledi; yine sıfır sapmayla. Yabancının yeniden üretimi daha küçük bir rastgele tohum kümesi kullandı, sayıların farklı olmasının sebebi budur; iki koşum da aynı açık günlüklerden (differential-large.txt) okunur ve ikisi de farklı ölçekte aynı tür kanıttır.

TLA+ sınırlı model kontrolü

DÜZELTME, 2026-08-02: bu bölüm daha önce "HotStuff türevi uzlaşma çekirdeğinin TLA+ ile biçimsel bir şartnamesi var" diyordu ve bir okur bunu haklı olarak bu ağın çalıştırdığı uzlaşma diye anlardı. Öyle değil. Depoda tam olarak bir TLA+ dosyası var ve kendi başlığı, o kasanın güvenlik ve çekirdek modüllerini yansıtarak v2 çekirdeğinin iki zincirli, ardışık görünüm taahhüt kuralını şartnamelendirdiğini söylüyor. Bugün çalışan zincir daha eski üç zincirli uygulamayı kullanıyor ve onu kapsayan hiçbir şartname yok. Aşağıdaki model kontrolü gerçektir ve dağıtılmamış bir uygulamayı kapsar. Bu bölümdeki diğer her şey yazıldığı gibi geçerlidir.

Fark testinden ayrı olarak, v2 uzlaşma çekirdeğinin TLA+ ile biçimsel bir şartnamesi vardır ve TLC ile kontrol edilmiştir. Yayımlanan sonuç: MaxView=2'de kapsamlı olarak kontrol edilmiş 963,033 durum, sıfır güvenlik ihlali. MaxView=4'te daha büyük ve kapsamlı olmayan bir benzetim koşumu 124.4 milyon durumu kapsadı; yine sıfır güvenlik ihlali bulundu.

Buna tam olarak ne olduğunu söyleyin: bir sınırlı model kontrolü, bir kanıt değil. MaxView=2, kapsamlı aramanın dikkate aldığı uzlaşma turu sayısını sabitler; o sınır içindeki her erişilebilir durum sayıldı ve güvenlik özelliğine karşı kontrol edildi, hiçbiri ihlal etmedi. Bu güçlü bir sonuçtur: protokolün her görünüm numarasında, her takvimde, sonsuza kadar güvenli olduğunun kanıtıyla aynı iddia değildir. Ayrım, bu sayfanın kontrol her gündeme geldiğinde belirtmesine yetecek kadar önemlidir: sınırlı model kontrolü, asla kanıt değil.

Şartname ve tam sonuçlar dosyası (tla+/TLC_RESULTS.md), modelledikleri kodun yanında açık depoda yaşar; o kod dağıtılmış olan değil v2 kasasıdır. Onu okumak fark testini çalıştırmaktan daha ağır bir iştir, kapsamlı kontrolü kendiniz yeniden üretmek TLC kurmak ve onu şartnameye karşı çalıştırmak demektir, ama sonuçlar dosyası okunmak için orada ve şartname, tarif ettiğini iddia ettiği uygulamaya karşı kontrol edilmek için orada.

İş hacmi sayısını dürüstçe okumak

2,186,046 işlemlik koşumu üreten differential-large günlüğü, geçerken bir iş hacmi rakamı da üretir, çünkü test tesadüfen bir tane bildirir. O günlükten ya da projenin diğer kıyaslama günlüklerinden gelen her iş hacmi sayısı tek bir Apple M4, 10 çekirdek, tek bir makinede ölçüldü; asla dağıtık bir ağda değil, asla yük altında birden fazla doğrulayıcıyla değil. O çekince burada her anıldığında sayıyla birlikte gider, çünkü tek makinelik bir rakam ile bir ağın gerçek iş hacmi farklı soruları yanıtlar ve ikisini bulanıklaştırmak, gerçekte neyin ölçüldüğünü yanlış aktarırdı. Yerine gösterilecek coğrafi olarak dağıtık ya da çok düğümlü bir rakam mevcut değil.

Bu neyi kontrol eder, neyi etmez

Bir arada, bu sayfadaki iki artefakt "Solidus'un uzlaşması doğru mu"dan daha dar bir soruyu yanıtlar. Şunu yanıtlarlar: hızlı yürütme yolu, geniş bir rastgele örneklem boyunca bir referans uygulamayla anlaşıyor mu ve uzlaşma çekirdeğinin biçimsel modeli, sınırlı sayıda tur içinde kapsamlı arama altında ayakta kalıyor mu. İki cevap da evettir, ikisi de bağımsız olarak kontrol edilebilir ve biri, sonuçta hiçbir payı olmayan biri tarafından çoktan bağımsız olarak kontrol edildi.

Tasarımın üretim ölçeğinde, düşmanca ağ koşulları altında ya da sınırsız sayıda görünüm boyunca ayakta kalıp kalmadığını yanıtlamazlar: bunlar farklı ve daha zor sorulardır ve bu sayfa aksini iddia etmiyor.

Neden önce kontrol edilecek doğru şey bu

Uzlaşma tasarımının, onu işletecek bir getiri var olmadan önce, işletilmeye değecek kadar sağlam olup olmadığına karar veren bir okur için: bu, "bu projeye güvenmeli miyim"den daha küçük ve daha yanıtlanabilir bir sorudur. Kimseye güvenmeyi gerektirmez. Fark testi ve TLA+ şartnamesi açık depodadır; fark testi doğrudan çalıştırılabilir ve şartname, Solidus'tan hiçbir şey istemeden okunabilir ve tarif ettiği koda karşı kontrol edilebilir. Bunları bir belgedeki bir iddia yerine böyle yayımlamanın amacı budur: uzlaşma matematiğini doğrulamak isteyen bir okur bunu hesapsız, izinsiz ve projenin sözüne inanmadan yapabilir.

Geri kalanı nerede yaşıyor

Bir okur buraya başka bir platformdaki teknik bir yazıdan geldiyse, bu yeniden üretimi tarif eden bir dev.to yazısı ya da bir forum başlığından: bu sayfa, tam ayrıntının ve tam komutların bundan sonra yaşayacağı yerdir. O malzemenin yeniden yazımı değil; deponun değiştikçe güncel tutulan, kanonik ve dizinlenebilir eviyidir. Bu sitedeki hiçbir şeyin görünen değeriyle alınıp alınamayacağına dair daha geniş soru için sevk edilenler-karşısında-yol haritası sayfasına; altındaki uzlaşma motorunun gerçekte neyin kimliğini doğruladığı için Proof-of-Identity sayfasına bakın.

Yukarıda kesin teknik anlamlarıyla kullanılan terimler, BFT ve kesinlik, lexicon'da uzun uzadıya tanımlanmıştır; bu sayfa onları yalnızca fark testini açıklamak için gerektiği kadar kullanır.