Specula: Scaling formal specs for autonomous model checking of system code