Initially, validators have signed no certificates.
Theorem: signed-certs-when-init
(defthm signed-certs-when-init (implies (and (system-initp systate) (in val (correct-addresses systate))) (equal (signed-certs val systate) nil)))
