diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli
index b67f5ff119f95e2459b676f596ed22454ac948c7..7416846996dc383940351c145ad19ab0fa18d4b0 100644
--- a/src/proto_alpha/lib_protocol/alpha_context.mli
+++ b/src/proto_alpha/lib_protocol/alpha_context.mli
@@ -2530,6 +2530,11 @@ module Sc_rollup : sig
 
   val input_request_equal : input_request -> input_request -> bool
 
+  type output = {
+    message_counter : Z.t;
+    payload : Sc_rollup_outbox_message_repr.t;
+  }
+
   module PVM : sig
     type boot_sector = string
 
@@ -2571,7 +2576,18 @@ module Sc_rollup : sig
       val verify_proof : proof -> bool Lwt.t
 
       val produce_proof :
-        context -> input option -> state -> (proof, string) result Lwt.t
+        context -> input option -> state -> (proof, error) result Lwt.t
+
+      type output_proof
+
+      val output_of_output_proof : output_proof -> output
+
+      val state_of_output_proof : output_proof -> State_hash.t
+
+      val verify_output_proof : output_proof -> bool Lwt.t
+
+      val produce_output_proof :
+        context -> state -> output -> (output_proof, error) result Lwt.t
     end
 
     type t = (module S)
@@ -2678,7 +2694,7 @@ module Sc_rollup : sig
       val get_status : state -> status Lwt.t
 
       val produce_proof :
-        context -> input option -> state -> (proof, string) result Lwt.t
+        context -> input option -> state -> (proof, error) result Lwt.t
     end
 
     module ProtocolImplementation :
@@ -2854,6 +2870,36 @@ module Sc_rollup : sig
     end
   end
 
+  module Outbox : sig
+    (** See {!Sc_rollup_outbox_message_repr}. *)
+    module Message : sig
+      type transaction = {
+        unparsed_parameters : Script.expr;
+        destination : Contract_hash.t;
+        entrypoint : Entrypoint.t;
+      }
+
+      type t = Atomic_transaction_batch of {transactions : transaction list}
+
+      val of_bytes : string -> t tzresult
+
+      module Internal_for_tests : sig
+        val to_bytes : t -> string tzresult
+      end
+    end
+
+    val record_applied_message :
+      context ->
+      t ->
+      Raw_level.t ->
+      message_index:int ->
+      (Z.t * context) tzresult Lwt.t
+  end
+
+  module Errors : sig
+    type error += Sc_rollup_does_not_exist of t
+  end
+
   module type PVM_with_proof = sig
     include PVM.S
 
@@ -2884,7 +2930,7 @@ module Sc_rollup : sig
       (module PVM_with_context_and_state) ->
       Sc_rollup_inbox_repr.t ->
       Raw_level_repr.t ->
-      (t, string) result Lwt.t
+      (t, error) result Lwt.t
   end
 
   module Game : sig
@@ -2947,7 +2993,7 @@ module Sc_rollup : sig
       State_hash.t option ->
       Tick.t ->
       (State_hash.t option * Tick.t) list ->
-      (unit, string) result Lwt.t
+      (unit, error) result Lwt.t
 
     val play : t -> refutation -> (outcome, t) Either.t Lwt.t
   end
@@ -3005,36 +3051,6 @@ module Sc_rollup : sig
 
   val get_boot_sector : context -> t -> string tzresult Lwt.t
 
-  module Outbox : sig
-    (** See {!Sc_rollup_outbox_message_repr}. *)
-    module Message : sig
-      type transaction = {
-        unparsed_parameters : Script.expr;
-        destination : Contract_hash.t;
-        entrypoint : Entrypoint.t;
-      }
-
-      type t = Atomic_transaction_batch of {transactions : transaction list}
-
-      val of_bytes : string -> t tzresult
-
-      module Internal_for_tests : sig
-        val to_bytes : t -> string tzresult
-      end
-    end
-
-    val record_applied_message :
-      context ->
-      t ->
-      Raw_level.t ->
-      message_index:int ->
-      (Z.t * context) tzresult Lwt.t
-  end
-
-  module Errors : sig
-    type error += Sc_rollup_does_not_exist of t
-  end
-
   module Internal_for_tests : sig
     val originated_sc_rollup : Origination_nonce.Internal_for_tests.t -> t
   end
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml
index b81e924a08df3a97f7984252517bc6d425c4afe1..bacfc69148a53d974c2f9d73aa0d33342488dc4f 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml
@@ -135,6 +135,26 @@ let input_request_equal a b =
       Raw_level_repr.equal l m && Z.equal n o
   | First_after _, _ -> false
 
+type output = {message_counter : Z.t; payload : Sc_rollup_outbox_message_repr.t}
+
+let output_encoding =
+  let open Data_encoding in
+  conv
+    (fun {message_counter; payload} -> (message_counter, payload))
+    (fun (message_counter, payload) -> {message_counter; payload})
+    (obj2
+       (req "message_counter" n)
+       (req "payload" Sc_rollup_outbox_message_repr.encoding))
+
+let pp_output fmt {message_counter; payload} =
+  Format.fprintf
+    fmt
+    "@[%a@;%a@;@]"
+    Z.pp_print
+    message_counter
+    Sc_rollup_outbox_message_repr.pp
+    payload
+
 module type S = sig
   (**
 
@@ -268,5 +288,27 @@ module type S = sig
         - the [context] for this instance of the PVM doesn't have access
         to enough of the [state] to build the proof. *)
   val produce_proof :
