Raft konsensüs algoritması, dağıtık sistemlerde durum makinesi replikasyonunu anlaşılır bir model üzerinden gerçekleştirmek amacıyla tasarlanmıştır; ancak bu anlaşılırlık, doğruluğun hafife alınması anlamına gelmez. Raft lider seçimi, term (dönem) sayacı etrafında şekillenen bir oylama protokolüdür ve bu protokolün doğruluğu, TLA+ gibi temporal mantık araçlarıyla biçimsel olarak ifade edilebilir. Seçim süreci şu garantiler üzerine inşa edilmiştir: bir term içinde en fazla bir lider seçilebilir (election safety) ve yeterli sayıda sunucu erişilebilir durumda olduğu sürece bir lider mutlaka seçilir (liveness). Election safety garantisi, her adayın çoğunluk quorum'undan oy toplaması zorunluluğundan doğar; iki farklı aday aynı term'de eş zamanlı çoğunluk sağlayamaz çünkü kümeler kesişmek zorundadır. Formal doğrulama bağlamında Raft lider seçimi, Lamport'un TLA+ modelinde bir invariant kümesiyle temsil edilir. `LeaderCompleteness` ve `ElectionSafety` özelliklerinin model checking yoluyla doğrulanması, olası durum uzayının tamamını kapsayan exhaustive bir tarama gerektirir. Bu taramada, ağ bölünmelerinin, paket kayıplarının ve sunucu çökmelerinin etkileri ayrı ayrı simüle edilir. Önemli bir ince nokta, `RequestVote` RPC'sindeki log karşılaştırma mantığındadır. Aday, alıcının log'undan daha güncel (up-to-date) bir log'a sahip olduğunu ispat etmek zorundadır. Güncellik kriteri term bazlı, eşitlik durumunda ise indeks bazlıdır. Bu kriterin gevşetilmesi, committed entry'lerin kaybolmasına yol açan senaryolara kapı aralar; formal doğrulama araçları tam da bu tür kenar vakaları ortaya çıkarmak için kullanılır. Raft lider seçim mekanizmasının pratikte güvenli çalışması, randomized election timeout'a da bağlıdır. Timeout değerlerinin çakışması, split vote döngülerine neden olarak liveness garantisini geçici olarak kırar. TLA+ modeli bu senaryoyu fair scheduling varsayımları altında ele alır ve sonunda bir adayın çoğunluk sağlayacağını kanıtlar. Bu kanıt, sonsuz split vote döngüsünün mümkün olmadığını gösterir.
