Brown and Colbourn showed that reliability roots of connected multigraphs are dense in the unit disk and that the closure of the real roots is [-1,0] ∪ {1}. A conjecture of Brown and McMullin asks for the same results for simple graphs.

The graphs C_m[K_n] are built by substituting each edge of a cycle C_m with a complete graph K_n. Their reliability polynomial factors through the reliability and split reliability polynomials of K_n. These are analyzed asymptotically, with Rel(K_n) tending to 1 and splitRel(K_n)/q^{n-1} tending to 2 uniformly on compact subsets of the open unit disk. A general lemma on zeros of f_n + m·g_n then gives the density result. The real-root density part was formalized in Lean 4; the complex part awaits a Lean formalization of Rouché's theorem.

Reliability roots of simple graphs are dense in the unit disk, and their real roots are dense in [-1,0], confirming the Brown–McMullin conjecture. The real-root statement is machine-checked in Lean 4. The paper also leaves open whether all reliability roots of complete graphs lie inside the unit disk.