-    context -> input option -> state -> (proof, string) result Lwt.t
+    context -> input option -> state -> (proof, error) result Lwt.t
+
+  (** The following type is inhabited by the proofs that a given [output]
+      is part of the outbox of a given [state]. *)
+  type output_proof
+
+  (** [output_of_output_proof proof] returns the [output] that is
+      referred to in [proof]'s statement. *)
+  val output_of_output_proof : output_proof -> output
+
+  (** [state_of_output_proof proof] returns the [state] hash that is
+      referred to in [proof]'s statement. *)
+  val state_of_output_proof : output_proof -> hash
+
+  (** [verify_output_proof output_proof] returns [true] iff [proof] is
+      a valid witness that its [output] is part of its [state]'s outbox. *)
+  val verify_output_proof : output_proof -> bool Lwt.t
+
+  (** [produce_output_proof ctxt state output] returns a proof
+      that witnesses the fact that [output] is part of [state]'s
+      outbox. *)
+  val produce_output_proof :
+    context -> state -> output -> (output_proof, error) result Lwt.t
 end
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml
index b6ebcb4aa067f8638e874f73f1a569082cd46af4..cfd9f2389f9c3292f83c3d7bebde0ac8a7b348fe 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_arith.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.ml
@@ -335,6 +335,13 @@ module Make (Context : P) :
 
       let set k v = set_value (key k) P.encoding v
 
+      let mapped_to k v state =
+        let open Lwt_syntax in
+        let* state', _ = Monad.(run (set k v) state) in
+        let* t = Tree.find_tree state (key k)
+        and* t' = Tree.find_tree state' (key k) in
+        Lwt.return (Option.equal Tree.equal t t')
+
       let pp =
         let open Monad.Syntax in
         let* l = children [P.name] P.encoding in
@@ -630,6 +637,28 @@ module Make (Context : P) :
         | Some false -> Format.fprintf fmt "evaluation fails"
     end)
 
+    module OutputCounter = MakeVar (struct
+      type t = Z.t
+
+      let initial = Z.zero
+
+      let name = "output_counter"
+
+      let encoding = Data_encoding.z
+
+      let pp = Z.pp_print
+    end)
+
+    module Output = MakeDict (struct
+      type t = Sc_rollup_PVM_sem.output
+
+      let name = "output"
+
+      let encoding = Sc_rollup_PVM_sem.output_encoding
+
+      let pp = Sc_rollup_PVM_sem.pp_output
+    end)
+
     let pp =
       let open Monad.Syntax in
       let* status_pp = Status.pp in
@@ -640,10 +669,23 @@ module Make (Context : P) :
       let* lexer_state_pp = LexerState.pp in
       let* evaluation_result_pp = EvaluationResult.pp in
       let* vars_pp = Vars.pp in
+      let* output_pp = Output.pp in
+      let* stack = Stack.to_list in
       return @@ fun fmt () ->
       Format.fprintf
         fmt
-        "@[<v 0 >@;%a@;%a@;%a@;%a@;%a@;%a@;%a@;%a@]"
+        "@[<v 0 >@;\
+         %a@;\
+         %a@;\
+         %a@;\
+         %a@;\
+         %a@;\
+         %a@;\
+         %a@;\
+         vars : %a@;\
+         output :%a@;\
+         stack : %a@;\
+         @]"
         status_pp
         ()
         message_counter_pp
@@ -660,6 +702,10 @@ module Make (Context : P) :
         ()
         vars_pp
         ()
+        output_pp
+        ()
+        Format.(pp_print_list pp_print_int)
+        stack
   end
 
   open State
@@ -905,6 +951,21 @@ module Make (Context : P) :
         | None -> stop_parsing true
         | _ -> stop_parsing false)
 
+  let output v =
+    let open Monad.Syntax in
+    let open Sc_rollup_outbox_message_repr in
+    let* counter = OutputCounter.get in
+    let* () = OutputCounter.set (Z.succ counter) in
+    let unparsed_parameters =
+      Micheline.(Int ((), Z.of_int v) |> strip_locations)
+    in
+    let destination = Contract_hash.zero in
+    let entrypoint = Entrypoint_repr.default in
+    let transaction = {unparsed_parameters; destination; entrypoint} in
+    let payload = Atomic_transaction_batch {transactions = [transaction]} in
+    let output = Sc_rollup_PVM_sem.{message_counter = counter; payload} in
+    Output.set (Z.to_string counter) output
+
   let evaluate =
     let open Monad.Syntax in
     let* i = Code.pop in
@@ -913,7 +974,10 @@ module Make (Context : P) :
     | Some (IPush x) -> Stack.push x
     | Some (IStore x) -> (
         let* v = Stack.top in
-        match v with None -> stop_evaluating false | Some v -> Vars.set x v)
+        match v with
+        | None -> stop_evaluating false
+        | Some v ->
+            if Compare.String.(x = "out") then output v else Vars.set x v)
     | Some IAdd -> (
         let* v = Stack.pop in
         match v with
@@ -981,15 +1045,58 @@ module Make (Context : P) :
     | Some (_, request) ->
         return (PS.input_request_equal request proof.requested)
 
+  type error += Arith_proof_production_failed
+
   let produce_proof context input_given state =
-    let open Lwt_syntax in
-    let* result =
+    let open Lwt_result_syntax in
+    let*! result =
       Context.produce_proof context state (step_transition input_given)
     in
     match result with
     | Some (tree_proof, requested) ->
-        return (Result.ok {tree_proof; given = input_given; requested})
-    | None -> return (Result.error "Context.produce_proof returned None")
+        return {tree_proof; given = input_given; requested}
+    | None -> fail Arith_proof_production_failed
+
+  (* TEMPORARY: The following definitions will be extended in a future commit. *)
+
+  type output_proof = {
+    output_proof : Context.proof;
+    output_proof_state : hash;
+    output_proof_output : PS.output;
+  }
+
+  let output_of_output_proof s = s.output_proof_output
+
+  let state_of_output_proof s = s.output_proof_state
+
+  let output_key (output : PS.output) = Z.to_string output.message_counter
+
+  let has_output output tree =
+    let open Lwt_syntax in
+    let* equal = Output.mapped_to (output_key output) output tree in
+    return (tree, equal)
+
+  let verify_output_proof p =
+    let open Lwt_syntax in
+    let transition = has_output p.output_proof_output in
+    let* result = Context.verify_proof p.output_proof transition in
+    match result with None -> return false | Some _ -> return true
+
+  type error += Arith_output_proof_production_failed
+
+  type error += Arith_invalid_claim_about_outbox
+
+  let produce_output_proof context state output_proof_output =
+    let open Lwt_result_syntax in
+    let*! output_proof_state = state_hash state in
+    let*! result =
+      Context.produce_proof context state @@ has_output output_proof_output
+    in
+    match result with
+    | Some (output_proof, true) ->
+        return {output_proof; output_proof_state; output_proof_output}
+    | Some (_, false) -> fail Arith_invalid_claim_about_outbox
+    | None -> fail Arith_output_proof_production_failed
 end
 
 module ProtocolImplementation = Make (struct
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli
index 93d9afcdee827c724a968ac5f3a127446a3b21ec..dc3efc840c8dfe5cc9c4800c5887fe73809850bd 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_arith.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_arith.mli
@@ -37,8 +37,13 @@
    - a variable [a] is interpreted as storing the topmost element of the
      stack in the storage under the name "a" ;
 
+   - a variable [out] is interpreted as adding a message to the outbox
+     containing a single transaction batch with the topmost element of the
+     stack as payload, the zero contract as destination, and a default
+     entrypoint ;
+
    - a symbol [+] pops two integers [x] and [y] and pushes [x + y] on
-   the stack.
+     the stack ;
 
    If a message is not syntactically correct or does not evaluate
    correctly, the machine stops its evaluation and waits for the next
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml
index 6478fd03e4149a4266c6fb37388beaeb61ed785b..5381bfbd8195865e526674c2fd2f1a526ca56c4c 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.ml
@@ -325,6 +325,12 @@ let outcome_encoding =
     (fun (loser, reason) -> {loser; reason})
     (obj2 (req "loser" player_encoding) (req "reason" reason_encoding))
 
+type error += Game_error of string
+
+let game_error reason =
+  let open Lwt_result_syntax in
+  fail (Game_error reason)
+
 let find_choice game tick =
   let open Lwt_result_syntax in
   let rec traverse states =
@@ -333,16 +339,16 @@ let find_choice game tick =
         if Sc_rollup_tick_repr.(tick = state_tick) then
           return (state, tick, next_state, next_tick)
         else traverse ((next_state, next_tick) :: others)
-    | _ -> fail "This choice was not proposed"
+    | _ -> game_error "This choice was not proposed"
   in
   traverse game.dissection
 
 let check pred reason =
   let open Lwt_result_syntax in
-  if pred then return () else fail reason
+  if pred then return () else game_error reason
 
 let check_dissection start start_tick stop stop_tick dissection =
-  let open Lwt_result_syntax in
+  let open Lwt_tzresult_syntax in
   let len = Z.of_int @@ List.length dissection in
   let dist = Sc_rollup_tick_repr.distance start_tick stop_tick in
   let should_be_equal_to what =
@@ -353,7 +359,9 @@ let check_dissection start start_tick stop stop_tick dissection =
       check Z.(equal len (of_int 32)) (should_be_equal_to (Z.of_int 32))
     else if Z.(gt dist one) then
       check Z.(equal len (succ dist)) (should_be_equal_to Z.(succ dist))
-    else fail (Format.asprintf "Cannot have a dissection of only one section")
+    else
+      game_error
+        (Format.asprintf "Cannot have a dissection of only one section")
   in
   let* _ =
     match (List.hd dissection, List.last_opt dissection) with
@@ -394,16 +402,16 @@ let check_dissection start start_tick stop stop_tick dissection =
                b_tick
                pp
                stop_tick))
-    | _ -> fail "Dissection should contain at least 2 elements"
+    | _ -> game_error "Dissection should contain at least 2 elements"
   in
   let rec traverse states =
     match states with
     | (None, _) :: (Some _, _) :: _ ->
-        fail "Cannot return to a Some state after being at a None state"
+        game_error "Cannot return to a Some state after being at a None state"
     | (_, tick) :: (next_state, next_tick) :: others ->
         if Sc_rollup_tick_repr.(tick < next_tick) then
           traverse ((next_state, next_tick) :: others)
-        else fail "Ticks should only increase in dissection"
+        else game_error "Ticks should only increase in dissection"
     | _ -> return ()
   in
   traverse dissection
@@ -450,8 +458,8 @@ let check_proof_start_stop start start_tick stop stop_tick proof =
        stop_proof)
 
 let play game refutation =
