Ok. Please write me an implementation of RAFT using no tests and have the Rust type checker prove correctness. I admit complete ignorance into how to get Rust to even go about partially proving that.

you cannot prove RAFT correctness using Rust type checker.

wdym by "no tests"?

seems you have not read my response at all...

> sure we need write tests, and tests like antithesis helps with.

also, imho both lamports (bft and paxos) and are better of raft https://www.hytradboi.com/2025/2016d6c4-b08d-40b3-af2f-67926...