sig
  type 'a process =
      ?valid:bool ->
      ?failed:bool ->
      ?provers:VCS.prover list ->
      ?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) -> Wpo.t -> 'a
  val prove : unit Task.task ProverScript.process
  val spawn : unit ProverScript.process
  val get : Wpo.t -> [ `None | `Proof | `Saved | `Script ]
  val save : Wpo.t -> unit
end