-  let result =
-    let open Lwt_result_syntax in
+  let open Lwt_result_syntax in
+  let*! result =
     let* start, start_tick, stop, stop_tick =
       find_choice game refutation.choice
     in
@@ -467,24 +475,20 @@ let play game refutation =
                pvm_name = game.pvm_name;
                dissection = states;
              })
-    | Proof proof -> (
+    | Proof proof ->
         let* _ = check_proof_start_stop start start_tick stop stop_tick proof in
         let {inbox_snapshot; level; pvm_name; _} = game in
-        let*! proof_valid =
+        let* proof_valid =
           Sc_rollup_proof_repr.valid inbox_snapshot level ~pvm_name proof
         in
-        match proof_valid with
-        | Error s ->
-            fail (Format.asprintf "Invalid proof: %s" s) (* Illformed? *)
-        | Ok proof_valid ->
-            let* _ = check proof_valid "Invalid proof" in
-            return
-              (Either.Left
-                 {loser = opponent game.turn; reason = Conflict_resolved}))
+        let* _ = check proof_valid "Invalid proof" in
+        return
+          (Either.Left {loser = opponent game.turn; reason = Conflict_resolved})
+  in
+  let game_over reason =
+    Either.Left {loser = game.turn; reason = Invalid_move reason}
   in
