sig
  val prove :
    Wpo.t ->
    ?mode:VCS.mode ->
    ?start:(Wpo.t -> unit) ->
    ?callin:(Wpo.t -> VCS.prover -> unit) ->
    ?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
    VCS.prover -> bool Task.task
  val spawn :
    Wpo.t ->
    ?start:(Wpo.t -> unit) ->
    ?callin:(Wpo.t -> VCS.prover -> unit) ->
    ?callback:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
    ?success:(Wpo.t -> VCS.prover option -> unit) ->
    (VCS.mode * VCS.prover) list -> unit
end