Function election_jitter_ms 

pub fn election_jitter_ms(me: u64, epoch: u32, base_ms: u64) -> u64

Deterministic per-(node, epoch) election-timeout jitter in [0, base_ms).

This is Raft’s randomized backoff, made reproducible for the deterministic sims: the jitter is a fixed hash of the node ID and the epoch, so the same run replays the same way. The contract proves only the range, 0 for a zero base and below base_ms otherwise. It does not prove that two nodes, or two epochs of one node, get different values; the hash usually spreads them, and the unit tests pin a few spread values, but a collision is possible and nothing here rules it out.