-  Lwt.map
-    (fun r ->
-      match r with
-      | Ok x -> x
-      | Error e -> Either.Left {loser = game.turn; reason = Invalid_move e})
-    result
+  match result with
+  | Ok x -> Lwt.return x
+  | Error (Game_error e) -> Lwt.return @@ game_over e
+  | Error _ -> Lwt.return @@ game_over "undefined"
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli
index 1da29f1ba2d3458b03546ca096e4984792a325c7..2df0a7415e130f55c484788da37b486eee7d46b7 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_game_repr.mli
@@ -293,7 +293,7 @@ val find_choice :
     * Sc_rollup_tick_repr.t
     * Sc_rollup_repr.State_hash.t option
     * Sc_rollup_tick_repr.t,
-    string )
+    error )
   result
   Lwt.t
 
@@ -320,7 +320,7 @@ val check_dissection :
   Sc_rollup_repr.State_hash.t option ->
   Sc_rollup_tick_repr.t ->
   (Sc_rollup_repr.State_hash.t option * Sc_rollup_tick_repr.t) list ->
-  (unit, string) result Lwt.t
+  (unit, error) result Lwt.t
 
 (** Applies the move [refutation] to the game. Checks the move is
     valid and returns an [Invalid_move] outcome if not.
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.ml
index 52b6ded2b30e739c9e6a358efa95cf91fba70ff7..733fafcc6c01f0cc04372f217248067c3d9bd2ce 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.ml
@@ -800,8 +800,16 @@ module Proof = struct
     | `Node h -> Hash.(equal (of_context_hash h) hash)
     | `Value h -> Hash.(equal (of_context_hash h) hash)
 
-  let drop_error result reason =
-    Lwt.map (Result.map_error (fun _ -> reason)) result
+  type error += Inbox_proof_error of string
+
+  let proof_error reason =
+    let open Lwt_result_syntax in
+    fail (Inbox_proof_error reason)
+
+  let drop_error promise reason =
+    let open Lwt_tzresult_syntax in
+    let*! result = promise in
+    match result with Ok r -> return r | Error _ -> proof_error reason
 
   let rec valid (l, n) inbox proof =
     assert (Z.(geq n zero)) ;
@@ -825,20 +833,20 @@ module Proof = struct
           match payload with
           | None ->
               if equal proof.level inbox then return None
-              else fail "payload is None, inbox proof.level not top"
+              else proof_error "payload is None, inbox proof.level not top"
           | Some msg ->
               return
               @@ Some
                    Sc_rollup_PVM_sem.
                      {inbox_level = l; message_counter = n; payload = msg}
-        else fail "Inbox proof parameters don't match (message level)"
+        else proof_error "Inbox proof parameters don't match (message level)"
     | Some (level, inc, remaining_proof) ->
         if
           verify_inclusion_proof inc level (bottom_level remaining_proof)
           && Raw_level_repr.equal (inbox_level level) l
           && Z.equal level.message_counter n
         then valid (Raw_level_repr.succ l, Z.zero) inbox remaining_proof
-        else fail "Inbox proof parameters don't match (lower level)"
+        else proof_error "Inbox proof parameters don't match (lower level)"
 
   (* TODO #2997 This needs to be implemented when the inbox structure is
      improved. *)
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.mli
index 8bcabf3e1195bf492988c015077c68a0005d40a1..6aba77b97fdf5075b0f8a5f883ece52cbba83b46 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_inbox_repr.mli
@@ -357,7 +357,7 @@ module Proof : sig
     Raw_level_repr.t * Z.t ->
     inbox ->
     t ->
-    (Sc_rollup_PVM_sem.input option, string) result Lwt.t
+    (Sc_rollup_PVM_sem.input option, error) result Lwt.t
 
   (** TODO #2997 Currently a placeholder, needs implementation.
 
@@ -368,5 +368,5 @@ module Proof : sig
   val produce_proof :
     inbox ->
     Raw_level_repr.t * Z.t ->
-    (t * Sc_rollup_PVM_sem.input option, string) result Lwt.t
+    (t * Sc_rollup_PVM_sem.input option, error) result Lwt.t
 end
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_outbox_message_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_outbox_message_repr.ml
index 4d51e8bc4f56f15cbaec4d6df14013d6e3bded91..f3b3e8ef3dd4c9a33a36d63b9b57f7a17a1a6031 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_outbox_message_repr.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_outbox_message_repr.ml
@@ -85,6 +85,22 @@ let encoding =
     (fun transactions -> Atomic_transaction_batch {transactions})
     (obj1 (req "transactions" (list transaction_encoding)))
 
+let pp_transaction fmt {destination; entrypoint; unparsed_parameters = _} =
+  Format.fprintf
+    fmt
+    "@[%a@;%a@]"
+    Contract_hash.pp
+    destination
+    Entrypoint_repr.pp
+    entrypoint
+
+let pp fmt (Atomic_transaction_batch {transactions}) =
+  Format.pp_print_list
+    ~pp_sep:Format.pp_print_space
+    pp_transaction
+    fmt
+    transactions
+
 let of_bytes bytes =
   let open Tzresult_syntax in
   match Data_encoding.Binary.of_string_opt encoding bytes with
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_outbox_message_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_outbox_message_repr.mli
index 43d1f4b91479cf5ab238b778c2e17c284c9ae836..f7de49497640f022cf404b9173afe232629940b7 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_outbox_message_repr.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_outbox_message_repr.mli
@@ -45,6 +45,10 @@ type transaction = {
 (** A type representing messages from Layer 2 to Layer 1. *)
 type t = Atomic_transaction_batch of {transactions : transaction list}
 
+val encoding : t Data_encoding.t
+
+val pp : Format.formatter -> t -> unit
+
 (** [of_bytes ctxt bs] decodes an outbox message value from the
     given bytes [bs]. The function involves parsing Micheline expressions to
     typed values. *)
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.ml b/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.ml
index 1af051287343b078737f511340a06940c3bfa866..074de5883e5640bc0a1621f71a6ed5ea7281c849 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.ml
@@ -59,9 +59,15 @@ let cut_at_level level input =
   let input_level = Sc_rollup_PVM_sem.(input.inbox_level) in
   if Raw_level_repr.(level <= input_level) then None else Some input
 
+type error += Sc_rollup_proof_check of string
+
+let proof_error reason =
+  let open Lwt_result_syntax in
+  fail (Sc_rollup_proof_check reason)
+
 let check p reason =
   let open Lwt_result_syntax in
-  if p then return () else fail reason
+  if p then return () else proof_error reason
 
 let valid snapshot commit_level ~pvm_name proof =
   let (module P) = Sc_rollups.wrapped_proof_module proof.pvm_step in
@@ -83,7 +89,7 @@ let valid snapshot commit_level ~pvm_name proof =
           snapshot
           inbox_proof
     | _ ->
-        fail
+        proof_error
           (Format.asprintf
              "input_requested is %a, inbox proof is %a"
              Sc_rollup_PVM_sem.pp_input_request
@@ -109,10 +115,12 @@ module type PVM_with_context_and_state = sig
   val state : state
 end
 
+type error += Proof_cannot_be_wrapped
+
 let produce pvm_and_state inbox commit_level =
   let open Lwt_result_syntax in
   let (module P : PVM_with_context_and_state) = pvm_and_state in
-  let* request = Lwt.map Result.ok (P.is_input_state P.state) in
+  let*! request = P.is_input_state P.state in
   let* inbox, input_given =
     match request with
     | Sc_rollup_PVM_sem.No_input_required -> return (None, None)
@@ -136,4 +144,4 @@ let produce pvm_and_state inbox commit_level =
   end in
   match Sc_rollups.wrap_proof (module P_with_proof) with
   | Some pvm_step -> return {pvm_step; inbox}
-  | None -> fail "Could not wrap proof"
+  | None -> fail Proof_cannot_be_wrapped
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.mli b/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.mli
index 4cf611d4ec0e1e7c00d1b9ea7d2f260bd8433b9a..bf87644baad239e5aa75cd645f086861442c6e23 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.mli
+++ b/src/proto_alpha/lib_protocol/sc_rollup_proof_repr.mli
@@ -26,18 +26,18 @@
 
 (** A refutation game proof is required as part of the final move in a
     game.
-    
+
     This proof is basically a combination of a PVM proof (provided by
     each implementation of the PVM signature) and an inbox proof. To
     check the proof we must check each part separately and then also
     check that they match on the two points where they touch:
-      
+
       - the [input_requested] of the PVM proof should match the starting
-      point of the inbox proof ; 
-      
+      point of the inbox proof ;
+
       - the [input_given] of the PVM proof should match the output
       message of the inbox proof.
-    
+
     It is also often the case that the PVM proof has [No_input_required]
     for its [input_requested] and [None] for its [input_given]. If this
     is the case, we don't need the inbox proof at all and the [inbox]
@@ -77,16 +77,16 @@ val start : t -> State_hash.t
 val stop : t -> State_hash.t option
 
 (** Check the validity of a proof.
-    
+
     This function requires a few bits of data (available from the
     refutation game record in the storage):
-      
+
       - a snapshot of the inbox, used by the [inbox] proof ;
-      
+
       - the inbox level of the commitment, used to determine if an
       output from the [inbox] proof is too recent to be allowed into the
       PVM proof ;
-      
+
       - the [pvm_name], used to check that the proof given has the right
       PVM kind. *)
 val valid :
@@ -94,7 +94,7 @@ val valid :
   Raw_level_repr.t ->
   pvm_name:string ->
   t ->
-  (bool, string) result Lwt.t
+  (bool, error) result Lwt.t
 
 module type PVM_with_context_and_state = sig
   include Sc_rollups.PVM.S
@@ -122,4 +122,4 @@ val produce :
   (module PVM_with_context_and_state) ->
   Sc_rollup_inbox_repr.t ->
   Raw_level_repr.t ->
-  (t, string) result Lwt.t
+  (t, error) result Lwt.t
diff --git a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml
index 15e55c241dcd1c6091c8c824a59f5d7f3f5f84ed..21fa930d03b94a9f88b53c9d6eeb8f882e87fd65 100644
--- a/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml
+++ b/src/proto_alpha/lib_protocol/sc_rollup_wasm.ml
@@ -421,15 +421,37 @@ module V2_0_0 = struct
       | Some (_, request) ->
           return (PS.input_request_equal request proof.requested)
 
+    type error += WASM_proof_production_failed
+
     let produce_proof context input_given state =
-      let open Lwt_syntax in
-      let* result =
+      let open Lwt_result_syntax in
+      let*! result =
         Context.produce_proof context state (step_transition input_given)
       in
       match result with
       | Some (tree_proof, requested) ->
-          return (Result.ok {tree_proof; given = input_given; requested})
-      | None -> return (Result.error "Context.produce_proof returned None")
+          return {tree_proof; given = input_given; requested}
+      | None -> fail WASM_proof_production_failed
+
+    type output_proof = {
+      output_proof_state : hash;
+      output_proof_output : PS.output;
+    }
+
+    (* FIXME: #3176
+       The WASM PVM must provide an implementation for these
+       proofs. These are likely to be similar to the proofs about the
+       PVM execution steps. *)
+    let output_of_output_proof s = s.output_proof_output
+
+    let state_of_output_proof s = s.output_proof_state
+
+    let verify_output_proof _proof = Lwt.return true
+
+    let produce_output_proof _context state output_proof_output =
+      let open Lwt_result_syntax in
+      let*! output_proof_state = state_hash state in
+      return {output_proof_state; output_proof_output}
   end
 
   module ProtocolImplementation = Make (struct
diff --git a/src/proto_alpha/lib_protocol/test/integration/test_sc_rollup_wasm.ml b/src/proto_alpha/lib_protocol/test/integration/test_sc_rollup_wasm.ml
index e1abcf782286338e23e79719d3fb9b0e2c19dc92..b4894197adb444692bf4693123f2ff0295e55c5c 100644
--- a/src/proto_alpha/lib_protocol/test/integration/test_sc_rollup_wasm.ml
+++ b/src/proto_alpha/lib_protocol/test/integration/test_sc_rollup_wasm.ml
@@ -119,6 +119,7 @@ let should_boot () =
   | Ok proof ->
       let*! is_correct = Verifier.verify_proof proof in
       if is_correct then return_unit else Stdlib.failwith "incorrect proof"
-  | Error err -> Stdlib.failwith ("Could not produce a proof " ^ err)
+  | Error err ->
+      failwith "Could not produce a proof %a" Environment.Error_monad.pp err
 
 let tests = [Tztest.tztest "should boot" `Quick should_boot]
diff --git a/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml b/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml
index 48c18821066178a12da115ed083ab43e24b2b7cf..91927e3f6a91fd4f86d478a399263b94e0c2aa6a 100644
--- a/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml
+++ b/src/proto_alpha/lib_protocol/test/pbt/test_refutation_game.ml
@@ -257,8 +257,21 @@ end) : TestPVM with type state = int = struct
 
   let verify_proof proof = return proof.valid
 
-  let produce_proof _ _ _ =
-    return (Result.error "Dummy PVM can't produce proof")
+  let produce_proof _ _ _ = Stdlib.failwith "Dummy PVM can't produce proof"
+
+  type output_proof = unit
+
+  let state_of_output_proof _ =
+    Stdlib.failwith "Dummy PVM can't handle output proof"
+
+  let output_of_output_proof _ =
+    Stdlib.failwith "Dummy PVM can't handle output proof"
+
+  let verify_output_proof _ =
+    Stdlib.failwith "Dummy PVM can't handle output proof"
+
+  let produce_output_proof _ _ _ =
+    Stdlib.failwith "Dummy PVM can't handle output proof"
 end
 
 (** This is a random PVM. Its state is a pair of a string and a
@@ -327,8 +340,21 @@ end) : TestPVM with type state = string * int list = struct
 
   let verify_proof proof = return proof.valid
 
-  let produce_proof _ _ _ =
-    return (Result.error "Dummy PVM can't produce proof")
+  let produce_proof _ _ _ = Stdlib.failwith "Dummy PVM can't produce proof"
+
+  type output_proof = unit
+
+  let state_of_output_proof _ =
+    Stdlib.failwith "Dummy PVM can't handle output proof"
+
+  let output_of_output_proof _ =
+    Stdlib.failwith "Dummy PVM can't handle output proof"
+
+  let verify_output_proof _ =
+    Stdlib.failwith "Dummy PVM can't handle output proof"
+
+  let produce_output_proof _ _ _ =
+    Stdlib.failwith "Dummy PVM can't handle output proof"
 end
 
 module ContextPVM = ArithPVM.Make (struct
diff --git a/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_arith.ml b/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_arith.ml
index 55f10e356a9dff9dae4ad5f12893c910a6ac156c..93e740354e74892ec1118db7af0d5199ba8e2230 100644
--- a/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_arith.ml
+++ b/src/proto_alpha/lib_protocol/test/unit/test_sc_rollup_arith.ml
@@ -32,14 +32,78 @@
 *)
 
 open Protocol
-open Sc_rollup_arith.ProtocolImplementation
+module Context_binary = Tezos_context_memory.Context_binary
 
-let create_context () =
-  Context.init1 () >>=? fun (block, _contract) -> return block.context
+(* We first instantiate an arithmetic PVM capable of generating proofs. *)
+module Tree :
+  Protocol.Environment.Context.TREE
+    with type t = Context_binary.t
+     and type tree = Context_binary.tree
+     and type key = string list
+     and type value = bytes = struct
+  type t = Context_binary.t
+
+  type tree = Context_binary.tree
+
+  type key = Context_binary.key
+
+  type value = Context_binary.value
+
+  include Context_binary.Tree
+end
+
+module Arith_Context = struct
+  module Tree = Tree
+
+  type tree = Tree.tree
+
+  type proof = Context_binary.Proof.tree Context_binary.Proof.t
+
+  let proof_encoding =
+    Tezos_context_helpers.Merkle_proof_encoding.V2.Tree2.tree_proof_encoding
+
+  let kinded_hash_to_state_hash = function
+    | `Value hash | `Node hash ->
+        Sc_rollup_repr.State_hash.hash_bytes [Context_hash.to_bytes hash]
+
+  let proof_before proof =
+    kinded_hash_to_state_hash proof.Context_binary.Proof.before
+
+  let proof_after proof =
+    kinded_hash_to_state_hash proof.Context_binary.Proof.after
+
+  let produce_proof context tree step =
+    let open Lwt_syntax in
+    (* FIXME: With on-disk context, we cannot commit the empty
+       context. Is it also true in our case? *)
+    let* context = Context_binary.add_tree context [] tree in
+    let* _hash = Context_binary.commit ~time:Time.Protocol.epoch context in
+    let index = Context_binary.index context in
+    match Context_binary.Tree.kinded_key tree with
+    | Some k ->
+        let* p = Context_binary.produce_tree_proof index k step in
+        return (Some p)
+    | None -> return None
+
+  let verify_proof proof step =
+    let open Lwt_syntax in
+    let* result = Context_binary.verify_tree_proof proof step in
+    match result with
+    | Ok v -> return (Some v)
+    | Error _ ->
+        (* We skip the error analysis here since proof verification is not a
+           job for the rollup node. *)
+        return None
+end
+
+module FullArithPVM = Sc_rollup_arith.Make (Arith_Context)
+open FullArithPVM
 
 let setup boot_sector f =
-  create_context () >>=? fun ctxt ->
-  initial_state ctxt boot_sector >>= fun state -> f state
+  let open Lwt_syntax in
+  let ctxt = Context_binary.empty in
+  let* state = initial_state ctxt boot_sector in
+  f ctxt state
 
 let pre_boot boot_sector f =
   parse_boot_sector boot_sector |> function
@@ -49,13 +113,14 @@ let pre_boot boot_sector f =
 let test_preboot () =
   [""; "1"; "1 2 +"]
   |> List.iter_es (fun boot_sector ->
-         pre_boot boot_sector @@ fun _state -> return ())
+         pre_boot boot_sector @@ fun _ctxt _state -> return ())
 
-let boot boot_sector f = pre_boot boot_sector @@ fun state -> eval state >>= f
+let boot boot_sector f =
+  pre_boot boot_sector @@ fun ctxt state -> eval state >>= f ctxt
 
 let test_boot () =
   let open Sc_rollup_PVM_sem in
-  boot "" @@ fun state ->
+  boot "" @@ fun _ctxt state ->
   is_input_state state >>= function
   | Initial -> return ()
   | First_after _ ->
@@ -66,7 +131,7 @@ let test_boot () =
 
 let test_input_message () =
   let open Sc_rollup_PVM_sem in
-  boot "" @@ fun state ->
+  boot "" @@ fun _ctxt state ->
   let input =
     {
       inbox_level = Raw_level_repr.root;
@@ -97,7 +162,7 @@ let go ~max_steps target_status state =
 
 let test_parsing_message ~valid (source, expected_code) =
   let open Sc_rollup_PVM_sem in
-  boot "" @@ fun state ->
+  boot "" @@ fun _ctxt state ->
   let input =
     {
       inbox_level = Raw_level_repr.root;
@@ -165,7 +230,7 @@ let test_parsing_messages () =
 let test_evaluation_message ~valid
     (boot_sector, source, expected_stack, expected_vars) =
   let open Sc_rollup_PVM_sem in
-  boot boot_sector @@ fun state ->
+  boot boot_sector @@ fun _ctxt state ->
   let input =
     {
       inbox_level = Raw_level_repr.root;
@@ -237,6 +302,81 @@ let test_evaluation_messages () =
   >>=? fun () ->
   List.iter_es (test_evaluation_message ~valid:false) invalid_messages
 
+let test_output_messages_proofs ~valid (source, expected_outputs) =
+  let open Lwt_result_syntax in
+  let open Sc_rollup_PVM_sem in
+  boot "" @@ fun ctxt state ->
+  let input =
+    {
+      inbox_level = Raw_level_repr.root;
+      message_counter = Z.zero;
+      payload = source;
+    }
+  in
+  let*! state = set_input input state in
+  let*! state = eval state in
+  let* state = go ~max_steps:10000 WaitingForInputMessage state in
+  let check_output output =
+    let*! result = produce_output_proof ctxt state output in
+    if valid then
+      match result with
+      | Ok proof ->
+          let*! valid = verify_output_proof proof in
+          fail_unless valid (Exn (Failure "An output proof is not valid."))
+      | Error _ -> failwith "Error during proof generation"
+    else
+      match result with
+      | Ok proof ->
+          let*! proof_is_valid = verify_output_proof proof in
+          fail_when
+            proof_is_valid
+            (Exn (Failure "A wrong output proof is valid."))
+      | Error _ -> return ()
+  in
+  List.iter_es check_output expected_outputs
+
+let make_output ~counter n =
+  let open Sc_rollup_outbox_message_repr in
+  let unparsed_parameters =
+    Micheline.(Int (dummy_location, Z.of_int n) |> strip_locations)
+  in
+  let destination = Contract_hash.zero in
+  let entrypoint = Entrypoint_repr.default in
+  let transaction = {unparsed_parameters; destination; entrypoint} in
+  let transactions = [transaction] in
+  let message_counter = Z.of_int counter
+  and payload = Atomic_transaction_batch {transactions} in
+  Sc_rollup_PVM_sem.{message_counter; payload}
+
+let test_valid_output_messages () =
+  [
+    ("1", []);
+    ("1 out", [make_output ~counter:0 1]);
+    ("1 out 2 out", [make_output ~counter:0 1; make_output ~counter:1 2]);
+    ("1 out 1 1 + out", [make_output ~counter:0 1; make_output ~counter:1 2]);
+    ( "1 out 1 1 + out out",
+      [
+        make_output ~counter:0 1;
+        make_output ~counter:1 2;
+        make_output ~counter:2 2;
+      ] );
+  ]
+  |> List.iter_es (test_output_messages_proofs ~valid:true)
+
+let test_invalid_output_messages () =
+  [
+    ("1", [make_output ~counter:0 1]);
+    ("1 out", [make_output ~counter:1 1]);
+    ("1 out 1 1 + out", [make_output ~counter:0 1; make_output ~counter:3 2]);
+    ( "1 out 1 1 + out out",
+      [
+        make_output ~counter:0 1;
+        make_output ~counter:1 2;
+        make_output ~counter:2 3;
+      ] );
+  ]
+  |> List.iter_es (test_output_messages_proofs ~valid:false)
+
 let tests =
   [
     Tztest.tztest "PreBoot" `Quick test_preboot;
@@ -244,4 +384,6 @@ let tests =
     Tztest.tztest "Input message" `Quick test_input_message;
     Tztest.tztest "Parsing message" `Quick test_parsing_messages;
     Tztest.tztest "Evaluating message" `Quick test_evaluation_messages;
+    Tztest.tztest "Valid output messages" `Quick test_valid_output_messages;
+    Tztest.tztest "Invalid output messages" `Quick test_invalid_output_messages;
   ]