diff --git a/changes/01-feature/1389-assert.md b/changes/01-feature/1389-assert.md
new file mode 100644
index 0000000000..9aab1429dc
--- /dev/null
+++ b/changes/01-feature/1389-assert.md
@@ -0,0 +1,2 @@
+- Add support for assertions; `assert` is now a keyword
+  ([PR 1389](https://github.com/jasmin-lang/jasmin/pull/1389)).
diff --git a/compiler/linter/Analyser/BackwardAnalyser.ml b/compiler/linter/Analyser/BackwardAnalyser.ml
index f166b67a45..2fde33277e 100644
--- a/compiler/linter/Analyser/BackwardAnalyser.ml
+++ b/compiler/linter/Analyser/BackwardAnalyser.ml
@@ -42,6 +42,12 @@ module type Logic = sig
     -> exprs
     -> domain
     -> domain annotation
+
+    val assertion :
+      Location.i_loc ->
+      string ->
+      expr ->
+      domain -> domain Annotation.annotation
 end
 
 module type S = sig
@@ -199,6 +205,9 @@ struct
       | Copn (lvs, tag, sopn, es) ->
           let annotation = Annotation.bind annotation (L.opn loc lvs tag sopn es) in
           (Copn (lvs, tag, sopn, es), annotation)
+      | Cassert (msg, e) ->
+          let annotation = Annotation.bind annotation (L.assertion loc msg e) in
+          (Cassert (msg, e), annotation)
       | Ccall (lvs, fn, es) ->
           let annotation = Annotation.bind annotation (L.funcall loc lvs fn es) in
           (Ccall (lvs, fn, es), annotation)
diff --git a/compiler/linter/Analyser/BackwardAnalyser.mli b/compiler/linter/Analyser/BackwardAnalyser.mli
index d10e82cb86..667d8f2348 100644
--- a/compiler/linter/Analyser/BackwardAnalyser.mli
+++ b/compiler/linter/Analyser/BackwardAnalyser.mli
@@ -116,6 +116,15 @@ module type Logic =
       Jasmin.Expr.assgn_tag ->
       'asm Jasmin.Sopn.sopn ->
       Jasmin.Prog.exprs -> domain -> domain Annotation.annotation
+
+    (**
+    Function to handle assert instruction
+    *)
+    val assertion :
+      Jasmin.Location.i_loc ->
+      string ->
+      Jasmin.Prog.expr ->
+      domain -> domain Annotation.annotation
   end
 
 (**
diff --git a/compiler/linter/Analyser/ForwardAnalyser.ml b/compiler/linter/Analyser/ForwardAnalyser.ml
index 2f061ab62a..4b019e4424 100644
--- a/compiler/linter/Analyser/ForwardAnalyser.ml
+++ b/compiler/linter/Analyser/ForwardAnalyser.ml
@@ -31,6 +31,8 @@ module type Logic = sig
 
   val opn :
     Location.i_loc -> lvals -> E.assgn_tag -> 'asm Sopn.sopn -> exprs -> domain -> domain annotation
+
+  val assertion : Location.i_loc -> string -> expr -> domain -> domain annotation
 end
 
 module type S = sig
@@ -180,6 +182,9 @@ module Make (Logic : Logic) : S with type domain = Logic.domain = struct
       | Copn (lvs, tag, sopn, es) ->
           let annotation = Annotation.bind annotation (Logic.opn loc lvs tag sopn es) in
           (Copn (lvs, tag, sopn, es), annotation)
+      | Cassert (msg, e) ->
+          let annotation = Annotation.bind annotation (Logic.assertion loc msg e) in
+          (Cassert (msg, e), annotation)
       | Ccall (lvs, fn, es) ->
           let annotation = Annotation.bind annotation (Logic.funcall loc lvs fn es) in
           (Ccall (lvs, fn, es), annotation)
diff --git a/compiler/linter/Analyser/ForwardAnalyser.mli b/compiler/linter/Analyser/ForwardAnalyser.mli
index b31a2d2e0f..db4c2e57d0 100644
--- a/compiler/linter/Analyser/ForwardAnalyser.mli
+++ b/compiler/linter/Analyser/ForwardAnalyser.mli
@@ -138,6 +138,16 @@ module type Logic =
       Jasmin.Expr.assgn_tag ->
       'asm Jasmin.Sopn.sopn ->
       Jasmin.Prog.exprs -> domain -> domain Annotation.annotation
+
+    (**
+    Function to handle assert instruction
+    *)
+    val assertion :
+      Jasmin.Location.i_loc ->
+      string ->
+      Jasmin.Prog.expr ->
+      domain -> domain Annotation.annotation
+
   end
 
 (**
diff --git a/compiler/linter/Analysis/Liveness/LivenessAnalyser.ml b/compiler/linter/Analysis/Liveness/LivenessAnalyser.ml
index 4b73536177..933dacf0ee 100644
--- a/compiler/linter/Analysis/Liveness/LivenessAnalyser.ml
+++ b/compiler/linter/Analysis/Liveness/LivenessAnalyser.ml
@@ -77,6 +77,9 @@ module LivenessDomain : BackwardAnalyser.Logic with type domain = Sv.t = struct
     | Oslh _ | Oasm _ | Opseudo_op _ ->
       Annotation (live_assigns domain lvs exprs)
 
+  let assertion _loc _msg e domain =
+    Annotation (Sv.union domain (Prog.vars_e e))
+
 end
 
 include BackwardAnalyser.Make (LivenessDomain)
diff --git a/compiler/linter/Analysis/ReachingDefinitions/RDAnalyser.ml b/compiler/linter/Analysis/ReachingDefinitions/RDAnalyser.ml
index 186770f27c..8010c73300 100644
--- a/compiler/linter/Analysis/ReachingDefinitions/RDAnalyser.ml
+++ b/compiler/linter/Analysis/ReachingDefinitions/RDAnalyser.ml
@@ -38,6 +38,7 @@ module ReachingDefinitionLogic :
   let syscall loc lvs _ _ domain = logic loc lvs domain
   let assign loc lv _ _ _ domain = logic loc [ lv ] domain
   let opn loc lvs _ _ _ domain = logic loc lvs domain
+  let assertion loc _ _ domain = logic loc [] domain
 end
 
 include ForwardAnalyser.Make (ReachingDefinitionLogic)
diff --git a/compiler/linter/Checker/DeadVariables.ml b/compiler/linter/Checker/DeadVariables.ml
index 5abd5745e3..78ed612186 100644
--- a/compiler/linter/Checker/DeadVariables.ml
+++ b/compiler/linter/Checker/DeadVariables.ml
@@ -31,7 +31,7 @@ let create_dv_error_instr loc =
 let has_keep_tag =
   function
   | Cassgn (_, tag, _, _) | Copn (_, tag, _, _) -> tag = AT_keep
-  | Csyscall _ | Cif _ | Cfor _ | Cwhile _ | Ccall _ -> false
+  | Csyscall _ | Cif _ | Cfor _ | Cwhile _ | Ccall _ | Cassert _ -> false
 
 let check_func func =
   let dv_errors = ref [] in
diff --git a/compiler/linter/Checker/VariableInitialisation.ml b/compiler/linter/Checker/VariableInitialisation.ml
index dce69fd940..a77e97ccaa 100644
--- a/compiler/linter/Checker/VariableInitialisation.ml
+++ b/compiler/linter/Checker/VariableInitialisation.ml
@@ -54,6 +54,7 @@ let check_func fd =
     | Copn (xs, _, _, es) | Csyscall (xs, _, es) | Ccall (xs, _, es) ->
         check_lvs i_info xs;
         check_es i_info es
+    | Cassert (_, e)
     | Cif (e, _, _) -> check_e i_info e
     | Cfor (_, (_, e1, e2), _) -> check_es i_info [ e1; e2 ]
     | Cwhile (_, _, e, (_, i), _) -> check_e i e
diff --git a/compiler/safetylib/safetyInterpreter.ml b/compiler/safetylib/safetyInterpreter.ml
index d253519ad4..477e2eb4ba 100644
--- a/compiler/safetylib/safetyInterpreter.ml
+++ b/compiler/safetylib/safetyInterpreter.ml
@@ -112,6 +112,8 @@ type safe_cond =
   | NotEqual of op_kind * expr * expr
   | Termination of bool (* the boolean signals whether this is a severe violation *)
 
+  | GeneralCond of expr
+
 let notZero(ws, e) = NotEqual(Op_w ws, e, pcast ws (Pconst (Z.of_int 0)))
 
 let severe_violation =
@@ -166,6 +168,8 @@ let pp_safety_cond fmt = function
 
   | Termination b -> Format.fprintf fmt "termination%s" (if b then "" else " has not been checked")
 
+  | GeneralCond e -> Format.fprintf fmt "%a" pp_expr e
+
 type violation_loc =
   | InProg of Prog.L.i_loc
   | InReturn of funname
@@ -454,6 +458,7 @@ let safe_opn pd asmOp safe opn es =
 let safe_instr pd asmOp ginstr = match ginstr.i_desc with
   | Cassgn (lv, _, _, e) -> safe_e_rec (safe_lval lv) e
   | Copn (lvs,_,opn,es) -> safe_opn pd asmOp (safe_lvals lvs @ safe_es es) opn es
+  | Cassert (_, e) -> safe_e_rec [ GeneralCond e ] e
   | Cif(e, _, _) -> safe_e e
   | Cwhile(_, _, _, _, _) -> []       (* We check the while condition later. *)
   | Ccall(lvs, _, es) | Csyscall(lvs, _, es) -> safe_lvals lvs @ safe_es es
@@ -758,6 +763,12 @@ end = struct
         | Some c ->
           AbsDom.is_bottom (AbsDom.meet_btcons state.abs c) end
 
+    | GeneralCond e ->
+       let ne = Papp1 (Onot, e) in
+       begin match AbsExpr.bexpr_to_btcons ne state.abs with
+       | None -> false
+       | Some c -> AbsDom.is_bottom (AbsDom.meet_btcons state.abs c) end
+
     (* These are checked elsewhere *)
     | AlignedPtr _ | AlignedExpr _ | Valid _ | Termination _ -> true
 
@@ -1251,6 +1262,7 @@ end = struct
       | Cassgn (lv, _, _, e)    -> nm_lv vs_for lv && nm_e vs_for e
       | Copn (lvs, _, _, es)    -> nm_lvs vs_for lvs && nm_es vs_for es
       | Csyscall(lvs, _ ,es)    -> nm_lvs vs_for lvs && nm_es vs_for es
+      | Cassert(_, e)           -> nm_e vs_for e
       | Cif (e, st, st')        ->
         nm_e vs_for e && nm_stmt vs_for st && nm_stmt vs_for st'
       | Cfor (i, _, st)         -> nm_stmt (i :: vs_for) st
@@ -1465,6 +1477,8 @@ end = struct
       | Csyscall(lvs, sc, es) ->
          aeval_syscall state sc lvs es
 
+      | Cassert _ -> state
+
       | Cif(e,c1,c2) ->
         aeval_if ginstr e c1 c2 state
 
diff --git a/compiler/safetylib/safetyPreanalysis.ml b/compiler/safetylib/safetyPreanalysis.ml
index d3ca7fea70..54227beb73 100644
--- a/compiler/safetylib/safetyPreanalysis.ml
+++ b/compiler/safetylib/safetyPreanalysis.ml
@@ -86,6 +86,8 @@ end = struct
       Cassgn (mk_lval fn lv, tag, ty, mk_expr fn e)
     | Copn (lvls, tag, opn, exprs) ->
       Copn (mk_lvals fn lvls, tag, opn, mk_exprs fn exprs)
+    | Cassert (msg, e) ->
+       Cassert (msg, mk_expr fn e)
     | Csyscall (lvls, o, exprs) ->
         Csyscall(mk_lvals fn lvls, o, mk_exprs fn exprs)
     | Cif (e, st, st') ->
@@ -357,6 +359,8 @@ end = struct
           | _ -> assert false
       else None
 
+    | Cassert _ -> None
+
     | Cif (_, c1, c2) ->
       begin match pa_flag_setfrom v c1, pa_flag_setfrom v c2 with
         | None, None -> None
@@ -380,6 +384,8 @@ end = struct
     | Copn (lvs, _, _, es) | Csyscall(lvs, _, es) -> List.fold_left (fun st lv ->
         List.fold_left (fun st e -> pa_lv st lv e) st es) st lvs
 
+    | Cassert _ -> st
+
     | Cif (b, c1, c2) ->
       let vs,st = expr_vars st b in
       let st = { st with if_conds = b :: st.if_conds } in
@@ -547,6 +553,7 @@ end = struct
       let sv = collect_vars_lv sv lv in
       collect_vars_e sv e
     | Ccall _ -> raise Fcall
+    | Cassert (_, e) ->  collect_vars_e sv e
 
   and collect_vars_is sv is = List.fold_left collect_vars_i sv is
 
diff --git a/compiler/src/alias.ml b/compiler/src/alias.ml
index acb06d4567..fe7c7e6836 100644
--- a/compiler/src/alias.ml
+++ b/compiler/src/alias.ml
@@ -252,6 +252,7 @@ let rec analyze_instr_r params cc a =
     | None -> a 
     | Some l -> link_array_return params a xs es l
     end
+  | Cassert _ -> a
   | Cif(_, s1, s2) ->
      let a1 = analyze_stmt params cc a s1 |> normalize_map in
      let a2 = analyze_stmt params cc a s2 |> normalize_map in
diff --git a/compiler/src/autoSpill.ml b/compiler/src/autoSpill.ml
index a4615a925f..1ca55f2c1e 100644
--- a/compiler/src/autoSpill.ml
+++ b/compiler/src/autoSpill.ml
@@ -42,13 +42,14 @@ let vars_i = function
   | Cassgn (x, _, _, e) -> Sv.union (vars_lv x) (vars_e e)
   | Copn (xs, _, _, es) | Csyscall (xs, _, es) | Ccall (xs, _, es) ->
       List.fold Sv.union (vars_es es) (List.map vars_lv xs)
+  | Cassert (_, e) -> vars_e e
   | Cfor _ | Cif _ | Cwhile _ -> assert false
 
 let rec spill_all_i strategy i =
   let wrap i_desc = { i with i_desc; i_annot = [] } in
   let op o xs = xs |> spillable strategy |> mk_spill o |> wrap in
   match i.i_desc with
-  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ ->
+  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _ ->
       [ op Unspill (vars_i i.i_desc); i; op Spill (assigns i.i_desc) ]
   | Cif (e, c1, c2) ->
       [
diff --git a/compiler/src/compile.ml b/compiler/src/compile.ml
index 8659277cd4..03443095ee 100644
--- a/compiler/src/compile.ml
+++ b/compiler/src/compile.ml
@@ -50,7 +50,7 @@ let rec warn_extra_i pd msfsize asmOp i =
   | Cfor _ ->
       hierror ~loc:(Lmore i.i_loc) ~kind:"compilation error" ~internal:true
         "for loop remains"
-  | Ccall _ | Csyscall _ -> ()
+  | Ccall _ | Csyscall _ | Cassert _ -> ()
 
 let warn_extra_fd pd msfsize asmOp (_, fd) = List.iter (warn_extra_i pd msfsize asmOp) fd.f_body
 
diff --git a/compiler/src/conv.ml b/compiler/src/conv.ml
index c80cbe624d..adc5fabdde 100644
--- a/compiler/src/conv.ml
+++ b/compiler/src/conv.ml
@@ -164,6 +164,10 @@ and cinstr_r_of_instr_r p i =
       C.Csyscall(clval_of_lvals x, o, cexpr_of_exprs e) in
     C.MkI(p, ir)
 
+  | Cassert (msg, e) ->
+     let ir = C.Cassert (msg, cexpr_of_expr e) in
+     C.MkI (p, ir)
+
   | Cif(e,c1,c2) ->
     let c1 = cstmt_of_stmt c1 in
     let c2 = cstmt_of_stmt c2 in
@@ -204,6 +208,9 @@ and instr_r_of_cinstr_r = function
   | C.Csyscall(x,o,e) ->
     Csyscall(lval_of_clvals x, o, expr_of_cexprs e)
 
+  | C.Cassert (msg, e) ->
+     Cassert (msg, expr_of_cexpr e)
+
   | C.Cif(e,c1,c2) ->
     let c1 = stmt_of_cstmt c1 in
     let c2 = stmt_of_cstmt c2 in
diff --git a/compiler/src/ct_checker_forward.ml b/compiler/src/ct_checker_forward.ml
index d3296ceaef..1a88f832d5 100644
--- a/compiler/src/ct_checker_forward.ml
+++ b/compiler/src/ct_checker_forward.ml
@@ -561,6 +561,9 @@ let rec ty_instr is_ct_asm fenv env i =
     let env, _ = ty_exprs_max ~public:true env es in
     ty_lvals1 env xs (declassify_lvl ~loc i.i_annot Secret)
 
+  (* We ignore the contents of assertion *)
+  | Cassert _ -> env
+
   | Cif(e, c1, c2) ->
     let env, _ = ty_expr ~public:true env e in
     let env1 = ty_cmd is_ct_asm fenv env c1 in
diff --git a/compiler/src/evaluator.ml b/compiler/src/evaluator.ml
index 1ecbd5f057..30b1df80cf 100644
--- a/compiler/src/evaluator.ml
+++ b/compiler/src/evaluator.ml
@@ -23,6 +23,7 @@ let pp_error fmt err =
   | ErrType  -> "type error"
   | ErrArith -> "arithmetic error"
   | ErrSemUndef -> "undefined semantics"
+  | ErrAssert _ -> "assertion violation"
 
 let exn_exec (ii:instr_info) (r: 't exec) = 
   match r with
@@ -109,6 +110,12 @@ let small_step1 ep spp sip s =
       let s2 = exn_exec ii (write_lvals nosubword ep spp true gd {escs = scs; emem = m; evm = s1.evm} xs vs) in
       { s with s_cmd = c; s_estate = s2 }
 
+    | Cassert (p,a) ->
+      let v = exn_exec ii (sem_pexpr nosubword ep spp true gd s1 a) in
+      let b = of_val_b ii v in
+      if not b then raise (Eval_error(ii, ErrAssert p));
+      { s with s_cmd = c }
+
     | Cif(e,c1,c2) ->
       let b = of_val_b ii (exn_exec ii (sem_pexpr nosubword ep spp true gd s1 e)) in
       let c = (if b then c1 else c2) @ c in
diff --git a/compiler/src/glob_options.ml b/compiler/src/glob_options.ml
index bec967b640..34b0f5b63c 100644
--- a/compiler/src/glob_options.ml
+++ b/compiler/src/glob_options.ml
@@ -141,6 +141,7 @@ let set_cc cc =
   in call_conv := cc
 
 let print_strings = function
+  | Compiler.RemoveAssertion             -> "rmassert", "remove logical assertion"
   | Compiler.Typing                      -> "typing"   , "typing"
   | Compiler.ParamsExpansion             -> "cstexp"   , "param expansion"
   | Compiler.InsertRenaming              -> "rename"   , "add renaming assignments at export function boundaries"
diff --git a/compiler/src/insert_copy_and_fix_length.ml b/compiler/src/insert_copy_and_fix_length.ml
index 4f0803cefe..bcec21012a 100644
--- a/compiler/src/insert_copy_and_fix_length.ml
+++ b/compiler/src/insert_copy_and_fix_length.ml
@@ -105,7 +105,7 @@ and iac_instr_r pd loc ir =
       Csyscall(xs, Syscall_t.RandomBytes (ws, Conv.pos_of_int len), es)
     end
 
-  | Ccall _ -> ir
+  | Ccall _ | Cassert _ -> ir
 
 let iac_func pd f =
   { f with f_body = iac_stmt pd f.f_body }
diff --git a/compiler/src/latex_printer.ml b/compiler/src/latex_printer.ml
index 648160eb5d..8199961457 100644
--- a/compiler/src/latex_printer.ml
+++ b/compiler/src/latex_printer.ml
@@ -328,6 +328,8 @@ let rec pp_instr depth fmt (annot, p) =
     F.fprintf fmt "%a%a;"
       pp_expr e
       (pp_opt pp_sidecond) cnd
+  | PIAssert (msg, e) ->
+     F.fprintf fmt "%a(%a, %a)" kw "assert" pp_string (L.unloc msg) pp_expr e
   | PIIf (b, th, el) ->
     begin
     F.fprintf fmt "%a %a %a"
diff --git a/compiler/src/lexer.mll b/compiler/src/lexer.mll
index 0aa1028834..130abbf2a7 100644
--- a/compiler/src/lexer.mll
+++ b/compiler/src/lexer.mll
@@ -63,6 +63,7 @@
     "from"  , FROM   ;
     "global", GLOBAL ;
     "if"    , IF     ;
+    "assert", ASSERT ;
     "inline", INLINE ;
     "mut"   , MUTABLE;
     "namespace", NAMESPACE;
diff --git a/compiler/src/liveness.ml b/compiler/src/liveness.ml
index 818e223f27..2c610b5c04 100644
--- a/compiler/src/liveness.ml
+++ b/compiler/src/liveness.ml
@@ -45,6 +45,10 @@ and live_d weak d (s_o: Sv.t) =
      else s_o in
     s_i, s_o, Copn(xs,t,o,es)
 
+  | Cassert (msg, e) ->
+     let s_i = Sv.union (vars_e e) s_o in
+     s_i, s_o, Cassert (msg, e)
+
   | Cif(e,c1,c2) ->
     let s1, c1 = live_c weak c1 s_o in
     let s2, c2 = live_c weak c2 s_o in
@@ -103,7 +107,7 @@ let iter_call_sites (cbf: L.i_loc -> funname -> lvals -> Sv.t * Sv.t -> unit)
       match i.i_desc with
       | Ccall (xs, fn, _) -> cbf i.i_loc fn xs i.i_info
       | Csyscall (xs, op, _) -> cbs i.i_loc op xs i.i_info
-      | (Cassgn _ | Copn _ | Cif _ | Cfor _ | Cwhile _) -> ()
+      | (Cassgn _ | Copn _ | Cif _ | Cfor _ | Cwhile _ | Cassert _) -> ()
     ) f.f_body
 
 let pp_info fmt (s1, s2) =
@@ -122,7 +126,7 @@ let rec conflicts_i cf i =
   let cf = merge_class cf s1 in
 
   match i.i_desc with
-  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ ->
+  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _ ->
     merge_class cf s2
   | Cfor( _, _, c) ->
     conflicts_c (merge_class cf s2) c
diff --git a/compiler/src/parser.mly b/compiler/src/parser.mly
index c267931b4c..911298f385 100644
--- a/compiler/src/parser.mly
+++ b/compiler/src/parser.mly
@@ -23,6 +23,7 @@
 %token ALIGNED
 %token AMP
 %token AMPAMP
+%token ASSERT
 %token BANG
 %token BANGEQ
 %token COLON
@@ -381,6 +382,9 @@ pinstr_r:
     { let { Location.pl_loc = loc; Location.pl_desc = (f, args) } = fc in
       PIAssign ((None, []), `Raw, Location.mk_loc loc (PECall (f, args)), c) }
 
+| ASSERT LPAREN msg=loc(STRING) COMMA e=pexpr RPAREN SEMICOLON
+    { PIAssert(msg, e) }
+
 | s=pif { s }
 
 | FOR v=var EQ ce1=pexpr TO ce2=pexpr is=pblock
diff --git a/compiler/src/pretyping.ml b/compiler/src/pretyping.ml
index 69abf9d444..ad31a99960 100644
--- a/compiler/src/pretyping.ml
+++ b/compiler/src/pretyping.ml
@@ -2137,6 +2137,10 @@ let rec tt_instr arch_info (env : 'asm Env.env) ((pannot,pi) : S.pinstr) : 'asm
 
   | S.PIAssign (ls, eqop, pe, ocp) -> env, tt_assign env env ls eqop pe ocp
 
+  | PIAssert (msg, pe) ->
+     let e  = tt_expr_bool arch_info.pd env pe in
+     env, [mk_i (P.Cassert (L.unloc msg, e))]
+
   | PIIf (cp, st, sf) ->
       let c  = tt_expr_bool arch_info.pd env cp in
       let st = tt_block arch_info env st in
@@ -2236,7 +2240,7 @@ let rec add_reserved_i env (_,i) =
      List.fold_left (fun env id -> Env.add_reserved env (L.unloc id)) env ids
   | S.PIdeclinit (_, ids) ->
       List.fold_left (fun env id -> Env.add_reserved env (L.unloc (fst (L.unloc id)))) env ids
-  | PIArrayInit _ | PIAssign _ -> env
+  | PIArrayInit _ | PIAssign _ | PIAssert _ -> env
   | PIIf(_, c, oc) -> add_reserved_oc (add_reserved_c' env c) oc
   | PIFor(_, _, c) -> add_reserved_c' env c
   | PIWhile(oc1, _, oc2) -> add_reserved_oc (add_reserved_oc env oc1) oc2
diff --git a/compiler/src/printer.ml b/compiler/src/printer.ml
index b7201845d4..73eca10051 100644
--- a/compiler/src/printer.ml
+++ b/compiler/src/printer.ml
@@ -175,6 +175,11 @@ let rec pp_gi ~debug pp_info pp_len pp_opn pp_var fmt i =
       F.fprintf fmt "@[<hov 2>%a%s(%a);@]"
         (pp_glvs ~debug pp_len pp_var) x (pp_syscall o) (pp_ges ~debug pp_len pp_var) e
 
+  | Cassert(msg, e) ->
+    F.fprintf fmt "@[<hov 2>assert(\"%a\", %a);@]"
+      pp_escape_string msg
+     (pp_ge ~debug pp_len pp_var) e
+
   | Cif(e, c, []) ->
     F.fprintf fmt "@[<v>if %a %a@]"
       (pp_ge ~debug pp_len pp_var) e (pp_cblock ~debug pp_info pp_len pp_opn pp_var) c
diff --git a/compiler/src/prog.ml b/compiler/src/prog.ml
index 904b4faba6..6ee7d115c8 100644
--- a/compiler/src/prog.ml
+++ b/compiler/src/prog.ml
@@ -92,11 +92,14 @@ type 'len glvals = 'len glval list
 
 type 'len grange = E.dir * 'len gexpr * 'len gexpr
 
+type 'len assertion = string * 'len gexpr
+
 type ('len, 'info, 'asm) ginstr_r =
   | Cassgn of 'len glval * E.assgn_tag * 'len gty * 'len gexpr
   (* turn 'asm Sopn.sopn into 'sopn? could be useful to ensure that we remove things statically *)
   | Copn   of 'len glvals * E.assgn_tag * 'asm Sopn.sopn * 'len gexprs
   | Csyscall of 'len glvals * (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t * 'len gexprs
+  | Cassert of 'len assertion
   | Cif    of 'len gexpr * ('len, 'info, 'asm) gstmt * ('len, 'info, 'asm) gstmt
   | Cfor   of 'len gvar_i * 'len grange * ('len, 'info, 'asm) gstmt
   | Cwhile of E.align * ('len, 'info, 'asm) gstmt * 'len gexpr * (IInfo.t * 'info) * ('len, 'info, 'asm) gstmt
@@ -276,6 +279,7 @@ let rec rvars_i f s i =
   match i.i_desc with
   | Cassgn(x, _, _, e)  -> rvars_e f (rvars_lv f s x) e
   | Copn(x,_,_,e)  | Csyscall (x, _, e) -> rvars_es f (rvars_lvs f s x) e
+  | Cassert(_, e) -> rvars_e f s e
   | Cif(e,c1,c2)   -> rvars_c f (rvars_c f (rvars_e f s e) c1) c2
   | Cfor(x,(_,e1,e2), c) ->
     rvars_c f (rvars_e f (rvars_e f (f (L.unloc x) s) e1) e2) c
@@ -328,6 +332,7 @@ let rec written_vars_i ((v, f) as acc) i =
     -> List.fold_left written_lv v xs, f
   | Ccall(xs, fn, _) ->
      List.fold_left written_lv v xs, Mf.modify_def [] fn (fun old -> i.i_loc :: old) f
+  | Cassert (_, _) -> v, f
   | Cif(_, s1, s2)
   | Cwhile(_, s1, _, _, s2)
     -> written_vars_stmt (written_vars_stmt acc s1) s2
@@ -344,7 +349,7 @@ let written_vars_fc fc =
 let rec refresh_i_loc_i (i:('info, 'asm) instr) : ('info, 'asm) instr =
   let i_desc =
     match i.i_desc with
-    | Cassgn _ | Copn _ | Csyscall _ | Ccall _ -> i.i_desc
+    | Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _ -> i.i_desc
     | Cif(e, c1, c2) ->
         Cif(e, refresh_i_loc_c c1, refresh_i_loc_c c2)
     | Cfor(x, r, c) ->
@@ -475,7 +480,7 @@ let expr_of_lval = function
 let rec has_syscall_i i =
   match i.i_desc with
   | Csyscall _ -> true
-  | Cassgn _ | Copn _ | Ccall _ -> false
+  | Cassgn _ | Copn _ | Ccall _ | Cassert _ -> false
   | Cif (_, c1, c2) | Cwhile(_, c1, _, _, c2) -> has_syscall c1 || has_syscall c2
   | Cfor (_, _, c) -> has_syscall c
 
@@ -484,7 +489,7 @@ and has_syscall c = List.exists has_syscall_i c
 let rec has_call_or_syscall_i i =
   match i.i_desc with
   | Csyscall _ | Ccall _ -> true
-  | Cassgn _ | Copn _ -> false
+  | Cassgn _ | Copn _ | Cassert _ -> false
   | Cif (_, c1, c2) | Cwhile(_, c1, _, _, c2) -> has_call_or_syscall c1 || has_call_or_syscall c2
   | Cfor (_, _, c) -> has_call_or_syscall c
 
@@ -498,7 +503,7 @@ let is_inline annot cc =
 let rec spilled_i s i =
   match i.i_desc with
   | Copn(_, _, Sopn.Opseudo_op (Pseudo_operator.Ospill _), es) -> rvars_es Sv.add s es
-  | Cassgn _ | Csyscall _ | Ccall _ | Copn _-> s
+  | Cassgn _ | Csyscall _ | Ccall _ | Copn _ | Cassert _ -> s
   | Cif(_e, c1, c2)  -> spilled_c (spilled_c s c1) c2
   | Cfor(_, _, c)    -> spilled_c s c
   | Cwhile(_, c, _, _, c') -> spilled_c (spilled_c s c) c'
@@ -511,7 +516,7 @@ let assigns = function
   | Cassgn (x, _, _, _) -> written_lv Sv.empty x
   | Copn (xs, _, _, _) | Csyscall (xs, _, _) | Ccall (xs, _, _) ->
       List.fold_left written_lv Sv.empty xs
-  | Cif _ | Cwhile _ |Cfor _ -> Sv.empty
+  | Cif _ | Cwhile _ | Cassert _ | Cfor _ -> Sv.empty
 
 let is_lmem = function
   | Lmem _ -> true
@@ -521,7 +526,7 @@ let has_effect = function
   | Csyscall _ | Ccall _ -> true
   | Cassgn (x, _, _, _) -> is_lmem x
   | Copn (xs, _, _, _) -> List.exists is_lmem xs
-  | Cif _ | Cwhile _ | Cfor _ -> false
+  | Cassert _ | Cif _ | Cwhile _ | Cfor _ -> false
 
 (* -------------------------------------------------------------------- *)
 let rec iter_instr f stmt = List.iter (iter_instr_i f) stmt
@@ -531,7 +536,7 @@ and iter_instr_i f gi =
   iter_instr_ir f gi.i_desc
 
 and iter_instr_ir f = function
-  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ -> ()
+  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _ -> ()
   | Cfor (_, _, c) -> iter_instr f c
   | Cif (_, c1, c2) | Cwhile (_, c1, _, _, c2) ->
      iter_instr f c1;
diff --git a/compiler/src/prog.mli b/compiler/src/prog.mli
index 0519548743..75ae4de85a 100644
--- a/compiler/src/prog.mli
+++ b/compiler/src/prog.mli
@@ -59,11 +59,14 @@ type 'len grange = E.dir * 'len gexpr * 'len gexpr
    This is durty ...
 *)
 
+type 'len assertion = string * 'len gexpr
+
 type ('len, 'info, 'asm) ginstr_r =
   | Cassgn of 'len glval * E.assgn_tag * 'len gty * 'len gexpr
   (* turn 'asm Sopn.sopn into 'sopn? could be useful to ensure that we remove things statically *)
   | Copn   of 'len glvals * E.assgn_tag * 'asm Sopn.sopn * 'len gexprs
   | Csyscall of 'len glvals * (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t * 'len gexprs
+  | Cassert of 'len assertion
   | Cif    of 'len gexpr * ('len, 'info, 'asm) gstmt * ('len, 'info, 'asm) gstmt
   | Cfor   of 'len gvar_i * 'len grange * ('len, 'info, 'asm) gstmt
   | Cwhile of E.align * ('len, 'info, 'asm) gstmt * 'len gexpr * (IInfo.t * 'info) * ('len, 'info, 'asm) gstmt
diff --git a/compiler/src/regalloc.ml b/compiler/src/regalloc.ml
index 0c8cacced0..f9785d73d6 100644
--- a/compiler/src/regalloc.ml
+++ b/compiler/src/regalloc.ml
@@ -38,6 +38,7 @@ let fill_in_missing_names (f: ('info, 'asm) func) : ('info, 'asm) func =
     | Cassgn (lv, tg, ty, e) -> Cassgn (fill_lv lv, tg, ty, e)
     | Copn (lvs, tg, op, es) -> Copn (fill_lvs lvs, tg, op, es)
     | Csyscall (lvs, op, es) -> Csyscall(fill_lvs lvs, op, es)
+    | Cassert (msg, e) -> Cassert (msg, e)
     | Cif (e, s1, s2) -> Cif (e, fill_stmt s1, fill_stmt s2)
     | Cfor (i, r, s) -> Cfor (i, r, fill_stmt s)
     | Cwhile (a, s, e, loc, s') -> Cwhile (a, fill_stmt s, e, loc, fill_stmt s')
@@ -275,6 +276,7 @@ let collect_equality_constraints_in_func
        | (None, _) | (_, None) -> ()
        end
     | Cassgn _ -> ()
+    | Cassert _ -> ()
     | Ccall (xs, fn, es) ->
       let get_Pvar a =
         match a with
@@ -471,6 +473,7 @@ let collect_conflicts pd reg_size asmOp
     | Copn _
     | Csyscall _
     | Ccall _
+    | Cassert _
       -> c
     | Cwhile (_, s1, _, _, s2)
     | Cif (_, s1, s2)
@@ -491,6 +494,7 @@ let iter_variables (cb: var -> unit) (f: ('info, 'asm) func) : unit =
   let iter_exprs es = vars_es es |> iter_sv in
   let rec iter_instr_r =
     function
+    | Cassert (_, e) -> iter_expr e
     | Cassgn (lv, _, _, e) -> iter_lv lv; iter_expr e
     | (Ccall (lvs, _, es) | Copn (lvs, _, _, es)) | Csyscall(lvs, _ , es) -> iter_lvs lvs; iter_exprs es
     | (Cwhile (_, s1, e, _, s2) | Cif (e, s1, s2)) -> iter_expr e; iter_stmt s1; iter_stmt s2
@@ -798,7 +802,7 @@ let allocate_forced_registers return_addresses nv (vars: int Hv.t) tr (cnf: conf
     | Cwhile (_, s1, _, _, s2)
     | Cif (_, s1, s2)
         -> alloc_stmt s1 c |> alloc_stmt s2
-    | Cassgn _
+    | Cassgn _ | Cassert _
       -> c
     | Ccall (lvs, _, es) ->
        (* TODO: check this *)
diff --git a/compiler/src/scopeTree.ml b/compiler/src/scopeTree.ml
index 8e3563a2b4..ca181e0cee 100644
--- a/compiler/src/scopeTree.ml
+++ b/compiler/src/scopeTree.ml
@@ -96,7 +96,7 @@ let variables_in_instr_r : _ pinstr_r -> Spv.t = function
       variables_in_pexprs (variables_in_plvals Spv.empty xs) es
   | Cfor (x, (_, e1, e2), _) ->
       variables_in_pexprs (Spv.singleton (L.unloc x)) [ e1; e2 ]
-  | Cif (e, _, _) | Cwhile (_, _, e, _, _) -> variables_in_pexpr Spv.empty e
+  | Cif (e, _, _) | Cwhile (_, _, e, _, _) | Cassert (_, e) -> variables_in_pexpr Spv.empty e
 
 (** Maps each variable to the set of nodes at which it occurs *)
 let variable_occurrences (c : _ pstmt) : nodeset Mpv.t =
@@ -119,7 +119,7 @@ let rec tree_of_instr ((acc : tree), (t : Tree.t option)) (i : _ ginstr) :
   (tree_of_instr_r acc t i.i_desc, Some t)
 
 and tree_of_instr_r (acc : tree) (t : Tree.t) : _ ginstr_r -> tree = function
-  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ -> acc
+  | Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _ -> acc
   | Cfor (_, _, c) -> tree_of_stmt acc (Some t) c |> fst
   | Cif (_, c1, c2) | Cwhile (_, c1, _, _, c2) ->
       let acc, _ = tree_of_stmt acc (Some t) c1 in
diff --git a/compiler/src/sct_checker_forward.ml b/compiler/src/sct_checker_forward.ml
index c6f4e3e79d..c1dab7d636 100644
--- a/compiler/src/sct_checker_forward.ml
+++ b/compiler/src/sct_checker_forward.ml
@@ -159,6 +159,7 @@ let rec modmsf_i fenv i =
       let r = modmsf_c fenv c0 in
       if is_Modified r then r else modmsf_c fenv c1
     else modified_here
+  | Cassert _
   | Cassgn _ -> NotModified
   | Copn (_, _, o, _) ->
     begin match is_special o with
@@ -267,6 +268,8 @@ let rec infer_msf_i ~withcheck fenv (tbl:(L.i_loc, Sv.t) Hashtbl.t) i ms =
       (* withcheck => is_empty ms *)
       ms
 
+  | Cassert _ -> ms
+
   | Cif (_, c1, c2) ->
     let ms1 = infer_msf_c ~withcheck fenv tbl c1 ms in
     let ms2 = infer_msf_c ~withcheck fenv tbl c2 ms in
@@ -1015,6 +1018,8 @@ and ty_instr_r is_ct_asm fenv env ((msf,venv) as msf_e :msf_e) i =
       ty_lvals1 env msf_e xs (declassify_ty ~loc:i.i_loc env i.i_annot ety)
     end
 
+  | Cassert _ -> msf_e
+
   | Cif(e, c1, c2) ->
     let msf1, msf2 =
       if is_inline i then
diff --git a/compiler/src/slicing.ml b/compiler/src/slicing.ml
index a046f1e886..2cf37c4b84 100644
--- a/compiler/src/slicing.ml
+++ b/compiler/src/slicing.ml
@@ -33,6 +33,7 @@ and inspect_instr_r k = function
   | Cassgn (x, _, _, e) -> inspect_lv (inspect_e k e) x
   | Copn (xs, _, _, es) | Csyscall (xs, _, es) ->
       inspect_lvs (inspect_es k es) xs
+  | Cassert (_, e) -> inspect_e k e
   | Cif (g, a, b) | Cwhile (_, a, g, _, b) ->
       inspect_stmt (inspect_stmt (inspect_e k g) a) b
   | Cfor (_, (_, e1, e2), s) -> inspect_stmt (inspect_es k [ e1; e2 ]) s
diff --git a/compiler/src/ssa.ml b/compiler/src/ssa.ml
index abd689c617..5568abeb61 100644
--- a/compiler/src/ssa.ml
+++ b/compiler/src/ssa.ml
@@ -34,6 +34,7 @@ let rec written_vars_instr_r allvars w =
   function
   | Cfor (_, _, s)
     -> written_vars_stmt allvars w s
+  | Cassert _ -> w
   | Cassgn (x, _, _, _) -> written_vars_lvar allvars w x
   | Copn (xs, _, _, _)
   | Csyscall(xs,_,_)
@@ -73,6 +74,9 @@ let split_live_ranges (allvars: bool) (f: ('info, 'asm) func) : (unit, 'asm) fun
       let m, ys = rename_lvals allvars m xs in
       m, Ccall (ys, n, es)
     | Cfor _ -> assert false
+    | Cassert (p, a) ->
+      let a = rename_expr m a in
+      m, Cassert (p, a)
     | Cif (e, s1, s2) ->
       let os = written_vars_stmt allvars (written_vars_stmt allvars Sv.empty s1) s2 in
       let e = rename_expr m e in
@@ -130,7 +134,7 @@ let remove_phi_nodes (f: ('info, 'asm) func) : ('info, 'asm) func =
        | _ -> Some i)
     | Cif (b, s1, s2) -> Some (Cif (b, stmt s1, stmt s2))
     | Cwhile (a, s1, b, loc, s2) -> Some (Cwhile (a, stmt s1, b, loc, stmt s2))
-    | (Copn _ | Csyscall _ | Cfor _ | Ccall _) as i -> Some i
+    | (Copn _ | Csyscall _ | Cfor _ | Ccall _ | Cassert _) as i -> Some i
   and instr i =
     try Option.map (fun i_desc -> { i with i_desc }) (instr_r i.i_desc)
     with HiError e -> raise (HiError (add_iloc e i.i_loc))
diff --git a/compiler/src/subst.ml b/compiler/src/subst.ml
index e408268fa9..531af6ab3d 100644
--- a/compiler/src/subst.ml
+++ b/compiler/src/subst.ml
@@ -60,6 +60,7 @@ let rec gsubst_i (flen: ?loc:L.t -> 'len1 -> 'len2) f i =
       Cassgn(x, tg, ty, e)
     | Copn(x,t,o,e)   -> Copn(gsubst_lvals flen f x, t, o, gsubst_es flen f e)
     | Csyscall(x,o,e)   -> Csyscall(gsubst_lvals flen f x, o, gsubst_es flen f e)
+    | Cassert (msg, e)  -> Cassert (msg, gsubst_e flen f e)
     | Cif(e,c1,c2)  -> Cif(gsubst_e flen f e, gsubst_c flen f c1, gsubst_c flen f c2)
     | Cfor(x,(d,e1,e2),c) ->
         Cfor(gsubst_vdest f x, (d, gsubst_e flen f e1, gsubst_e flen f e2), gsubst_c flen f c)
@@ -396,7 +397,7 @@ let clone_func fc =
 let rec extend_iinfo_i pre i =
   let i_desc =
     match i.i_desc with
-    | Cassgn _ | Copn _ | Csyscall _ | Ccall _ -> i.i_desc
+    | Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _ -> i.i_desc
     | Cif(e,c1,c2) ->
       Cif(e, extend_iinfo_c pre c1, extend_iinfo_c pre c2)
     | Cfor(x,r,c) ->
diff --git a/compiler/src/syntax.ml b/compiler/src/syntax.ml
index d961c28b31..77c2495ca2 100644
--- a/compiler/src/syntax.ml
+++ b/compiler/src/syntax.ml
@@ -251,6 +251,7 @@ type pinstr_r =
       (** ArrayInit(x); *)
   | PIAssign    of plvals * peqop * pexpr * pexpr option
       (** x, y += z >> 4 if c; *)
+  | PIAssert    of pident * pexpr
   | PIIf        of pexpr * pblock * pblock option
       (** if e { … } else { … } *)
   | PIFor       of pident * (fordir * pexpr * pexpr) * pblock
diff --git a/compiler/src/toEC.ml b/compiler/src/toEC.ml
index 7449ff7089..b8a41b6046 100644
--- a/compiler/src/toEC.ml
+++ b/compiler/src/toEC.ml
@@ -1329,6 +1329,7 @@ let rec is_write_i x i =
     is_write_lv x lv
   | Copn(lvs,_,_,_) | Ccall(lvs, _, _) | Csyscall(lvs,_,_) ->
     is_write_lvs x lvs
+  | Cassert _ -> false
   | Cif(_, c1, c2) | Cwhile(_, c1, _, _, c2) ->
     is_write_c x c1 || is_write_c x c2
   | Cfor(x',_,c) ->
@@ -1339,7 +1340,7 @@ and is_write_c x c = List.exists (is_write_i x) c
 let rec remove_for_i i =
   let i_desc =
     match i.i_desc with
-    | Cassgn _ | Copn _ | Ccall _ | Csyscall _ -> i.i_desc
+    | Cassgn _ | Copn _ | Ccall _ | Csyscall _ | Cassert _ -> i.i_desc
     | Cif(e, c1, c2) -> Cif(e, remove_for c1, remove_for c2)
     | Cwhile(a, c1, e, loc, c2) -> Cwhile(a, remove_for c1, e, loc, remove_for c2)
     | Cfor(j,r,c) ->
@@ -1850,6 +1851,7 @@ struct
           let args = List.map (toec_cast env) (List.combine itys es) in
           (ec_leaks_es env es) @
           (ec_pcall env lvs [] otys [ec_syscall env o] args)
+      | Cassert _a -> [(* TODO *)]
       | Cif (e, c1, c2) ->
           let c1 env = toec_cmd asmOp env c1 in
           let c2 env = toec_cmd asmOp env c2 in
@@ -2048,7 +2050,7 @@ and used_func_c used c =
 
 and used_func_i used i =
   match i.i_desc with
-  | Cassgn _ | Copn _ | Csyscall _ -> used
+  | Cassgn _ | Copn _ | Csyscall _ | Cassert _ -> used
   | Cif (_,c1,c2)     -> used_func_c (used_func_c used c1) c2
   | Cfor(_,_,c)       -> used_func_c used c
   | Cwhile(_, c1, _, _, c2) -> used_func_c (used_func_c used c1) c2
diff --git a/compiler/src/typing.ml b/compiler/src/typing.ml
index 15bc595465..22bd39daab 100644
--- a/compiler/src/typing.ml
+++ b/compiler/src/typing.ml
@@ -194,6 +194,9 @@ let rec check_instr pd msfsz asmOp env i =
     check_exprs pd loc es tins;
     check_lvals pd loc xs tout
 
+  | Cassert(_p, a) ->
+    check_expr pd loc a tbool
+
   | Cif(e,c1,c2) ->
     check_expr pd loc e tbool;
     check_cmd pd msfsz asmOp env c1;
diff --git a/compiler/src/varalloc.ml b/compiler/src/varalloc.ml
index 679a0ac45d..c7943463c2 100644
--- a/compiler/src/varalloc.ml
+++ b/compiler/src/varalloc.ml
@@ -105,7 +105,7 @@ in
 
 let rec live_ranges_instr_r d_acc =
   function
-  | (Cassgn _ | Copn _ | Csyscall _ | Ccall _) -> d_acc
+  | (Cassgn _ | Copn _ | Csyscall _ | Ccall _ | Cassert _) -> d_acc
   | Cif (_, s1, s2)
   | Cwhile (_, s1, _, _, s2) ->
      let d_acc = live_ranges_stmt d_acc s1 in
@@ -201,6 +201,7 @@ let classes_alignment (onfun : funname -> param_info option list) (gtbl: alignme
     try match i.i_desc with
     | Cassgn(x,_,_,e) -> add_lv x; add_e e
     | Copn(xs,_,_,es) | Csyscall(xs,_,es) -> add_lvs xs; add_es es
+    | Cassert (_, e) -> add_e e
     | Cif(e, _, _) | Cwhile (_, _, e, _, _) -> add_e e
     | Cfor _ -> assert false
     | Ccall(xs, fn, es) ->
diff --git a/compiler/tests/exec/basic.jazz b/compiler/tests/exec/basic.jazz
index 85e92c8309..d17dce4624 100644
--- a/compiler/tests/exec/basic.jazz
+++ b/compiler/tests/exec/basic.jazz
@@ -38,3 +38,7 @@ inline fn mem1() -> reg u32 {
 
   return r;
 }
+
+inline fn test_assert(reg bool x) {
+  assert("label", x);
+}
diff --git a/compiler/tests/exec/exec.expected b/compiler/tests/exec/exec.expected
index 86e59dbe79..962ede9daf 100644
--- a/compiler/tests/exec/exec.expected
+++ b/compiler/tests/exec/exec.expected
@@ -2,6 +2,8 @@ f() = 0X5; 0X6
 ft() = [0X1; 0X0; 0X0; 0X0; 0XF; 0X0; 0X0; 0X0]
 mem() = 0XFF
 mem1() = 0XFF
+test_assert(true) =
+test_assert(false) failed with assertion violation
 test_stc() = 0X1
 test_clc() = 0X0
 test_poly1305() = [0XA8; 0X6; 0X1D; 0XC1; 0X30; 0X51; 0X36; 0XC6; 0XC2; 0X2B;
diff --git a/compiler/tests/exec/exec.ml b/compiler/tests/exec/exec.ml
index dc0e144c66..778739d37a 100644
--- a/compiler/tests/exec/exec.ml
+++ b/compiler/tests/exec/exec.ml
@@ -1,11 +1,15 @@
 open Execlib
 
+let jasmin_bool b = Jasmin.Values.Vbool b
+
 let () =
   let prog = load_file "basic.jazz" in
   exec prog [] "f" [];
   exec prog [] "ft" [];
   exec prog [ (Z.of_string "0x1000", Z.of_int 8) ] "mem" [];
-  exec prog [ (Z.of_string "0x1000", Z.of_int 16) ] "mem1" []
+  exec prog [ (Z.of_string "0x1000", Z.of_int 16) ] "mem1" [];
+  exec prog [] "test_assert" [ jasmin_bool true ];
+  exec prog [] "test_assert" [ jasmin_bool false ]
 
 let () =
   let prog = load_file "../success/x86-64/clc-stc.jazz" in
diff --git a/compiler/tests/exec/execlib.ml b/compiler/tests/exec/execlib.ml
index 8ab0b101cf..17c1943451 100644
--- a/compiler/tests/exec/execlib.ml
+++ b/compiler/tests/exec/execlib.ml
@@ -18,10 +18,14 @@ let funnames prog =
 let load_file name =
   let prog =
     let open Pretyping in
-    name
-    |> tt_file Arch.arch_info Env.empty None None
-    |> fst |> Env.decls
-    |> Compile.preprocess Arch.pointer_data Arch.msf_size Arch.asmOp
+    try
+      name
+      |> tt_file Arch.arch_info Env.empty None None
+      |> fst |> Env.decls
+      |> Compile.preprocess Arch.pointer_data Arch.msf_size Arch.asmOp
+    with TyError (loc, e) ->
+      Format.eprintf "%a: %a@." Location.pp_loc loc pp_tyerror e;
+      assert false
   in
   (funnames prog, Conv.cuprog_of_prog prog)
 
@@ -45,7 +49,8 @@ let exec (fs, prog) ms f args =
   in
   let pp_vals = Utils.pp_list "; " Evaluator.pp_val in
   let pp_res fmt = function
-    | Ok res -> Format.fprintf fmt "= %a" pp_vals res
+    | Ok res ->
+        Format.fprintf fmt "=%s%a" (if res <> [] then " " else "") pp_vals res
     | Error err -> Format.fprintf fmt "failed with %a" Evaluator.pp_error err
   in
   Format.printf "%s(%a) %a@." f.fn_name pp_vals args pp_res res
diff --git a/compiler/tests/printing.ml b/compiler/tests/printing.ml
index bd8cf7d017..224e79e2aa 100644
--- a/compiler/tests/printing.ml
+++ b/compiler/tests/printing.ml
@@ -130,6 +130,7 @@ and eq_pinstr_r (x : _ pinstr_r) y =
       eq_plval a e && b = f && eq_pty c g && eq_pexpr d h
   | Copn (a, b, c, d), Copn (e, f, g, h) ->
       eq_plvals a e && b = f && c = g && eq_pexprs d h
+  | Cassert (a, b), Cassert (c, d) -> a = c && eq_pexpr b d
   | Csyscall (a, b, c), Csyscall (d, e, f) ->
       eq_plvals a d && b = e && eq_pexprs c f
   | Cif (a, b, c), Cif (d, e, f) -> eq_pexpr a d && eq_pstmt b e && eq_pstmt c f
@@ -139,7 +140,9 @@ and eq_pinstr_r (x : _ pinstr_r) y =
       a = f && eq_pstmt b g && eq_pexpr c h && eq_pstmt e j
   | Ccall (a, b, c), Ccall (d, e, f) ->
       eq_plvals a d && b.fn_name = e.fn_name && eq_pexprs c f
-  | (Cassgn _ | Copn _ | Csyscall _ | Cif _ | Cfor _ | Cwhile _ | Ccall _), _ ->
+  | ( ( Cassgn _ | Copn _ | Csyscall _ | Cassert _ | Cif _ | Cfor _ | Cwhile _
+      | Ccall _ ),
+      _ ) ->
       false
 
 let eq_f_annot x y =
diff --git a/compiler/tests/safety/success/common/assertion.jazz b/compiler/tests/safety/success/common/assertion.jazz
new file mode 100644
index 0000000000..8737e36959
--- /dev/null
+++ b/compiler/tests/safety/success/common/assertion.jazz
@@ -0,0 +1,11 @@
+export fn safe() { assert("", true); }
+
+export fn repeated_ifs(reg u32 x y) {
+  reg u32 z = 0;
+  if x < y {
+    z = 1;
+  }
+  if x < y {
+    assert("again", z == 1);
+  }
+}
diff --git a/compiler/tests/success/common/assertion.jazz b/compiler/tests/success/common/assertion.jazz
new file mode 100644
index 0000000000..897a29e0cd
--- /dev/null
+++ b/compiler/tests/success/common/assertion.jazz
@@ -0,0 +1,10 @@
+export fn noop() {
+  assert("trivial", true);
+}
+
+export fn checked(reg u32 a) -> reg u32 {
+  if a < 100 {
+    assert("basic math", a < 100);
+  }
+  return a;
+}
diff --git a/docs/source/language/syntax/code.md b/docs/source/language/syntax/code.md
index b7a77f993e..e84c6e6ba8 100644
--- a/docs/source/language/syntax/code.md
+++ b/docs/source/language/syntax/code.md
@@ -10,6 +10,7 @@ Jasmin code comprises the following constructs:
 <instr> ::=
   | <instr_assign>
   | <instr_intrinsic>
+  | <instr_assert>
   | <instr_conditional>
   | <instr_while>
   | <instr_for>
@@ -108,6 +109,19 @@ The list of available architecture-specific instructions can be seen using
 `$ jasminc -help-intrinsics`.
 
 
+## Assertions
+
+```
+<instr_assert> ::=
+  | assert("label", <expr>);
+```
+
+Assertions do nothing, provided their argument evaluates properly to `true`.
+They can be used in the [reference
+interpreter](../../tools/reference_interpreter). The compiler erases the
+assertions in an early pass (soon after type-checking): they do not contribute
+to any code in the target assembly program.
+
 ## Conditionals
 
 ```
diff --git a/proofs/_CoqProject b/proofs/_CoqProject
index 2617fc33c2..b981988496 100644
--- a/proofs/_CoqProject
+++ b/proofs/_CoqProject
@@ -109,6 +109,8 @@ compiler/riscv_params_common.v
 compiler/riscv_params_common_proof.v
 compiler/riscv_stack_zeroization.v
 compiler/riscv_stack_zeroization_proof.v
+compiler/remove_assert.v
+compiler/remove_assert_proof.v
 compiler/remove_globals.v
 compiler/remove_globals_proof.v
 compiler/slh_lowering.v
diff --git a/proofs/compiler/arm_lowering_proof.v b/proofs/compiler/arm_lowering_proof.v
index ade56768a2..6998fae807 100644
--- a/proofs/compiler/arm_lowering_proof.v
+++ b/proofs/compiler/arm_lowering_proof.v
@@ -2015,6 +2015,8 @@ Opaque esem.
     rewrite /disj_fvars vars_I_syscall => /disjoint_union [hdisjx hdisje].
     apply (wequiv_syscall_rel_eq (sip:=sip)) with
        checker_st_eq_ex fvars => //.
+  (* Assert *)
+  + by move=> ? ii _; apply wequiv_noassert with (ev1:=ev) (ii:=ii).
   (* If *)
   + move=> e c1 c2 hc1 hc2 ii /disj_fvars_vars_I_Cif [hfve /hc1{}hc1 /hc2{}hc2] /=.
     case heq: lower_condition => [pre e'].
diff --git a/proofs/compiler/array_copy.v b/proofs/compiler/array_copy.v
index 958f66fed0..fcccc64b6b 100644
--- a/proofs/compiler/array_copy.v
+++ b/proofs/compiler/array_copy.v
@@ -126,7 +126,7 @@ Fixpoint array_copy_i V (i:instr) : cexec cmd :=
 
     | _ => ok [:: i]
     end
-  | Csyscall _ _ _ => ok [:: i]
+  | Csyscall _ _ _ | Cassert _ => ok [:: i]
   | Cif e c1 c2    =>
       Let c1 := array_copy_c V array_copy_i c1 in
       Let c2 := array_copy_c V array_copy_i c2 in
diff --git a/proofs/compiler/array_copy_proof.v b/proofs/compiler/array_copy_proof.v
index 7b3d460760..7b77f331b6 100644
--- a/proofs/compiler/array_copy_proof.v
+++ b/proofs/compiler/array_copy_proof.v
@@ -632,6 +632,8 @@ Proof.
     apply wequiv_syscall_rel_uincl with checker_st_uincl_on X => //.
     + by split => //; clear -hsub; SvD.fsetdec.
     by split => //; clear -hsub; SvD.fsetdec.
+  + move=> >; rewrite vars_I_assert /= => hsub _ [<-].
+    by apply wequiv_assert_rel_uincl with checker_st_uincl_on => //; split.
   + move=> e c1 c2 hc1 hc2 ii; rewrite vars_I_if => hsub i2 /=.
     t_xrbindP => c1' hc1' c2' hc2' <-.
     apply wequiv_if_rel_uincl with checker_st_uincl_on X X X => //.
diff --git a/proofs/compiler/array_expansion.v b/proofs/compiler/array_expansion.v
index 4e382794fb..337df67384 100644
--- a/proofs/compiler/array_expansion.v
+++ b/proofs/compiler/array_expansion.v
@@ -277,6 +277,10 @@ Fixpoint expand_i (m : t) (i : instr) : cexec instr :=
     Let es := add_iinfo ii (expand_es m es) in
     ok (MkI ii (Csyscall xs o es))
 
+  | Cassert a =>
+    Let a := add_iinfo ii (sndM (expand_e m) a) in
+    ok (MkI ii (Cassert a))
+
   | Cif b c1 c2 =>
     Let b  := add_iinfo ii (expand_e m b) in
     Let c1 := mapM (expand_i m) c1 in 
diff --git a/proofs/compiler/array_expansion_proof.v b/proofs/compiler/array_expansion_proof.v
index eb7bc38732..05ce43f414 100644
--- a/proofs/compiler/array_expansion_proof.v
+++ b/proofs/compiler/array_expansion_proof.v
@@ -967,6 +967,7 @@ Proof.
     by apply wequiv_opn_rel_eq with checker_exp m.
   + move=> xs1 o es1 ii i2_ /=; t_xrbindP => xs2 hxs es2 hes <-.
     by apply wequiv_syscall_rel_eq with checker_exp m.
+  + by move=> *; apply wequiv_noassert.
   + move=> e1 c1 c1' hc1 hc1' ii i2_ /=; t_xrbindP => e2 he c2 /hc1{}hc1 c2' /hc1'{}hc1' <-.
     apply wequiv_if_rel_eq with checker_exp m m m => //.
     by split => //=; rewrite he.
diff --git a/proofs/compiler/array_init.v b/proofs/compiler/array_init.v
index 363b61b5db..da50ab5ec4 100644
--- a/proofs/compiler/array_init.v
+++ b/proofs/compiler/array_init.v
@@ -30,8 +30,9 @@ Fixpoint remove_init_i i :=
           end in
         if t then [::] else [::i]
       else [::i]
-    | Copn _ _ _ _   => [::i]
-    | Csyscall _ _ _ => [::i]
+    | Copn _ _ _ _
+    | Csyscall _ _ _
+    | Cassert _ => [::i]
     | Cif e c1 c2  =>
       let c1 := foldr (fun i c => remove_init_i i ++ c) [::] c1 in
       let c2 := foldr (fun i c => remove_init_i i ++ c) [::] c2 in
diff --git a/proofs/compiler/array_init_proof.v b/proofs/compiler/array_init_proof.v
index 048d44a2f2..b8cb4f6367 100644
--- a/proofs/compiler/array_init_proof.v
+++ b/proofs/compiler/array_init_proof.v
@@ -306,6 +306,7 @@ Proof.
     by apply hu.
   + by move=> xs tg o es ii; apply wequiv_opn_rel_uincl with checker_st_uincl tt.
   + by move=> xs sc es ii; apply wequiv_syscall_rel_uincl with checker_st_uincl tt.
+  + by move=> a ii; apply wequiv_assert_rel_uincl with checker_st_uincl.
   + by move=> e c1 c2 hc1 hc2 ii; apply wequiv_if_rel_uincl with checker_st_uincl tt tt tt.
   + by move=> > hc ii; apply wequiv_for_rel_uincl with checker_st_uincl tt tt.
   + by move=> > ?? ii; apply wequiv_while_rel_uincl with checker_st_uincl tt.
@@ -728,7 +729,7 @@ Proof.
    apply wequiv_cat with (cmpl_inv I').
    + by have /= := hi I; rewrite heqi.
    by have /= := hc I'; rewrite heqc.
- 1-3, 5-7: by move=> * ii I; apply/it_aux.
+ 1-4, 6-8: by move=> * ii I; apply/it_aux.
  move=> e c1 c2 hc1 hc2 ii I /=.
  case heq1 : add_init_c => [c1' I1].
  case heq2 : add_init_c => [c2' I2] /=.
diff --git a/proofs/compiler/compiler.v b/proofs/compiler/compiler.v
index 75ba2d4cfc..c165118a6c 100644
--- a/proofs/compiler/compiler.v
+++ b/proofs/compiler/compiler.v
@@ -33,6 +33,7 @@ Require Import
   propagate_inline
   slh_lowering
   remove_globals
+  remove_assert
   stack_alloc
   stack_zeroization
   tunneling
@@ -85,6 +86,7 @@ Section COMPILER.
 Variant compiler_step :=
   | Typing                      : compiler_step
   | ParamsExpansion             : compiler_step
+  | RemoveAssertion             : compiler_step
   | InsertRenaming              : compiler_step
   | WintWord                    : compiler_step
   | ArrayCopy                   : compiler_step
@@ -122,6 +124,7 @@ Definition compiler_step_list := [::
     Typing
   ; ParamsExpansion
   ; InsertRenaming
+  ; RemoveAssertion
   ; WintWord
   ; ArrayCopy
   ; AddArrInit
@@ -257,6 +260,9 @@ Definition inlining (to_keep: seq funname) (p: uprog) : cexec uprog :=
 
 Definition compiler_first_part (to_keep: seq funname) (p: uprog) : cexec uprog :=
 
+  let p := remove_assert_prog p in
+  let p := cparams.(print_uprog) RemoveAssertion p in
+
   Let p := wi2w_prog (wsw:=withsubword) cparams.(remove_wint_annot) cparams.(dead_vars_ufd) p in
   let p := cparams.(print_uprog) WintWord p in
 
diff --git a/proofs/compiler/compiler_proof.v b/proofs/compiler/compiler_proof.v
index 6603089987..5dee5f4aa3 100644
--- a/proofs/compiler/compiler_proof.v
+++ b/proofs/compiler/compiler_proof.v
@@ -25,6 +25,7 @@ Require Import
   dead_code_proof
   array_expansion
   array_expansion_proof
+  remove_assert_proof
   remove_globals_proof
   stack_alloc_proof_2
   tunneling_proof
@@ -315,7 +316,8 @@ Lemma compiler_first_partP entries (p: prog) (p': uprog) scs m fn va scs' m' vr
     List.Forall2 value_uincl vr vr' &
     sem_call (dc:=direct_c) p' tt scs m fn va scs' m' vr'.
 Proof.
-  rewrite /compiler_first_part; t_xrbindP => paw ok_paw pa0.
+  rewrite /compiler_first_part; t_xrbindP => paw.
+  rewrite print_uprogP => ok_paw pa0.
   rewrite !print_uprogP => ok_pa0 pb.
   rewrite print_uprogP => ok_pb pa ok_pa pc ok_pc ok_puc ok_puc'.
   rewrite !print_uprogP => pd ok_pd.
@@ -379,6 +381,8 @@ Proof.
     exact.
   apply: compose_pass_uincl'.
   + by move=> vr'; apply: wi2w_progP; apply ok_paw.
+  apply: compose_pass.
+  + move => vr'; exact: remove_assert_progP.
   apply: compose_pass; first by move => vr'; exact: psem_call_u.
   exists vr => //.
   exact: values_uincl_refl.
diff --git a/proofs/compiler/constant_prop.v b/proofs/compiler/constant_prop.v
index 4f666258a1..a11938ae13 100644
--- a/proofs/compiler/constant_prop.v
+++ b/proofs/compiler/constant_prop.v
@@ -496,6 +496,10 @@ Fixpoint const_prop_ir (m:cpm) ii (ir:instr_r) : cpm * cmd :=
     let (m,xs) := const_prop_rvs without_globals m xs in
     (m, [:: MkI ii (Csyscall xs o es) ])
 
+  | Cassert a =>
+    let b := const_prop_e without_globals m a.2 in
+    (m, [:: MkI ii (Cassert (a.1, b)) ])
+
   | Cif b c1 c2 =>
     let b := const_prop_e without_globals m b in
     match is_bool b with
diff --git a/proofs/compiler/constant_prop_proof.v b/proofs/compiler/constant_prop_proof.v
index c5df8ab774..2b0e464f17 100644
--- a/proofs/compiler/constant_prop_proof.v
+++ b/proofs/compiler/constant_prop_proof.v
@@ -892,6 +892,14 @@ Section PROPER.
     by do 3 f_equal; apply: map_ext => z _; rewrite Heq.
   Qed.
 
+  Local Lemma Wassert a : Pr (Cassert a).
+  Proof.
+    move=> ii m1 m2 Heq /=.
+    rewrite /const_prop_ir.
+    split => //=; rewrite /RelationPairs.RelCompFun /=.
+    by do 4 f_equal; rewrite Heq.
+  Qed.
+
   Local Lemma Wif e c1 c2: Pc c1 -> Pc c2 -> Pr (Cif e c1 c2).
   Proof.
     move=> Hc1 Hc2 ii m1 m2 Heq /=.
@@ -949,7 +957,7 @@ Lemma const_prop_i_m :
 Proof.
   move=> g _ <- m1 m2 Hm i1 i2 <-.
   exact:
-    (instr_Rect (Wmk (gd:=g)) (Wnil g) (Wcons (gd:=g)) (Wasgn g) (Wopn g) (Wsyscall g)
+    (instr_Rect (Wmk (gd:=g)) (Wnil g) (Wcons (gd:=g)) (Wasgn g) (Wopn g) (Wsyscall g) (Wassert g)
        (Wif (gd:=g)) (Wfor (gd:=g)) (Wwhile (gd:=g)) (Wcall g)).
 Qed.
 
@@ -958,7 +966,7 @@ Lemma const_prop_i_r_m :
 Proof.
   move=> g _ <- m1 m2 Hm ii1 ii2 <- i1 i2 <-.
   exact:
-    (instr_r_Rect (Wmk (gd:=g)) (Wnil g) (Wcons (gd:=g)) (Wasgn g) (Wopn g) (Wsyscall g)
+    (instr_r_Rect (Wmk (gd:=g)) (Wnil g) (Wcons (gd:=g)) (Wasgn g) (Wopn g) (Wsyscall g) (Wassert g)
        (Wif (gd:=g)) (Wfor (gd:=g)) (Wwhile (gd:=g)) (Wcall g)).
 Qed.
 
@@ -967,7 +975,7 @@ Lemma const_prop_m g :
 Proof.
   move=> m1 m2 Hm c1 c2 <-.
   exact:
-    (cmd_rect (Wmk (gd:=g)) (Wnil g) (Wcons (gd:=g)) (Wasgn g) (Wopn g) (Wsyscall g)
+    (cmd_rect (Wmk (gd:=g)) (Wnil g) (Wcons (gd:=g)) (Wasgn g) (Wopn g) (Wsyscall g) (Wassert g)
        (Wif (gd:=g)) (Wfor (gd:=g)) (Wwhile (gd:=g)) (Wcall g)).
 Qed.
 
@@ -1532,6 +1540,8 @@ Local Opaque opp_word.
   + move=> xs o es ii m /=.
     rewrite (surjective_pairing (const_prop_rvs _ _ _)) /=.
     by apply wequiv_syscall_rel_uincl with checker_cp m.
+  + move=> a ii m /=.
+    by apply wequiv_assert_rel_uincl with checker_cp.
   + move=> e c1 c2 hc1 hc2 ii m /=.
     case heq : is_bool => [b|].
     + apply wequiv_if_rcond with b.
diff --git a/proofs/compiler/dead_calls.v b/proofs/compiler/dead_calls.v
index dccb2b9ee7..8eb8039713 100644
--- a/proofs/compiler/dead_calls.v
+++ b/proofs/compiler/dead_calls.v
@@ -26,7 +26,7 @@ with i_calls_r (c : Sf.t) (i : instr_r) {struct i} : Sf.t :=
   in
 
   match i with
-  | Cassgn _ _ _ _ | Copn _ _ _ _ | Csyscall _ _ _ => c
+  | Cassgn _ _ _ _ | Copn _ _ _ _ | Csyscall _ _ _ | Cassert _ => c
   | Cif    _  c1 c2   => c_calls (c_calls c c1) c2
   | Cfor   _  _  c1   => c_calls c c1
   | Cwhile _ c1 _ _ c2 => c_calls (c_calls c c1) c2
diff --git a/proofs/compiler/dead_calls_proof.v b/proofs/compiler/dead_calls_proof.v
index c36a2ce493..9815575245 100644
--- a/proofs/compiler/dead_calls_proof.v
+++ b/proofs/compiler/dead_calls_proof.v
@@ -30,6 +30,7 @@ with i_Calls_r (i : instr_r) {struct i} : Sf.t :=
   | Cassgn _ _ _ _
   | Copn   _ _ _ _
   | Csyscall _ _ _
+  | Cassert _
     => Sf.empty
   | Cif    _  c1 c2   => Sf.union (c_Calls c1) (c_Calls c2)
   | Cfor   _  _  c1   => c_Calls c1
@@ -98,14 +99,12 @@ Lemma c_callsE c i : Sf.Equal (c_calls c i) (Sf.union c (c_Calls i)).
 Proof.
 move: c.
 apply: (cmd_rect (Pr := Pr) (Pi := Pi) (Pc := Pc)) => /=
-  [ i0 ii Hi | | i0 c0 Hi Hc | x t ty e | xs t o es | xs o es | e c1 c2 Hc1 Hc2
+  [ i0 ii Hi | | i0 c0 Hi Hc | x t ty e | xs t o es | xs o es | a | e c1 c2 Hc1 Hc2
     | v dir lo hi c0 Hc | a c0 e ei c' Hc Hc' | ii xs f es ] c /=.
 + by apply Hi.
 + rewrite CallsE; SfD.fsetdec.
 + rewrite CallsE Hc Hi; SfD.fsetdec.
-+ SfD.fsetdec.
-+ SfD.fsetdec.
-+ SfD.fsetdec.
+1-4: SfD.fsetdec.
 + rewrite /i_calls_r  -/(foldl _ _) -/(foldl _ _) -/(c_calls _ _) -/(c_calls _ _)
     Hc2 Hc1 -/(c_Calls _) -/(c_Calls _); SfD.fsetdec.
 + by apply Hc.
@@ -388,6 +387,7 @@ Section PROOF.
     + by move=> > _; apply wequiv_assgn_rel_eq with checker_st_eq tt.
     + by move=> > _; apply wequiv_opn_rel_eq with checker_st_eq tt.
     + by move=> > _; apply wequiv_syscall_rel_eq with checker_st_eq tt.
+    + by move=> > _; apply wequiv_assert_rel_eq with checker_st_eq.
     + move=> > hc1 hc2 ii; rewrite !CallsE => /def_incl_union [??].
       apply wequiv_if_rel_eq with checker_st_eq tt tt tt => //.
       + by apply hc1.
diff --git a/proofs/compiler/dead_code.v b/proofs/compiler/dead_code.v
index 973c571538..b8e7079965 100644
--- a/proofs/compiler/dead_code.v
+++ b/proofs/compiler/dead_code.v
@@ -128,6 +128,8 @@ Fixpoint dead_code_i (i:instr) (s:Sv.t) {struct i} : cexec (Sv.t * cmd) :=
   | Csyscall xs o es =>
     ok (read_es_rec (read_rvs_rec (Sv.diff s (vrvs xs)) xs) es, [:: i])
 
+  | Cassert a => ok (read_e_rec s a.2 , [::i])
+
   | Cif b c1 c2 =>
     Let sc1 := dead_code_c dead_code_i c1 s in
     Let sc2 := dead_code_c dead_code_i c2 s in
diff --git a/proofs/compiler/dead_code_proof.v b/proofs/compiler/dead_code_proof.v
index cb8b3ea412..04cd7e2630 100644
--- a/proofs/compiler/dead_code_proof.v
+++ b/proofs/compiler/dead_code_proof.v
@@ -655,6 +655,9 @@ Section PROOF.
       apply wequiv_syscall_rel_uincl with checker_st_uincl_on I => //=; subst I.
       + by split => //; rewrite read_esE; SvD.fsetdec.
       by split => //; rewrite read_esE read_rvsE; SvD.fsetdec.
+    + move=> /= a ii I c' O [hI <-].
+      apply wequiv_assert_rel_uincl with checker_st_uincl_on => //=; subst I.
+      by split => //; rewrite read_eE; SvD.fsetdec.
     + move=> e c1 c2 hc1 hc2 ii I c' O /=; t_xrbindP.
       move=> [I1 c1'] /hc1{}hc1 [I2 c2'] /hc2{}hc2 [??]; subst I c'.
       apply wequiv_if_rel_uincl with checker_st_uincl_on (read_e_rec (Sv.union I1 I2) e) O O => //=.
diff --git a/proofs/compiler/direct_call_proof.v b/proofs/compiler/direct_call_proof.v
index 2f9f4c0b67..f17fca6d3d 100644
--- a/proofs/compiler/direct_call_proof.v
+++ b/proofs/compiler/direct_call_proof.v
@@ -337,6 +337,7 @@ Proof.
   + by move=> xs tg o es ii; apply wequiv_opn_rel_uincl with checker_st_uincl tt.
   + move=> xs sc es ii; apply wequiv_syscall_rel_uincl_core with checker_st_uincl tt => //.
     by apply fs_uincl_syscall.
+  + by move=> >; apply wequiv_noassert.
   + by move=> e c1 c2 hc1 hc2 ii; apply wequiv_if_rel_uincl with checker_st_uincl tt tt tt.
   + by move=> > hc ii; apply wequiv_for_rel_uincl with checker_st_uincl tt tt.
   + by move=> > ?? ii; apply wequiv_while_rel_uincl with checker_st_uincl tt.
diff --git a/proofs/compiler/inline.v b/proofs/compiler/inline.v
index 1b2e7c975f..148ae67e66 100644
--- a/proofs/compiler/inline.v
+++ b/proofs/compiler/inline.v
@@ -80,6 +80,7 @@ Fixpoint inline_i (p:ufun_decls) (i:instr) (X:Sv.t) : cexec (Sv.t * cmd) :=
   | Cassgn _ _ _ _
   | Copn _ _ _ _
   | Csyscall _ _ _
+  | Cassert _
     => ok (Sv.union (read_i ir) X, [::i])
   | Cif e c1 c2  =>
     Let c1 := inline_c (inline_i p) c1 X in
diff --git a/proofs/compiler/inline_proof.v b/proofs/compiler/inline_proof.v
index 7549716c0c..929a20f3c6 100644
--- a/proofs/compiler/inline_proof.v
+++ b/proofs/compiler/inline_proof.v
@@ -50,9 +50,7 @@ Section INCL.
     apply: (cmd_rect (Pr := Pr) (Pi := Pi) (Pc := Pc)) => // {c}.
     + move=> i c Hi Hc X1 c' X2 /=.
       by t_xrbindP => -[Xc cc] /Hc -> /= -[Xi ci] /Hi -> /= -> <-.
-    + by move=> * ?.
-    + by move=> * ?.
-    + by move=> * ?.
+    1-4: by move=> * ?.
     + move=> e c1 c2 Hc1 Hc2 ii X1 c' X2 /=.
       by t_xrbindP => -[Xc1 c1'] /Hc1 -> /= -[Xc2 c2'] /Hc2 -> /= <- <-.
     + move=> i dir lo hi c Hc ii X1 c0 X2 /=.
@@ -157,6 +155,9 @@ Section SUBSET.
   Local Lemma Ssyscall   : forall xs o es, Pr (Csyscall xs o es).
   Proof. by move=> ??? ii X2 Xc /= [<-]. Qed.
 
+  Local Lemma Sassert : forall a, Pr (Cassert a).
+  Proof. by move=> ? ii X2 Xc /= [<-]. Qed.
+
   Local Lemma Sif    : forall e c1 c2, Pc c1 -> Pc c2 -> Pr (Cif e c1 c2).
   Proof.
     move=> e c1 c2 Hc1 Hc2 ii X2 Xc /=.
@@ -182,19 +183,19 @@ Section SUBSET.
 
   Lemma inline_c_subset c : Pc c.
   Proof.
-    exact: (cmd_rect Smk Snil Scons Sasgn Sopn Ssyscall Sif Sfor Swhile Scall).
+    exact: (cmd_rect Smk Snil Scons Sasgn Sopn Ssyscall Sassert Sif Sfor Swhile Scall).
   Qed.
 
   Lemma inline_i_subset i : Pr i.
   Proof.
     exact:
-      (instr_r_Rect Smk Snil Scons Sasgn Sopn Ssyscall Sif Sfor Swhile Scall).
+      (instr_r_Rect Smk Snil Scons Sasgn Sopn Ssyscall Sassert Sif Sfor Swhile Scall).
   Qed.
 
   Lemma inline_i'_subset i : Pi i.
   Proof.
     exact:
-      (instr_Rect Smk Snil Scons Sasgn Sopn Ssyscall Sif Sfor Swhile Scall).
+      (instr_Rect Smk Snil Scons Sasgn Sopn Ssyscall Sassert Sif Sfor Swhile Scall).
   Qed.
 
 End SUBSET.
@@ -724,6 +725,7 @@ Proof.
   + move=> xs o es ii X1 X2 _ [? <-].
     by apply wequiv_syscall_rel_uincl with checker_st_uincl_on X1 => //=; subst X1; split => //;
       rewrite !read_writeE; SvD.fsetdec.
+  + by move=> ? ii ??? _; apply wequiv_noassert.
   + move=> e c1 c2 hc1 hc2 ii X1 X2 c_; t_xrbindP.
     move=> [X11 c1'] /hc1{}hc1 [X12 c2'] /hc2{}hc2 ? <-.
     apply wequiv_if_rel_uincl with checker_st_uincl_on X1 X2 X2 => //=; subst X1.
diff --git a/proofs/compiler/insert_renaming_proof.v b/proofs/compiler/insert_renaming_proof.v
index 758456f360..0f2df7f460 100644
--- a/proofs/compiler/insert_renaming_proof.v
+++ b/proofs/compiler/insert_renaming_proof.v
@@ -381,6 +381,7 @@ Section WITH_PARAMS.
       - by move => x tg ty e ii; apply wequiv_assgn_rel_uincl with checker_st_uincl tt.
       - by move=> xs tg o es ii; apply wequiv_opn_rel_uincl with checker_st_uincl tt.
       - by move=> xs sc es ii; apply wequiv_syscall_rel_uincl with checker_st_uincl tt.
+      - by move=> a ii; apply wequiv_assert_rel_uincl with checker_st_uincl.
       - by move=> e c1 c2 hc1 hc2 ii; apply wequiv_if_rel_uincl with checker_st_uincl tt tt tt.
       - by move=> > hc ii; apply wequiv_for_rel_uincl with checker_st_uincl tt tt.
       - by move=> > ?? ii; apply wequiv_while_rel_uincl with checker_st_uincl tt.
diff --git a/proofs/compiler/it_compiler_proof.v b/proofs/compiler/it_compiler_proof.v
index e28cdc5be0..3c7eeba746 100644
--- a/proofs/compiler/it_compiler_proof.v
+++ b/proofs/compiler/it_compiler_proof.v
@@ -32,6 +32,7 @@ Require Import
   dead_code_proof
   array_expansion
   array_expansion_proof
+  remove_assert_proof
   remove_globals_proof
   stack_alloc_proof_2
   tunneling_proof
@@ -164,11 +165,13 @@ Lemma it_compiler_first_part {entries p p' ev fn} :
   compiler_first_part aparams cparams entries p = ok p' ->
   fn \in entries ->
   wiequiv_f
+    (wa1 := withassert) (wa2 := noassert)
     (wsw1 := nosubword) (wsw2 := withsubword)
     (dc1 := indirect_c) (dc2 := direct_c)
     p p' ev ev pre_eq fn fn post_incl.
 Proof.
-rewrite /compiler_first_part; t_xrbindP => paw ok_paw pa0.
+rewrite /compiler_first_part; t_xrbindP => paw.
+rewrite print_uprogP => ok_paw pa0.
 rewrite !print_uprogP => ok_pa0 pb.
 rewrite print_uprogP => ok_pb pa ok_pa pc ok_pc ok_puc ok_puc'.
 rewrite !print_uprogP => pd ok_pd.
@@ -180,13 +183,11 @@ rewrite !print_uprogP => plc ok_plc.
 rewrite !print_uprogP => ok_fvars pj ok_pj pp.
 rewrite !print_uprogP => ok_pp <- {p'} ok_fn.
 
-apply: (
-  wiequiv_f_trans
-    (wsw1 := nosubword) (wsw2 := withsubword) (wsw3 := withsubword)
-    rpreF_trans_eq_eq_eq
-    rpostF_trans_eq_eq_eq_uincl
-    (it_psem_call_u p ev (fn := fn))
-).
+apply: (wiequiv_f_trans_EE_EU (wsw2:=nosubword) (dc2:=indirect_c)).
++ by apply: (it_remove_assert_progP (dc:=indirect_c) (sip:=sip_of_asm_e) (pT:=progUnit) (wsw:=nosubword) ev).
+
+apply: (wiequiv_f_trans_EE_EU (wsw2:= withsubword) (dc2:=indirect_c)).
++ exact: it_psem_call_u.
 
 apply: wiequiv_f_trans_UU_EU; first exact (it_wi2w_progP _ _ ok_paw).
 apply: wiequiv_f_trans_UU_EU; first exact: (it_insert_renaming_callP (insert_renaming cparams)).
@@ -369,6 +370,7 @@ Lemma it_compiler_front_endP ev fn :
   fn \in entries ->
   wiequiv_f
     (wsw1 := nosubword) (wsw2 := withsubword)
+    (wa1 := withassert) (wa2 := noassert)
     (dc1 := indirect_c) (dc2 := direct_c)
     up sp ev rip rpreF fn fn rpostF.
 Proof.
diff --git a/proofs/compiler/linearization.v b/proofs/compiler/linearization.v
index 542b95cf57..813f9255b0 100644
--- a/proofs/compiler/linearization.v
+++ b/proofs/compiler/linearization.v
@@ -451,6 +451,8 @@ Definition pop_to_save
       allM (check_rexpr ii) es >> allM (check_lexpr ii) xs
     | Csyscall xs o es =>
       ok tt
+    | Cassert _ =>
+      Error (E.ii_error ii "assert found in linear")
     | Cif b c1 c2 =>
       check_fexpr ii b >> check_c check_i c1 >> check_c check_i c2
     | Cfor _ _ _ =>
@@ -655,6 +657,8 @@ Fixpoint linear_i (i:instr) (lbl:label) (lc:lcmd) :=
 
   | Csyscall xs o es => (lbl, MkLI ii (Lsyscall o) :: lc)
 
+  | Cassert _ => (lbl, lc) (* absurd case *)
+
   | Cif e [::] c2 =>
     let L1 := lbl in
     let lbl := next_lbl L1 in
diff --git a/proofs/compiler/linearization_proof.v b/proofs/compiler/linearization_proof.v
index a306da7832..731d5afecb 100644
--- a/proofs/compiler/linearization_proof.v
+++ b/proofs/compiler/linearization_proof.v
@@ -137,6 +137,10 @@ Section CAT.
   Lemma cat_syscall : forall xs o es, Pr (Csyscall xs o es).
   Proof. by []. Qed.
 
+  #[ local ]
+  Lemma cat_assert : forall a, Pr (Cassert a).
+  Proof. by []. Qed.
+
   #[ local ]
   Lemma cat_if   : forall e c1 c2,  Pc c1 -> Pc c2 -> Pr (Cif e c1 c2).
   Proof.
@@ -185,7 +189,7 @@ Section CAT.
      let: (lbl, lc) := linear_i fn i lbl [::] in (lbl, lc ++ tail).
   Proof.
     exact:
-      (instr_Rect cat_mkI cat_skip cat_seq cat_assgn cat_opn cat_syscall cat_if cat_for cat_while cat_call).
+      (instr_Rect cat_mkI cat_skip cat_seq cat_assgn cat_opn cat_syscall cat_assert cat_if cat_for cat_while cat_call).
   Qed.
 
   Lemma linear_c_nil fn c lbl tail :
@@ -193,7 +197,7 @@ Section CAT.
      let: (lbl, lc) := linear_c (linear_i fn) c lbl [::] in (lbl, lc ++ tail).
   Proof.
     exact:
-      (cmd_rect cat_mkI cat_skip cat_seq cat_assgn cat_opn cat_syscall cat_if cat_for cat_while cat_call).
+      (cmd_rect cat_mkI cat_skip cat_seq cat_assgn cat_opn cat_syscall cat_assert cat_if cat_for cat_while cat_call).
   Qed.
 
 End CAT.
@@ -829,6 +833,10 @@ Section VALIDITY.
   Lemma valid_labels_syscall (xs : lvals) (o : syscall_t) (es : pexprs) : Pr (Csyscall xs o es).
   Proof. move => ?; exact: default. Qed.
 
+  #[ local ]
+  Lemma valid_labels_assert (a : assertion) : Pr (Cassert a).
+  Proof. move=> ?; exact: default. Qed.
+
   #[ local ]
   Lemma valid_labels_if (e : pexpr) (c1 c2 : cmd) : Pc c1 → Pc c2 → Pr (Cif e c1 c2).
   Proof.
@@ -921,10 +929,10 @@ Section VALIDITY.
   Qed.
 
   Definition linear_has_valid_labels : ∀ c, Pc c :=
-    cmd_rect valid_labels_MkI valid_labels_nil valid_labels_cons valid_labels_assign valid_labels_opn valid_labels_syscall valid_labels_if valid_labels_for valid_labels_while valid_labels_call.
+    cmd_rect valid_labels_MkI valid_labels_nil valid_labels_cons valid_labels_assign valid_labels_opn valid_labels_syscall valid_labels_assert valid_labels_if valid_labels_for valid_labels_while valid_labels_call.
 
   Definition linear_has_valid_labels_instr : ∀ i, Pi i :=
-    instr_Rect valid_labels_MkI valid_labels_nil valid_labels_cons valid_labels_assign valid_labels_opn valid_labels_syscall valid_labels_if valid_labels_for valid_labels_while valid_labels_call.
+    instr_Rect valid_labels_MkI valid_labels_nil valid_labels_cons valid_labels_assign valid_labels_opn valid_labels_syscall valid_labels_assert valid_labels_if valid_labels_for valid_labels_while valid_labels_call.
 
 End VALIDITY.
 
@@ -988,6 +996,10 @@ Section NUMBER_OF_LABELS.
   Lemma nb_labels_syscall (xs : lvals) (o : syscall_t) (es : pexprs) : Pr (Csyscall xs o es).
   Proof. by move=> ii fn lbl /=; apply Z.le_refl. Qed.
 
+  #[ local ]
+  Lemma nb_labels_assert (a : assertion) : Pr (Cassert a).
+  Proof. by move => ii fn lbl /=; apply Z.le_refl. Qed.
+
   #[ local ]
   Lemma nb_labels_if (e : pexpr) (c1 c2 : cmd) : Pc c1 → Pc c2 → Pr (Cif e c1 c2).
   Proof.
@@ -1078,10 +1090,10 @@ Section NUMBER_OF_LABELS.
   Qed.
 
   Definition linear_c_nb_labels : ∀ c, Pc c :=
-    cmd_rect nb_labels_MkI nb_labels_nil nb_labels_cons nb_labels_assign nb_labels_opn nb_labels_syscall nb_labels_if nb_labels_for nb_labels_while nb_labels_call.
+    cmd_rect nb_labels_MkI nb_labels_nil nb_labels_cons nb_labels_assign nb_labels_opn nb_labels_syscall nb_labels_assert nb_labels_if nb_labels_for nb_labels_while nb_labels_call.
 
   Definition linear_i_nb_labels : ∀ i, Pi i :=
-    instr_Rect nb_labels_MkI nb_labels_nil nb_labels_cons nb_labels_assign nb_labels_opn nb_labels_syscall nb_labels_if nb_labels_for nb_labels_while nb_labels_call.
+    instr_Rect nb_labels_MkI nb_labels_nil nb_labels_cons nb_labels_assign nb_labels_opn nb_labels_syscall nb_labels_assert nb_labels_if nb_labels_for nb_labels_while nb_labels_call.
 
   Lemma linear_body_nb_labels fn fi e body :
     let: (lbl, lc) := linear_body liparams p fn fi e body in
diff --git a/proofs/compiler/load_constants_in_cond.v b/proofs/compiler/load_constants_in_cond.v
index 482ee90373..ae6e311a37 100644
--- a/proofs/compiler/load_constants_in_cond.v
+++ b/proofs/compiler/load_constants_in_cond.v
@@ -81,6 +81,7 @@ Fixpoint load_constants_i (i : instr) :=
   | Cassgn _ _ _ _
   | Copn _ _ _ _
   | Csyscall _ _ _
+  | Cassert _
   | Ccall _ _ _
     => ok [::i]
   | Cif e c1 c2  =>
diff --git a/proofs/compiler/load_constants_in_cond_proof.v b/proofs/compiler/load_constants_in_cond_proof.v
index f6f9c57d86..bc137eaf58 100644
--- a/proofs/compiler/load_constants_in_cond_proof.v
+++ b/proofs/compiler/load_constants_in_cond_proof.v
@@ -453,6 +453,7 @@ Proof.
     by apply wequiv_opn_rel_eq with checker_st_eq_on X => //=; split=> //; SvD.fsetdec.
   + move=> xs sc es ii _ [<-]; rewrite !read_writeE => hsub.
     by apply wequiv_syscall_rel_eq with checker_st_eq_on X => //=; split=> //; SvD.fsetdec.
+  + by move=> *; apply wequiv_noassert.
   + move=> e c1 c2 hc1 hc2 ii c_; t_xrbindP.
     move=> [c e'] hcond; t_xrbindP => c1' hc1' c2' hc2' <-; rewrite !read_writeE => hsub.
     rewrite map_cat.
diff --git a/proofs/compiler/lower_spill.v b/proofs/compiler/lower_spill.v
index c0f88d1cd1..b73d8a3568 100644
--- a/proofs/compiler/lower_spill.v
+++ b/proofs/compiler/lower_spill.v
@@ -45,7 +45,7 @@ Fixpoint to_spill_i (s : Sv.t * bool) (i : instr) :=
     | Some (Unspill, _) => (s.1, true)
     | _ => s
     end
-  | Csyscall _ _ _ => s
+  | Csyscall _ _ _ | Cassert _ => s
   | Cif _ c1 c2 => foldl to_spill_i (foldl to_spill_i s c1) c2
   | Cfor _ _ c => foldl to_spill_i s c
   | Cwhile _ c1 _ _ c2 => foldl to_spill_i (foldl to_spill_i s c1) c2
@@ -163,6 +163,7 @@ Fixpoint spill_i (env : spill_env) (i : instr) : cexec (spill_env * cmd) :=
     | None                => ok (update_lvs env lvs, [::i])
     end
   | Csyscall lvs c es => ok (update_lvs env lvs, [::i])
+  | Cassert _ => ok (env, [::i])
   | Cif e c1 c2 =>
     Let ec1 := spill_c spill_i env c1 in
     Let ec2 := spill_c spill_i env c2 in
diff --git a/proofs/compiler/lower_spill_proof.v b/proofs/compiler/lower_spill_proof.v
index fb261abd98..7490b6a968 100644
--- a/proofs/compiler/lower_spill_proof.v
+++ b/proofs/compiler/lower_spill_proof.v
@@ -784,6 +784,9 @@ Proof.
     apply wequiv_syscall_rel_eq with (checker_st_ve S) env => //.
     + by split => //; SvD.fsetdec.
     split => //; SvD.fsetdec.
+  + move=> a ii env env' c' [<- <-]; rewrite vars_I_assert => hsub.
+    apply wequiv_assert_rel_eq with (checker_st_ve S) => //.
+    by split => //; SvD.fsetdec.
   + move=> e c1 c2 hc1 hc2 ii env env' c' /=; t_xrbindP.
     move=> [env1 c1'] hc1' [env2 c2'] hc2' <- <-.
     rewrite vars_I_if => hsub.
diff --git a/proofs/compiler/makeReferenceArguments.v b/proofs/compiler/makeReferenceArguments.v
index b89492d07f..47820678d2 100644
--- a/proofs/compiler/makeReferenceArguments.v
+++ b/proofs/compiler/makeReferenceArguments.v
@@ -150,7 +150,8 @@ Fixpoint update_i (X:Sv.t) (i:instr) : cexec cmd :=
         let tg := if [&& size prologue == 2 & size epilogue == 2] then AT_inline else tg in
         ok (prologue ++ MkI ii (Copn xs tg (Opseudo_op (pseudo_operator.Oswap ty)) es) :: epilogue)
       else ok [:: i ]
-  | Cassgn _ _ _ _ => ok [:: i ]
+  | Cassgn _ _ _ _
+  | Cassert _ => ok [:: i ]
   | Cif b c1 c2 =>
     Let c1 := update_c (update_i X) c1 in
     Let c2 := update_c (update_i X) c2 in
diff --git a/proofs/compiler/makeReferenceArguments_proof.v b/proofs/compiler/makeReferenceArguments_proof.v
index de9db5660f..ff914ebf5d 100644
--- a/proofs/compiler/makeReferenceArguments_proof.v
+++ b/proofs/compiler/makeReferenceArguments_proof.v
@@ -771,6 +771,9 @@ Context
       move=> ? hes ? [[??]?] /= ho [<-] /= hw.
       have [vm2 ??] := sem_syscall_update_i hes ho hw hup hsub heq.
       by exists (with_vm t vm2).
+    + move=> a ii X c' /= [<-]; rewrite !read_writeE => hsub.
+      apply wequiv_assert_rel_eq with checker_st_eq_on => //.
+      by split => //; SvD.fsetdec.
     + move=> e c1 c2 hc1 hc2 ii X c' /=; t_xrbindP.
       move=> c1' hc1' c2' hc2' <-; rewrite !read_writeE => hsub.
       apply wequiv_if_rel_eq with checker_st_eq_on X X X => //.
diff --git a/proofs/compiler/merge_varmaps.v b/proofs/compiler/merge_varmaps.v
index ce7a82c80e..7bcf23638d 100644
--- a/proofs/compiler/merge_varmaps.v
+++ b/proofs/compiler/merge_varmaps.v
@@ -67,6 +67,7 @@ Section WRITE1.
     | Cassgn x _ _ _  => vrv_rec s x
     | Copn xs _ _ _   => vrvs_rec s xs
     | Csyscall xs o _ => vrvs_rec (Sv.union s syscall_kill) (to_lvals (syscall_sig o).(scs_vout))
+    | Cassert _       => s
     | Cif   _ c1 c2   => foldl write_I_rec (foldl write_I_rec s c2) c1
     | Cfor  x _ c     => foldl write_I_rec (Sv.add x s) c
     | Cwhile _ c _ _ c' => foldl write_I_rec (foldl write_I_rec s c') c
@@ -173,6 +174,8 @@ Section CHECK.
         (E.internal_error ii "bad syscall dests") in
       let W := syscall_kill in
       ok (Sv.diff (Sv.union D W) (vrvs (to_lvals (syscall_sig o).(scs_vout))))
+    | Cassert _ =>
+      Error (E.internal_error ii "assert remain")
     | Cif b c1 c2 =>
       Let _ := check_e ii D b in
       Let D1 := check_c (check_i sz) D c1 in
diff --git a/proofs/compiler/merge_varmaps_proof.v b/proofs/compiler/merge_varmaps_proof.v
index 54b5c7368c..afc8283e7d 100644
--- a/proofs/compiler/merge_varmaps_proof.v
+++ b/proofs/compiler/merge_varmaps_proof.v
@@ -174,6 +174,7 @@ Section LEMMA.
     - by move => x tg ty e s; rewrite /write_i /write_i_rec -vrv_recE.
     - by move => xs tg op es s; rewrite /write_i /write_i_rec -vrvs_recE.
     - by move => xs op es s; rewrite /write_i /write_i_rec !vrvs_recE; SvD.fsetdec.
+    - by move=> a s; rewrite /write_i /write_i_rec; SvD.fsetdec.
     - by move => e c1 c2 h1 h2 s; rewrite /write_i /write_i_rec -!/write_c_rec -/write_c !h1 h2; SvD.fsetdec.
     - by move => v d lo hi body h s; rewrite /write_i /write_i_rec -!/write_c_rec !h; SvD.fsetdec.
     - by move => a c1 e ei c2  h1 h2 s; rewrite /write_i /write_i_rec -!/write_c_rec -/write_c !h1 h2; SvD.fsetdec.
diff --git a/proofs/compiler/post_unrolling_check.v b/proofs/compiler/post_unrolling_check.v
index adf65c4dfe..2418b994f1 100644
--- a/proofs/compiler/post_unrolling_check.v
+++ b/proofs/compiler/post_unrolling_check.v
@@ -40,7 +40,7 @@ End CHECK_NO_FOR_LOOP_CMD.
 
 Fixpoint check_no_for_loop_instr_r i : cexec unit :=
   match i with
-  | (Cassgn _ _ _ _ | Copn _ _ _ _ | Csyscall _ _ _ | Ccall _ _ _)
+  | (Cassgn _ _ _ _ | Copn _ _ _ _ | Csyscall _ _ _ | Cassert _ | Ccall _ _ _)
     => ok tt
   | (Cif _ c c' | Cwhile _ c _ _ c') =>
       check_no_for_loop_cmd check_no_for_loop_instr c >> check_no_for_loop_cmd check_no_for_loop_instr c'
@@ -61,7 +61,7 @@ Definition check_no_inline_instr_cmd (i: instr → cexec unit) (c: cmd) := allM
 
 Fixpoint check_no_inline_instr_instr_r i : cexec unit :=
   match i with
-  | (Cassgn _ _ _ _ | Copn _ _ _ _ | Csyscall _ _ _ | Cfor _ _ _ | Ccall _ _ _)
+  | (Cassgn _ _ _ _ | Copn _ _ _ _ | Csyscall _ _ _ | Cassert _ | Cfor _ _ _ | Ccall _ _ _)
       => ok tt
   | (Cif _ c c' | Cwhile _ c _ _ c') =>
       check_no_inline_instr_cmd check_no_inline_instr_instr c >> check_no_inline_instr_cmd check_no_inline_instr_instr c'
diff --git a/proofs/compiler/propagate_inline.v b/proofs/compiler/propagate_inline.v
index 5091579861..94a6614e70 100644
--- a/proofs/compiler/propagate_inline.v
+++ b/proofs/compiler/propagate_inline.v
@@ -172,7 +172,11 @@ Fixpoint pi_i (pi:pimap) (i:instr) :=
     let (pi, xs) := pi_lvs pi xs in
     ok (pi, MkI ii (Csyscall xs o es))
 
-  | Cif e c1 c2 => 
+  | Cassert (msg, e) =>
+    let e := pi_e pi e in
+    ok (pi, MkI ii (Cassert (msg, e)))
+
+  | Cif e c1 c2 =>
     let e := pi_e pi e in
     Let pic1 := pi_c pi_i pi c1 in
     Let pic2 := pi_c pi_i pi c2 in
diff --git a/proofs/compiler/propagate_inline_proof.v b/proofs/compiler/propagate_inline_proof.v
index 87c4c42206..88734ffe27 100644
--- a/proofs/compiler/propagate_inline_proof.v
+++ b/proofs/compiler/propagate_inline_proof.v
@@ -868,6 +868,8 @@ Section PROOF.
         by apply/valid_pi_with_scs/valid_pi_remove_m.
       + by rewrite /check_lvals /= /check_lvals_pi heq.
       by apply fs_uincl_syscall.
+    + case => msg e ii d _ /ok_inj<-.
+      by apply wequiv_assert_rel_uincl with checker_pi.
     + move=> e c1 c2 hc1 hc2 ii d di /=; t_xrbindP => di1 /hc1{}hc1 di2 /hc2{}hc2 <- /=.
       apply wequiv_if_rel_uincl_R with checker_pi d di1.1 di2.1 => //.
       + by apply/st_pi_incl/incl_merge_l.
diff --git a/proofs/compiler/remove_assert.v b/proofs/compiler/remove_assert.v
new file mode 100644
index 0000000000..cec500fef0
--- /dev/null
+++ b/proofs/compiler/remove_assert.v
@@ -0,0 +1,49 @@
+From Coq Require Import ssreflect.
+Require Import expr compiler_util ZArith.
+
+Section ASM_OP.
+
+Context `{asmop : asmOp}.
+
+Definition remove_assert_c (remove_assert_i: instr -> cmd) c :  cmd :=
+  foldr (fun i r =>
+    let i := remove_assert_i i in
+     i ++ r) [::] c.
+
+Fixpoint remove_assert_i (i: instr) : cmd :=
+  let 'MkI ii ir := i in
+  match ir with
+  | Cassert _ => [::]
+  | Cassgn _ _ _ _
+  | Copn _ _ _ _ | Csyscall _ _ _ | Ccall _ _ _ =>
+    [:: i]
+  | Cif e c1 c2 =>
+    let c1 := remove_assert_c remove_assert_i c1 in
+    let c2 := remove_assert_c remove_assert_i c2 in
+    [:: MkI ii (Cif e c1 c2)]
+  | Cwhile al c1 e ii' c2 =>
+    let c1 := remove_assert_c remove_assert_i c1 in
+    let c2 := remove_assert_c remove_assert_i c2 in
+    [:: MkI ii (Cwhile al c1 e ii' c2)]
+  | Cfor x (d, e1, e2) c =>
+    let c := remove_assert_c remove_assert_i c in
+    [:: MkI ii (Cfor x (d, e1, e2) c)]
+  end.
+
+Context {pT:progT}.
+
+Definition remove_assert_fd (fd: fundef) :=
+  let c := remove_assert_c remove_assert_i fd.(f_body) in
+  {| f_info   := fd.(f_info);
+     f_tyin   := fd.(f_tyin);
+     f_params := fd.(f_params);
+     f_body   := c;
+     f_tyout  := fd.(f_tyout);
+     f_res    := fd.(f_res);
+     f_extra  := fd.(f_extra);
+  |}.
+
+Definition remove_assert_prog (p: prog) : prog :=
+  map_prog remove_assert_fd p.
+
+End ASM_OP.
diff --git a/proofs/compiler/remove_assert_proof.v b/proofs/compiler/remove_assert_proof.v
new file mode 100644
index 0000000000..15b62e9fdc
--- /dev/null
+++ b/proofs/compiler/remove_assert_proof.v
@@ -0,0 +1,225 @@
+From Coq Require Import ssreflect.
+Require Import psem compiler_util.
+Require Export remove_assert.
+Import Utf8 ssrfun.
+
+Section REMOVE_ASSERT.
+
+  Context
+    {wsw:WithSubWord}
+    {dc:DirectCall}
+    {asm_op syscall_state : Type}
+    {ep : EstateParams syscall_state}
+    {spp : SemPexprParams}
+    {sip : SemInstrParams asm_op syscall_state}
+    {pT:progT} {sCP: semCallParams}.
+
+  Context (p p' : prog) (ev: extra_val_t).
+
+  Hypothesis remove_assert_ok : remove_assert_prog p = p'.
+
+  Lemma eq_globs : p_globs p' = p_globs p.
+  Proof. by rewrite -remove_assert_ok. Qed.
+
+  Lemma eq_p_extra : p_extra p' = p_extra p.
+  Proof. by rewrite -remove_assert_ok. Qed.
+
+  Section SEM.
+
+  Let Pi s1 (i: instr) s2 :=
+    forall c, remove_assert_i i = c ->
+    sem p' ev s1 c s2.
+
+  Let Pi_r s1 (i: instr_r) s2 := forall ii, Pi s1 (MkI ii i) s2.
+
+  Let Pc s1 (c: cmd) s2 :=
+    forall c', remove_assert_c remove_assert_i c = c' ->
+    sem p' ev s1 c' s2.
+
+  Let Pfor (i: var_i) vs s1 c s2 :=
+    forall c', remove_assert_c remove_assert_i c = c' ->
+    sem_for p' ev i vs s1 c' s2.
+
+  Let Pfun scs m fn vargs scs' m' vres :=
+    sem_call p' ev scs m fn vargs scs' m' vres.
+
+  Local Lemma Rnil : sem_Ind_nil Pc.
+  Proof. move=> s _ <-; constructor. Qed.
+
+  Local Lemma Rcons : sem_Ind_cons p ev Pc Pi.
+  Proof.
+    move=> s1 s2 s3 i c _ Hi _ Hc c' /= <-; apply: sem_app.
+    + exact: Hi.
+    exact: Hc.
+  Qed.
+
+  Local Lemma RmkI : sem_Ind_mkI p ev Pi_r Pi.
+  Proof. by auto. Qed.
+
+  Local Lemma Rasgn : sem_Ind_assgn p Pi_r.
+  Proof.
+    move=> s1 s2 x tag ty e v v' he htr hw ii c' /= <-.
+    by apply: sem_seq1; constructor; econstructor; eauto; rewrite eq_globs.
+  Qed.
+
+  Local Lemma Ropn : sem_Ind_opn p Pi_r.
+  Proof.
+    move=> s1 s2 t o xs es; rewrite /sem_sopn; t_xrbindP => ?? he hex hw ii _ <-.
+    by apply: sem_seq1; constructor;econstructor;eauto; rewrite /sem_sopn eq_globs he /= hex.
+  Qed.
+
+  Local Lemma Rsyscall : sem_Ind_syscall p Pi_r.
+  Proof.
+    move=> s1 scs m s2 o xs es ves vs he hex hw ii _ <-.
+    by apply: sem_seq1; constructor; econstructor; eauto; rewrite eq_globs.
+  Qed.
+
+  Local Lemma Rif_true : sem_Ind_if_true p ev Pc Pi_r.
+  Proof.
+    move=> s1 s2 e c1 c2 he _ hc ii _ <-.
+    apply sem_seq1; constructor; apply Eif_true.
+    + by rewrite eq_globs.
+    exact: hc.
+  Qed.
+
+  Local Lemma Rif_false : sem_Ind_if_false p ev Pc Pi_r.
+  Proof.
+    move=> s1 s2 e c1 c2 he _ hc ii _ <-.
+    apply sem_seq1; constructor; apply Eif_false.
+    + by rewrite eq_globs.
+    exact: hc.
+  Qed.
+
+  Local Lemma Rwhile_true : sem_Ind_while_true p ev Pc Pi_r.
+  Proof.
+    move=> s1 s2 s3 s4 a c e ei c' _ Hc he _ Hc' _ hw ii _ <-.
+    apply sem_seq1; constructor; eapply Ewhile_true; eauto.
+    + by rewrite eq_globs.
+    have /sem_seq1_iff /sem_IE := hw ii _ erefl.
+    exact.
+  Qed.
+
+  Local Lemma Rwhile_false : sem_Ind_while_false p ev Pc Pi_r.
+  Proof.
+    move=> s1 s2 a c e ei c' _ Hc he ii _ <-.
+    apply sem_seq1; constructor; eapply Ewhile_false; eauto.
+    by rewrite eq_globs.
+  Qed.
+
+  Local Lemma Rfor : sem_Ind_for p ev Pi_r Pfor.
+  Proof.
+    move=> s1 s2 i d lo hi c vlo vhi hlo hhi _ hfor ii _ <-.
+    by apply sem_seq1; constructor; econstructor; eauto; rewrite eq_globs.
+  Qed.
+
+  Local Lemma Rfor_nil : sem_Ind_for_nil Pfor.
+  Proof. move=> s i c c' hc'. constructor. Qed.
+
+  Local Lemma Rfor_cons : sem_Ind_for_cons p ev Pc Pfor.
+  Proof.
+    move=> s1 s1' s2 s3 i w ws c hw _ hc _ hfor c' hcc'; econstructor; eauto.
+  Qed.
+
+  Local Lemma Rcall : sem_Ind_call p ev Pi_r Pfun.
+  Proof.
+    move=> s1 scs2 m2 s2 xs fn es vargs vres hargs _ hfun hw ii _ <-.
+    by apply: sem_seq1; constructor; econstructor; eauto; rewrite eq_globs.
+  Qed.
+
+  Local Lemma Rproc : sem_Ind_proc p ev Pc Pfun.
+  Proof.
+    move=> scs1 m1 scs2 m2 fn fd vargs vargs' s0 s1 s2 vres vres' hget htin hinit hw _ hbody hgetr htout -> ->.
+    econstructor.
+    - rewrite -remove_assert_ok get_map_prog hget /=; reflexivity.
+    all: eauto.
+    by rewrite eq_p_extra.
+  Qed.
+
+  Lemma remove_assert_progP f scs mem scs' mem' va vr:
+    sem_call p ev scs mem f va scs' mem' vr ->
+    sem_call p' ev scs mem f va scs' mem' vr.
+  Proof.
+    exact:
+      (sem_call_Ind
+         Rnil
+         Rcons
+         RmkI
+         Rasgn
+         Ropn
+         Rsyscall
+         Rif_true
+         Rif_false
+         Rwhile_true
+         Rwhile_false
+         Rfor
+         Rfor_nil
+         Rfor_cons
+         Rcall
+         Rproc).
+  Qed.
+
+  End SEM.
+
+  Section IT.
+
+  Context {E E0: Type -> Type} {wE : with_Error E E0} {rE : EventRels E0}.
+
+  #[local] Notation st_eq := (st_rel (λ _ : unit, eq) tt).
+
+  Lemma st_rel_eq d s1 s2 : st_rel (λ _ : unit, eq) d s1 s2 → s1 = s2.
+  Proof. by case: s1 s2 => ??? [] ??? [] /= <- <- <-. Qed.
+
+  Program Instance checker_ra_eq : Checker_e (st_rel (λ _ : unit, eq)) :=
+    {| check_es _ x y _ := x = y; check_lvals _ x y _ := x = y; |}.
+
+  Instance checker_ra_eqP : Checker_eq p p' checker_ra_eq.
+  Proof.
+    rewrite -remove_assert_ok.
+    constructor.
+    - by move => > /wdb_ok_eq <- <- > /st_rel_eq <-; eauto.
+    by move => > /wdb_ok_eq <- <- > /st_rel_eq <- -> /=; eexists; first reflexivity.
+  Qed.
+  #[local] Hint Resolve checker_ra_eqP : core.
+
+  Let Pi (i: instr) :=
+      wequiv_rec (wa1:=withassert) (wa2:=noassert) p p' ev ev eq_spec st_eq [::i] (remove_assert_i i) st_eq.
+
+  Let Pi_r (i: instr_r) := forall ii, Pi (MkI ii i).
+
+  Let Pc (c: cmd) :=
+      wequiv_rec (wa1:=withassert) (wa2:=noassert) p p' ev ev eq_spec st_eq c (remove_assert_c remove_assert_i c) st_eq.
+
+  Lemma it_remove_assert_progP fn :
+    wiequiv_f (wa1 := withassert) (wa2 := noassert) p p' ev ev (rpreF (eS:= eq_spec)) fn fn (rpostF (eS:=eq_spec)).
+  Proof.
+    apply wequiv_fun_ind => {fn}.
+    move=> fn _ fs ft [<- <-] fd hget.
+    rewrite -{1 2}remove_assert_ok get_map_prog hget /=.
+    eexists; first reflexivity.
+    move=> s1 hinit; exists s1 => //=.
+    exists st_eq, st_eq; split; cycle -1.
+    + by move => ? _ fr /st_rel_eq <- hfin; exists fr.
+    + done.
+    move: (f_body fd) => {hget hinit s1 fs ft fn fd}.
+    apply: (cmd_rect (Pr := Pi_r) (Pi := Pi) (Pc := Pc)) => //.
+    + by apply wequiv_nil.
+    + by move=> i c hi hc; rewrite -cat1s; apply wequiv_cat with st_eq.
+    + by move => >; apply wequiv_assgn_rel_eq with checker_ra_eq tt.
+    + by move => >; apply wequiv_opn_rel_eq with checker_ra_eq tt.
+    + move => >; apply wequiv_syscall_rel_eq_core with checker_ra_eq tt => //.
+      by move => > <- ->; eauto.
+    + by move => >; apply wequiv_assert_left.
+    + move=> > hc1 hc2 ii.
+      by apply wequiv_if_rel_eq with checker_ra_eq tt tt tt.
+    + move=> > hc >.
+      by apply wequiv_for_rel_eq with checker_ra_eq tt tt.
+    + move=> > hc hc' >.
+      by apply wequiv_while_rel_eq with checker_ra_eq tt.
+    move=> >.
+    apply wequiv_call_rel_eq with checker_ra_eq tt => //.
+    move=> ?? <-; exact/wequiv_fun_rec.
+  Qed.
+
+  End IT.
+
+End REMOVE_ASSERT.
diff --git a/proofs/compiler/remove_globals.v b/proofs/compiler/remove_globals.v
index 17336409f0..2086f595ac 100644
--- a/proofs/compiler/remove_globals.v
+++ b/proofs/compiler/remove_globals.v
@@ -110,7 +110,7 @@ Section REMOVE.
         else ok gd
       | _ => ok gd
       end
-    | Copn _ _ _ _ | Csyscall _ _ _ | Ccall _ _ _ => ok gd
+    | Copn _ _ _ _ | Csyscall _ _ _ | Cassert _ | Ccall _ _ _ => ok gd
     | Cif _ c1 c2 =>
       Let gd := foldM extend_glob_i gd c1 in
       foldM extend_glob_i gd c2
@@ -301,6 +301,9 @@ Section REMOVE.
           Let lvs := mapM (remove_glob_lv ii env) lvs in
           Let es  := mapM (remove_glob_e ii env) es in
           ok (env, [::MkI ii (Csyscall lvs o es)])
+        | Cassert a =>
+          Let a := sndM (remove_glob_e ii env) a in
+          ok (env, [::MkI ii (Cassert a)])
         | Cif e c1 c2 =>
           Let e := remove_glob_e ii env e in
           Let envc1 := remove_glob remove_glob_i env c1 in
diff --git a/proofs/compiler/remove_globals_proof.v b/proofs/compiler/remove_globals_proof.v
index dffb9a2cb9..4c2e5757bb 100644
--- a/proofs/compiler/remove_globals_proof.v
+++ b/proofs/compiler/remove_globals_proof.v
@@ -261,6 +261,7 @@ Module INCL. Section INCL.
     + by move=> >; apply wequiv_assgn_rel_eq with checker_equal tt.
     + by move=> >; apply wequiv_opn_rel_eq with checker_equal tt.
     + by move=> >; apply wequiv_syscall_rel_eq with checker_equal tt.
+    + by move=> a ii; apply wequiv_assert_rel_eq with checker_equal.
     + by move=> > hc1 hc2 ii; apply wequiv_if_rel_eq with checker_equal tt tt tt.
     + by move=> > hc ii; apply wequiv_for_rel_eq with checker_equal tt tt.
     + by move=> > hc hc' ii; apply wequiv_while_rel_eq with checker_equal tt.
@@ -346,6 +347,9 @@ Section PROOFS.
   Local Lemma Hsyscall : forall xs o es, Pr (Csyscall xs o es).
   Proof. by move=> xs o es ii gd1 gd2 /= [<-]. Qed.
 
+  Local Lemma Hassert : forall a, Pr (Cassert a).
+  Proof. by move=> a ii gd1 gd2 /= [<-]. Qed.
+
   Local Lemma Hif  : forall e c1 c2, Pc c1 -> Pc c2 -> Pr (Cif e c1 c2).
   Proof.
     move=> e c1 c2 hc1 hc2 ii gd1 gd2 /=.
@@ -368,7 +372,7 @@ Section PROOFS.
     foldM (extend_glob_i fresh_id) gd1 c = ok gd2 ->
     gd_incl gd1 gd2.
   Proof.
-    exact: (cmd_rect Hmk Hnil Hcons Hasgn Hopn Hsyscall Hif Hfor Hwhile Hcall).
+    exact: (cmd_rect Hmk Hnil Hcons Hasgn Hopn Hsyscall Hassert Hif Hfor Hwhile Hcall).
   Qed.
 
 End PROOFS.
@@ -1149,6 +1153,9 @@ Module RGP. Section PROOFS.
       apply wequiv_syscall_rel_uincl_core_R with (checker_valid ii) d d => //.
       + by move=> > []. + by move=> > [?????].
       exact: fs_uincl_syscall.
+    + move=> a ii d dc_ /=; rewrite /sndM; t_xrbindP => _ e he <- <-.
+      apply wequiv_assert_rel_uincl with (checker_valid ii) => //.
+      by split => //=; rewrite he.
     + move=> e c1 c2 hc1 hc2 ii d dc_ /=; t_xrbindP.
       move=> e' he' dc1 /hc1{}hc1 dc2 /hc2{}hc2 <- /=.
       apply wequiv_if_rel_uincl_R with (checker_valid ii) d dc1.1 dc2.1 => //.
diff --git a/proofs/compiler/riscv_lower_addressing.v b/proofs/compiler/riscv_lower_addressing.v
index 54119f15b9..ebb10c603e 100644
--- a/proofs/compiler/riscv_lower_addressing.v
+++ b/proofs/compiler/riscv_lower_addressing.v
@@ -77,6 +77,7 @@ Fixpoint lower_addressing_i (i: instr) :=
     else [:: i]
   | Cassgn _ _ _ _
   | Csyscall _ _ _
+  | Cassert _
   | Ccall _ _ _ => [:: i]
   | Cif b c1 c2 =>
     let c1 := conc_map lower_addressing_i c1 in
diff --git a/proofs/compiler/riscv_lower_addressing_proof.v b/proofs/compiler/riscv_lower_addressing_proof.v
index a024d1fb54..2e68f6882f 100644
--- a/proofs/compiler/riscv_lower_addressing_proof.v
+++ b/proofs/compiler/riscv_lower_addressing_proof.v
@@ -483,6 +483,7 @@ Proof.
     by eexists; first apply h.
   + move=> xs sc es ii; rewrite !read_writeE => hsub.
     by apply (wequiv_syscall_rel_eq (sip:=sip)) with checker_st_eq_on X => //=; split=> //; SvD.fsetdec.
+  + by move=> ? ii ?; apply wequiv_noassert with (ev1:=ev) (ii:=ii).
   + move=> e c1 c2 hc1 hc2 ii; rewrite !read_writeE => hsub.
     apply (wequiv_if_rel_eq (sip:=sip)) with checker_st_eq_on X X X => //.
     + by split => //; rewrite /read_es /= read_eE; SvD.fsetdec.
diff --git a/proofs/compiler/riscv_lowering_proof.v b/proofs/compiler/riscv_lowering_proof.v
index 758d32e986..3ef79c6682 100644
--- a/proofs/compiler/riscv_lowering_proof.v
+++ b/proofs/compiler/riscv_lowering_proof.v
@@ -809,6 +809,8 @@ Proof.
   + move=> xs o es ii.
     by apply (wequiv_syscall_rel_eq (sip:=sip)) with
        checker_st_eq tt.
+  (* Assert *)
+  + by move=> ? ii; apply wequiv_noassert with (ev1:=ev) (ii:=ii).
   (* If *)
   + move=> e c1 c2 hc1 hc2 ii /=.
     by apply (wequiv_if_rel_eq (sip:=sip)) with checker_st_eq tt tt tt.
diff --git a/proofs/compiler/slh_lowering.v b/proofs/compiler/slh_lowering.v
index 6fac13c937..881c695e8e 100644
--- a/proofs/compiler/slh_lowering.v
+++ b/proofs/compiler/slh_lowering.v
@@ -444,6 +444,8 @@ Fixpoint check_i (i : instr) (env : Env.t) : cexec Env.t :=
 
   | Csyscall _ _ _ => ok Env.empty
 
+  | Cassert _ => ok env
+
   | Cif cond c0 c1 =>
       Let _ := chk_mem ii cond in
       Let env0 := check_cmd c0 (Env.update_cond env cond) in
@@ -504,6 +506,9 @@ Fixpoint lower_i (i : instr) : cexec instr :=
     | Csyscall _ _ _ =>
         ok ir
 
+    | Cassert _ =>
+        ok ir
+
     | Cif b c0 c1 =>
       Let c0' := lower_cmd c0 in
       Let c1' := lower_cmd c1 in
diff --git a/proofs/compiler/slh_lowering_proof.v b/proofs/compiler/slh_lowering_proof.v
index ce0750f821..802ca2d2e8 100644
--- a/proofs/compiler/slh_lowering_proof.v
+++ b/proofs/compiler/slh_lowering_proof.v
@@ -1444,6 +1444,7 @@ apply: (cmd_rect (Pr := Pi_r) (Pi := Pi) (Pc := Pc)) c env env' c' => //;
   [ | | |
   | exact: it_lower_opn
   |
+  |
   | exact: lower_it_if
   | exact: lower_it_for
   | exact: lower_it_while
@@ -1466,16 +1467,19 @@ apply: (cmd_rect (Pr := Pi_r) (Pi := Pi) (Pc := Pc)) c env env' c' => //;
     exact: EnvP.le_refl.
 
 (* Syscall *)
-move=> xs o es ii env _ _ _ [<-] [<- <-]; apply (
-  wequiv_syscall_rel_eq_core_R
-    _ _
-    (de := env)
-    (de' := Env.after_assign_vars Env.empty (vrvs xs))
-) => //.
-- by move=> > [-> _].
-- by move=> > [-> _].
-- split=> //. exact: EnvP.le_refl.
-exact: wrequiv_eq.
++ move=> xs o es ii env _ _ _ [<-] [<- <-]; apply (
+    wequiv_syscall_rel_eq_core_R
+      _ _
+      (de := env)
+      (de' := Env.after_assign_vars Env.empty (vrvs xs))
+  ) => //.
+  - by move=> > [-> _].
+  - by move=> > [-> _].
+  - split=> //. exact: EnvP.le_refl.
+  exact: wrequiv_eq.
+
+(* Assert *)
+by move=> > /= [<-] [<- <-]; apply wequiv_assert => //.
 Qed.
 
 Lemma it_lower_call {fn} : wiequiv_f p p' ev ev rpreF fn fn rpostF.
diff --git a/proofs/compiler/stack_alloc.v b/proofs/compiler/stack_alloc.v
index 5f0b32c43a..679afa2737 100644
--- a/proofs/compiler/stack_alloc.v
+++ b/proofs/compiler/stack_alloc.v
@@ -1781,6 +1781,9 @@ Fixpoint alloc_i sao (trmap:table*region_map) (i: instr) : cexec (table * region
     Let: (rmap, c) := alloc_syscall ii rmap rs o es in
     ok (table, rmap, c)
 
+  | Cassert _ =>
+    Error (pp_at_ii ii (stk_ierror_no_var "don't deal with assert"))
+
   | Cif e c1 c2 =>
     Let e := add_iinfo ii (alloc_e rmap e abool) in
     Let: (table1, rmap1, c1) := fmapM (alloc_i sao) (table, rmap) c1 in
diff --git a/proofs/compiler/stack_alloc_proof_2.v b/proofs/compiler/stack_alloc_proof_2.v
index 1da08dee8d..debb699b79 100644
--- a/proofs/compiler/stack_alloc_proof_2.v
+++ b/proofs/compiler/stack_alloc_proof_2.v
@@ -2383,6 +2383,9 @@ Proof.
   by apply wfr_VARS_STATUS_merge.
 Qed.
 
+Local Lemma Wassert a: Pi_r (Cassert a).
+Proof. done. Qed.
+
 Local Lemma Wif e c1 c2: Pc c1 -> Pc c2 -> Pi_r (Cif e c1 c2).
 Proof.
   move=> Hc1 Hc2 table1 rmap1 table2 rmap2 ii c /=.
@@ -2456,7 +2459,7 @@ Lemma alloc_i_invariant table1 rmap1 i table2 rmap2 c2 :
   wf_table_vars table1 rmap1 ->
   wf_table_vars table2 rmap2 /\ Sv.Subset table1.(vars) table2.(vars).
 Proof.
-  exact: (instr_Rect Wmk Wnil Wcons Wasgn Wopn Wsyscall Wif Wfor Wwhile Wcall).
+  exact: (instr_Rect Wmk Wnil Wcons Wasgn Wopn Wsyscall Wassert Wif Wfor Wwhile Wcall).
 Qed.
 
 Lemma alloc_is_invariant table1 rmap1 c1 table2 rmap2 c2 :
@@ -2464,7 +2467,7 @@ Lemma alloc_is_invariant table1 rmap1 c1 table2 rmap2 c2 :
   wf_table_vars table1 rmap1 ->
   wf_table_vars table2 rmap2 /\ Sv.Subset table1.(vars) table2.(vars).
 Proof.
-  exact: (cmd_rect Wmk Wnil Wcons Wasgn Wopn Wsyscall Wif Wfor Wwhile Wcall).
+  exact: (cmd_rect Wmk Wnil Wcons Wasgn Wopn Wsyscall Wassert Wif Wfor Wwhile Wcall).
 Qed.
 
 End SYNTACTIC_INVARIANTS.
diff --git a/proofs/compiler/unrolling.v b/proofs/compiler/unrolling.v
index 6dc4fe5155..be2fa7ea86 100644
--- a/proofs/compiler/unrolling.v
+++ b/proofs/compiler/unrolling.v
@@ -55,6 +55,7 @@ Fixpoint unroll_i (i: instr) : cmd * bool :=
   | Cassgn _ _ _ _
   | Copn _ _ _ _
   | Csyscall _ _ _
+  | Cassert _
   | Ccall _ _ _
     => ([:: i ], false)
   | Cif b c1 c2  =>
diff --git a/proofs/compiler/unrolling_proof.v b/proofs/compiler/unrolling_proof.v
index 9d540c3526..12769f20f9 100644
--- a/proofs/compiler/unrolling_proof.v
+++ b/proofs/compiler/unrolling_proof.v
@@ -252,6 +252,7 @@ Section PROOF.
     + by move=> ????? /=; apply wequiv_assgn_rel_eq with checker_st_eq tt.
     + by move=> ????? /=; apply wequiv_opn_rel_eq with checker_st_eq tt.
     + by move=> ???? /=; apply wequiv_syscall_rel_eq with checker_st_eq tt.
+    + by move=> ?? /=; apply wequiv_assert_rel_eq with checker_st_eq.
     + by move=> > ??? /=; surjpairing; apply wequiv_if_rel_eq with checker_st_eq tt tt tt.
     + move=> i d lo hi c hc ii /=; surjpairing.
       case: is_constP => [{}lo | {}lo]; last by apply wequiv_for_rel_eq with checker_st_eq tt tt.
diff --git a/proofs/compiler/wint_int.v b/proofs/compiler/wint_int.v
index ed002a7757..26ccffcd2e 100644
--- a/proofs/compiler/wint_int.v
+++ b/proofs/compiler/wint_int.v
@@ -324,6 +324,10 @@ Fixpoint wi2i_ir (ir:instr_r) : cexec instr_r :=
     Let xs := mapM2 (E.ierror_s "invalid dest in Csyscall") wi2i_lv xtys xs in
     ok (Csyscall xs o es)
 
+  | Cassert (msg, e) =>
+    Let e := wi2i_e e in
+    ok (Cassert (msg, e))
+
   | Cif b c1 c2 =>
     Let b := wi2i_e b in
     Let c1 := mapM wi2i_i c1 in
diff --git a/proofs/compiler/wint_word.v b/proofs/compiler/wint_word.v
index b209efd9ad..cfa1f919f0 100644
--- a/proofs/compiler/wint_word.v
+++ b/proofs/compiler/wint_word.v
@@ -87,6 +87,9 @@ Fixpoint wi2w_ir (ir:instr_r) : instr_r :=
   | Csyscall xs o es =>
     Csyscall (map wi2w_lv xs) o (map wi2w_e es)
 
+  | Cassert (msg, e) =>
+    Cassert (msg, wi2w_e e)
+
   | Cif b c1 c2 =>
     Cif (wi2w_e b) (map wi2w_i c1) (map wi2w_i c2)
 
diff --git a/proofs/compiler/wint_word_proof.v b/proofs/compiler/wint_word_proof.v
index db6b377f18..546b68d19a 100644
--- a/proofs/compiler/wint_word_proof.v
+++ b/proofs/compiler/wint_word_proof.v
@@ -445,6 +445,7 @@ Proof.
   + by move=> x tg ty e ii; apply wequiv_assgn_rel_uincl with checker_wi2w tt.
   + by move=> xs tg o es ii; apply wequiv_opn_rel_uincl with checker_wi2w tt.
   + by move=> xs o es ii; apply wequiv_syscall_rel_uincl with checker_wi2w tt.
+  + by move=> >; apply wequiv_noassert.
   + by move=> e c1 c2 hc1 hc2 ii; apply wequiv_if_rel_uincl with checker_wi2w tt tt tt.
   + by move=> v dir lo hi c hc ii; apply wequiv_for_rel_uincl with checker_wi2w tt tt.
   + by move=> a c e ii' c' hc hc' ii; apply wequiv_while_rel_uincl with checker_wi2w tt.
diff --git a/proofs/compiler/x86_lowering_proof.v b/proofs/compiler/x86_lowering_proof.v
index 5a1e5ffaf6..0e2a0fde53 100644
--- a/proofs/compiler/x86_lowering_proof.v
+++ b/proofs/compiler/x86_lowering_proof.v
@@ -2058,6 +2058,8 @@ Section PROOF.
       rewrite /disj_fvars  /x86_lowering.disj_fvars vars_I_syscall => /disjoint_union [hdisjx hdisje].
       apply (wequiv_syscall_rel_eq (sip:=sip)) with
          checker_st_eq_ex fvars => //.
+    (* Assert *)
+    + by move=> a ii _; apply wequiv_noassert with (ev1:=ev) (ii:=ii).
     (* If *)
     + move=> e c1 c2 hc1 hc2 ii /disj_fvars_vars_I_Cif [hfve /hc1{}hc1 /hc2{}hc2] /=.
       case heq: lower_condition => [pre e'].
diff --git a/proofs/lang/expr.v b/proofs/lang/expr.v
index 492c6a75d4..fea79a69c9 100644
--- a/proofs/lang/expr.v
+++ b/proofs/lang/expr.v
@@ -381,6 +381,11 @@ Variant align :=
 
 (* -------------------------------------------------------------------- *)
 
+Definition assertion := (assertion_label * pexpr)%type.
+Definition assertions := seq assertion.
+
+(* -------------------------------------------------------------------- *)
+
 Section ASM_OP.
 
 Context `{asmop:asmOp}.
@@ -389,6 +394,7 @@ Inductive instr_r :=
 | Cassgn   : lval -> assgn_tag -> atype -> pexpr -> instr_r
 | Copn     : lvals -> assgn_tag -> sopn -> pexprs -> instr_r
 | Csyscall : lvals -> syscall_t -> pexprs -> instr_r
+| Cassert  : assertion -> instr_r
 | Cif      : pexpr -> seq instr -> seq instr  -> instr_r
 | Cfor     : var_i -> range -> seq instr -> instr_r
 | Cwhile   : align -> seq instr -> pexpr -> instr_info -> seq instr -> instr_r
@@ -411,6 +417,7 @@ Section CMD_RECT.
   Hypothesis Hasgn: forall x tg ty e, Pr (Cassgn x tg ty e).
   Hypothesis Hopn : forall xs t o es, Pr (Copn xs t o es).
   Hypothesis Hsyscall : forall xs o es, Pr (Csyscall xs o es).
+  Hypothesis Hassert : forall a, Pr (Cassert a).
   Hypothesis Hif  : forall e c1 c2, Pc c1 -> Pc c2 -> Pr (Cif e c1 c2).
   Hypothesis Hfor : forall v dir lo hi c, Pc c -> Pr (Cfor v (dir,lo,hi) c).
   Hypothesis Hwhile : forall a c e info c', Pc c -> Pc c' -> Pr (Cwhile a c e info c').
@@ -435,6 +442,7 @@ Section CMD_RECT.
     | Cassgn x tg ty e => Hasgn x tg ty e
     | Copn xs t o es => Hopn xs t o es
     | Csyscall xs o es => Hsyscall xs o es
+    | Cassert a => Hassert a
     | Cif e c1 c2  => @Hif e c1 c2 (cmd_rect_aux instr_Rect c1) (cmd_rect_aux instr_Rect c2)
     | Cfor i (dir,lo,hi) c => @Hfor i dir lo hi c (cmd_rect_aux instr_Rect c)
     | Cwhile a c e info c'   => @Hwhile a c e info c' (cmd_rect_aux instr_Rect c) (cmd_rect_aux instr_Rect c')
@@ -809,6 +817,7 @@ Fixpoint write_i_rec s (i:instr_r) :=
   | Cassgn x _ _ _  => vrv_rec s x
   | Copn xs _ _ _   => vrvs_rec s xs
   | Csyscall xs _ _ => vrvs_rec s xs
+  | Cassert _       => s
   | Cif   _ c1 c2   => foldl write_I_rec (foldl write_I_rec s c2) c1
   | Cfor  x _ c     => foldl write_I_rec (Sv.add x s) c
   | Cwhile _ c _ _ c' => foldl write_I_rec (foldl write_I_rec s c') c
@@ -884,6 +893,7 @@ Fixpoint read_i_rec (s:Sv.t) (i:instr_r) : Sv.t :=
   | Cassgn x _ _ e => read_rv_rec (read_e_rec s e) x
   | Copn xs _ _ es => read_es_rec (read_rvs_rec s xs) es
   | Csyscall xs _ es => read_es_rec (read_rvs_rec s xs) es
+  | Cassert a => read_e_rec s a.2
   | Cif b c1 c2 =>
     let s := foldl read_I_rec s c1 in
     let s := foldl read_I_rec s c2 in
diff --git a/proofs/lang/expr_facts.v b/proofs/lang/expr_facts.v
index 87e5cc7035..108f3323e5 100644
--- a/proofs/lang/expr_facts.v
+++ b/proofs/lang/expr_facts.v
@@ -238,7 +238,7 @@ Let Pc c := forall s, Sv.Equal (foldl write_I_rec s c) (Sv.union s (write_c c)).
 Lemma write_c_recE s c : Sv.Equal (write_c_rec s c) (Sv.union s (write_c c)).
 Proof.
   apply: (cmd_rect (Pr := Pr) (Pi := Pi) (Pc := Pc)) => /= {c s}
-    [ i ii Hi | | i c Hi Hc | x tg ty e | xs t o es | p x e | e c1 c2 Hc1 Hc2
+    [ i ii Hi | | i c Hi Hc | x tg ty e | xs t o es | p x e | a | e c1 c2 Hc1 Hc2
     | v dir lo hi c Hc | a c e ii c' Hc Hc' | ii xs f es ] s;
     rewrite /write_I /write_I_rec /write_i /write_i_rec -/write_i_rec -/write_I_rec /write_c /=
     ?Hc1 ?Hc2 /write_c_rec ?Hc ?Hc' ?Hi -?vrv_recE -?vrvs_recE //;
@@ -270,6 +270,9 @@ Proof. done. Qed.
 Lemma write_i_syscall xs o es : write_i (Csyscall xs o es) = vrvs xs.
 Proof. done. Qed.
 
+Lemma write_i_assert a : write_i (Cassert a) = Sv.empty.
+Proof. done. Qed.
+
 Lemma write_i_if e c1 c2 :
   Sv.Equal (write_i (Cif e c1 c2)) (Sv.union (write_c c1) (write_c c2)).
 Proof.
@@ -383,7 +386,7 @@ Let Pc c := forall s, Sv.Equal (foldl read_I_rec s c) (Sv.union s (read_c c)).
 Lemma read_cE s c : Sv.Equal (read_c_rec s c) (Sv.union s (read_c c)).
 Proof.
   apply (cmd_rect (Pr := Pr) (Pi := Pi) (Pc := Pc)) => /= {c s}
-   [ i ii Hi | | i c Hi Hc | x tg ty e | xs t o es | p x e | e c1 c2 Hc1 Hc2
+   [ i ii Hi | | i c Hi Hc | x tg ty e | xs t o es | p x e | a | e c1 c2 Hc1 Hc2
     | v dir lo hi c Hc | a c e ii c' Hc Hc' | ii xs f es ] s;
     rewrite /read_I /read_I_rec /read_i /read_i_rec -/read_i_rec -/read_I_rec /read_c /=
      ?read_rvE ?read_eE ?read_esE ?read_rvE ?read_rvsE ?Hc2 ?Hc1 /read_c_rec ?Hc' ?Hc ?Hi //;
@@ -414,6 +417,12 @@ Lemma read_i_syscall xs o es:
   Sv.Equal (read_i (Csyscall xs o es)) (Sv.union (read_rvs xs) (read_es es)).
 Proof. rewrite /read_i /write_i /read_i_rec read_esE read_rvsE; clear; SvD.fsetdec. Qed.
 
+Lemma read_i_assert a :
+  Sv.Equal (read_i (Cassert a)) (read_e a.2).
+Proof.
+  rewrite /read_i /read_i_rec read_eE;SvD.fsetdec.
+Qed.
+
 Lemma read_i_if e c1 c2 :
    Sv.Equal (read_i (Cif e c1 c2)) (Sv.union (read_e e) (Sv.union (read_c c1) (read_c c2))).
 Proof.
@@ -448,6 +457,7 @@ Definition read_writeE :=
    read_i_assgn, write_i_assgn,
    read_i_opn, write_i_opn,
    read_i_syscall, write_i_syscall,
+   read_i_assert, write_i_assert,
    read_i_if, write_i_if,
    read_i_for, write_i_for,
    read_i_while, write_i_while,
@@ -482,6 +492,10 @@ Lemma vars_I_syscall ii xs o es:
   Sv.Equal (vars_I (MkI ii (Csyscall xs o es))) (Sv.union (vars_lvals xs) (read_es es)).
 Proof. by rewrite /vars_I read_Ii write_Ii read_i_syscall write_i_syscall /vars_lvals; clear; SvD.fsetdec. Qed.
 
+Lemma vars_I_assert ii a:
+  Sv.Equal (vars_I (MkI ii (Cassert a))) (read_e a.2).
+Proof. rewrite /vars_I read_Ii write_Ii //= !read_writeE; SvD.fsetdec. Qed.
+
 Lemma vars_I_if ii e c1 c2:
   Sv.Equal (vars_I (MkI ii (Cif e c1 c2))) (Sv.union (read_e e) (Sv.union (vars_c c1) (vars_c c2))).
 Proof.
diff --git a/proofs/lang/hoare_logic.v b/proofs/lang/hoare_logic.v
index 05d7b9fcd2..f4ea829d90 100644
--- a/proofs/lang/hoare_logic.v
+++ b/proofs/lang/hoare_logic.v
@@ -93,6 +93,7 @@ Context
   {syscall_state : Type}
   {ep : EstateParams syscall_state}
   {spp : SemPexprParams}
+  {wa: WithAssert}
   {asm_op: Type}
   {sip : SemInstrParams asm_op syscall_state}
   {pT : progT}
@@ -540,9 +541,35 @@ Proof.
   move=> s hP; apply (ho s hP _ ht).
 Qed.
 
+Lemma hoare_assert (P Q : Pred_c) Qerr ii a :
+  (forall s e, P s -> Qerr e -> rInvErr s e) ->
+  rhoare P (fun s => sem_assert (p_globs p) s a) PredT Qerr ->
+  (forall s, P s -> sem_assert (p_globs p) s a = ok tt -> Q s) ->
+  hoare P [:: MkI ii (Cassert a)] Q.
+Proof.
+  move=> herr he ha ; rewrite /hoare /isem_cmd_ /=.
+  apply khoare_bind with Q; last by apply khoare_ret.
+  apply  khoare_ioP.
+  move => s0 hpre.
+  apply khoare_read with (R:= (fun _ => P s0 /\ sem_assert (p_globs p) s0 a = ok tt)).
+  + rewrite /isem_assert.
+    apply khoare_iresult with (Qerr).
+    + move => s e h; subst.
+      exact: (herr _ _ hpre).
+    move => s hpre';subst.
+    have := he s0 hpre.
+    case (sem_assert (p_globs p) s0 a).
+    + by move => [] ?.
+    done.
+    move => _ [] _ has.
+    apply khoare_ret.
+    move => s heq;subst.
+    by apply: ha.
+Qed.
+
 Lemma hoare_if_full P Q Qerr ii e c c' :
   (forall s e, P s -> Qerr e -> rInvErr s e) ->
-  rhoare P (sem_cond (p_globs p) e) (fun _ => True) Qerr ->
+  rhoare P (sem_cond (p_globs p) e) PredT Qerr ->
   (forall b,
      hoare (fun s => P s /\ sem_cond (p_globs p) e s = ok b) (if b then c else c') Q) ->
   hoare P [:: MkI ii (Cif e c c')] Q.
@@ -590,7 +617,7 @@ Qed.
 
 Lemma hoare_for P Pi Qerr ii i d lo hi c :
   (forall s e, P s -> Qerr e -> rInvErr s e) ->
-  rhoare P (sem_bound (p_globs p) lo hi) (fun _ => True) Qerr ->
+  rhoare P (sem_bound (p_globs p) lo hi) PredT Qerr ->
   (forall (j:Z), rhoare P (write_var true i (Vint j)) Pi Qerr) ->
   hoare Pi c P ->
   hoare P [:: MkI ii (Cfor i (d, lo, hi) c)] P.
@@ -602,7 +629,7 @@ Qed.
 Lemma hoare_while_full I I' Qerr ii al e inf c c' :
   (forall s e, I' s -> Qerr e -> rInvErr s e) ->
   hoare I c I' ->
-  rhoare I' (sem_cond (p_globs p) e) (fun _ => True) Qerr  ->
+  rhoare I' (sem_cond (p_globs p) e) PredT Qerr  ->
   hoare (fun s => I' s /\ sem_cond (p_globs p) e s = ok true) c' I ->
   hoare I [:: MkI ii (Cwhile al c e inf c')]
      (fun s => I' s /\ sem_cond (p_globs p) e s = ok false).
@@ -627,7 +654,7 @@ Qed.
 Lemma hoare_while I I' Qerr ii al e inf c c' :
   (forall s e, I' s -> Qerr e -> rInvErr s e) ->
   hoare I c I' ->
-  rhoare I' (sem_cond (p_globs p) e) (fun _ => True) Qerr  ->
+  rhoare I' (sem_cond (p_globs p) e) PredT Qerr  ->
   hoare I' c' I ->
   hoare I [:: MkI ii (Cwhile al c e inf c')] I'.
 Proof.
@@ -790,7 +817,7 @@ End HOARE_FUN.
 
 (* Weak version of hoare logic where the post condition on errors is True *)
 Definition invErrT : InvErr :=
-  {| invErr_ := fun=> True |}.
+  {| invErr_ := PredT |}.
 
 Notation whoare := (hoare (iEr := invErrT)).
 Notation whoare_f := (hoare_f_ii (iEr := invErrT)).
@@ -824,6 +851,12 @@ Lemma whoare_syscall Rv Ro P Q ii xs sc es :
   whoare p ev P [:: MkI ii (Csyscall xs sc es)] Q.
 Proof. by apply hoare_syscall. Qed.
 
+Lemma whoare_assert (P Q : Pred_c) ii a :
+  rhoare P (fun s => sem_assert (p_globs p) s a) PredT PredT ->
+  (forall s, P s -> sem_assert (p_globs p) s a = ok tt -> Q s) ->
+  whoare p ev P [:: MkI ii (Cassert a)] Q.
+Proof. by apply hoare_assert. Qed.
+
 Lemma whoare_if_full P Q ii e c c' :
   rhoare P (sem_cond (p_globs p) e) (fun _ => True) PredT ->
   (forall b,
@@ -937,6 +970,7 @@ Context
   {ep : EstateParams syscall_state}
   {spp : SemPexprParams}
   {asm_op: Type}
+  {wa: WithAssert}
   {sip : SemInstrParams asm_op syscall_state}
   {pT : progT}
   {wsw : WithSubWord}
@@ -988,6 +1022,9 @@ Proof.
     apply whoare_syscall with PredT PredT; try auto using rhoare_true.
     move=> v _; apply wrhoareP => s s' <-.
     by rewrite write_Ii write_i_syscall => /vrvsP /=.
+  + move => a ii s0.
+    apply whoare_assert; try auto using rhoare_true.
+    move=> ? -> ? //=.
   + move=> e c1 c2 hc1 hc2 ii s0.
     apply whoare_if; first by auto using rhoare_true.
     move=> b; rewrite write_Ii.
diff --git a/proofs/lang/it_sems_core.v b/proofs/lang/it_sems_core.v
index 965e85ccbc..ed4dc95e7d 100644
--- a/proofs/lang/it_sems_core.v
+++ b/proofs/lang/it_sems_core.v
@@ -135,6 +135,7 @@ Context
   {syscall_state : Type}
   {ep : EstateParams syscall_state}
   {spp : SemPexprParams}
+  {wa: WithAssert}
   {sip : SemInstrParams asm_op syscall_state}
   {pT : progT}
   {scP : semCallParams}.
@@ -203,6 +204,12 @@ Definition sem_syscall (xs : lvals) (o : syscall_t) (es : pexprs)
 Definition sem_cond (gd : glob_decls) (e : pexpr) (s : estate) : exec bool :=
   (sem_pexpr true gd s e >>= to_bool)%result.
 
+Definition sem_assert (gd : glob_decls) (s : estate) (e : assertion) : exec unit :=
+  Let _ := assert (assert_allowed) ErrType in
+  Let b := sem_cond gd e.2 s in
+  Let _ := assert b (ErrAssert e.1) in
+  ok tt.
+
 Lemma sem_cond_sem_pexpr gd e s b :
   sem_cond gd e s = ok b -> sem_pexpr true gd s e = ok (Vbool b).
 Proof. rewrite /sem_cond /=; by t_xrbindP=> _ -> /to_boolI ->. Qed.
@@ -219,6 +226,9 @@ Definition sem_bound (gd : glob_decls) (lo hi : pexpr) (s : estate) :
 Definition isem_bound (lo hi : pexpr) (s : estate) : itree E (Z * Z) :=
   iresult s (sem_bound (p_globs p) lo hi s).
 
+Definition isem_assert (a: assertion) (s: estate) : itree E unit :=
+  iresult s (sem_assert (p_globs p) s a).
+
 (* recCall trigger *)
 Definition rec_call (ii:instr_info) (f : funname) (fs : fstate) :
    itree (recCall +' E) fstate :=
@@ -288,6 +298,8 @@ Fixpoint isem_i_body (p : prog) (ev : extra_val_t) (i : instr) (s : estate) :
 
   | Csyscall xs o es => iresult s (sem_syscall p xs o es s)
 
+  | Cassert a => isem_assert p a s;; Ret s
+
   | Cif e c1 c2 =>
     b <- isem_cond p e s;;
     isem_foldr isem_i_body p ev (if b then c1 else c2) s
@@ -368,6 +380,8 @@ Fixpoint esem_i (p : prog) (ev : extra_val_t) (i : instr) (s : estate) :
 
   | Csyscall xs o es => sem_syscall p xs o es s
 
+  | Cassert a => Let _ := sem_assert (p_globs p) s a in ok s
+
   | Cif e c1 c2 =>
     Let b := sem_cond (p_globs p) e s in
     foldM (esem_i p ev) s (if b then c1 else c2)
@@ -402,6 +416,7 @@ Proof.
   + move=> > /= [<-]; reflexivity.
   + by move=> i c hi hc s s' /=; t_xrbindP => s1 /hi ->; rewrite bind_ret_l; apply hc.
   1-3: move=> > /= -> /=; reflexivity.
+  + move => a ii s s' /=; t_xrbindP; rewrite /isem_assert => -> <-; rewrite bind_ret_l; reflexivity.
   + move=> > hc1 hc2 ii s s' /=.
     rewrite /isem_cond; t_xrbindP => b -> /=.
     by rewrite bind_ret_l; case: b; [apply hc1 | apply hc2].
@@ -605,6 +620,10 @@ Proof.
   + move=> i c hi hc s; rewrite interp_bind;apply eqit_bind; first by apply hi.
     by move=> s'; apply hc.
   1-3: by move=> >; apply interp_iresult.
+  + move => a ii s /=.
+    rewrite interp_bind; apply eqit_bind.
+    + by apply interp_iresult.
+    move => ?; rewrite interp_ret; reflexivity.
   + move=> e c1 c2 hc1 hc2 ii s; rewrite /isem_i /isem_i_rec /=.
     rewrite interp_bind; apply eqit_bind.
     + by apply interp_iresult.
@@ -714,6 +733,9 @@ Proof.
     + by move=> > ? >; apply interp_cond_iresult.
     + by move=> > ? > ? > ; apply interp_cond_iresult.
     + by move=> > ? >; apply interp_cond_iresult.
+    + move=> a ii s; rewrite interp_bind; apply eutt_eq_bind'.
+      + by apply interp_cond_iresult.
+      by move=> ?; rewrite interp_ret; reflexivity.
     + move=> e c1 c2 hc1 hc2 ii s; rewrite interp_bind.
       rewrite /isem_cond interp_cond_iresult.
       by apply/eutt_eq_bind; case; [apply hc1 | apply hc2].
diff --git a/proofs/lang/psem.v b/proofs/lang/psem.v
index 7f4d99ac76..8c2d75e85d 100644
--- a/proofs/lang/psem.v
+++ b/proofs/lang/psem.v
@@ -370,6 +370,7 @@ Lemma sem_iE s i s' :
     [/\ sem_pexprs true gd s es = ok ves,
         exec_syscall s.(escs) s.(emem) o ves = ok (scs, m, vs) &
         write_lvals true gd (with_scs (with_mem s m) scs) xs vs = ok s']
+  | Cassert _ => False
   | Cif e th el =>
     ∃ b, sem_pexpr true gd s e = ok (Vbool b) ∧ sem s (if b then th else el) s'
   | Cfor i (d, lo, hi) c =>
@@ -647,6 +648,7 @@ Proof.
   + by move=> >;apply wequiv_assgn_rel_eq with checker_st_eq tt.
   + by move=> >; apply wequiv_opn_rel_eq with checker_st_eq tt.
   + by move=> >; apply wequiv_syscall_rel_eq with checker_st_eq tt.
+  + by move=> a ii; apply wequiv_assert_rel_eq with checker_st_eq.
   + by move=> > hc1 hc2 ii; apply wequiv_if_rel_eq with checker_st_eq tt tt tt.
   + by move=> > hc ii; apply wequiv_for_rel_eq with checker_st_eq tt tt.
   + by move=> > hc hc' ii; apply wequiv_while_rel_eq with checker_st_eq tt.
@@ -1061,6 +1063,8 @@ Proof.
     by apply wequiv_opn_rel_eq with checker_st_eq_on X => //=; split=> //; SvD.fsetdec.
   + move=> xs sc es ii X. rewrite read_i_syscall => hsub.
     by apply wequiv_syscall_rel_eq with checker_st_eq_on X => //=; split=> //; SvD.fsetdec.
+  + move=> a ii X; rewrite read_i_assert => hsub.
+    by apply wequiv_assert_rel_eq with checker_st_eq_on => //; split.
   + move=> e c1 c2 hc1 hc2 ii X. rewrite read_i_if => hsub.
     apply wequiv_if_rel_eq with checker_st_eq_on X X X => //.
     + by split => //; rewrite /read_es /= read_eE; SvD.fsetdec.
@@ -1506,6 +1510,7 @@ Proof.
   + by move=> x tg ty e ii; apply wequiv_assgn_rel_uincl with checker_st_uincl tt.
   + by move=> xs tg o es ii; apply wequiv_opn_rel_uincl with checker_st_uincl tt.
   + by move=> xs sc es ii; apply wequiv_syscall_rel_uincl with checker_st_uincl tt.
+  + by move=> a ii; apply wequiv_assert_rel_uincl with checker_st_uincl.
   + by move=> e c1 c2 hc1 hc2 ii; apply wequiv_if_rel_uincl with checker_st_uincl tt tt tt.
   + by move=> > hc ii; apply wequiv_for_rel_uincl with checker_st_uincl tt tt.
   + by move=> > ?? ii; apply wequiv_while_rel_uincl with checker_st_uincl tt.
@@ -1765,6 +1770,7 @@ Context
   {E E0 : Type -> Type}
   {wE : with_Error E E0}
   {wsw1 wsw2 wsw3 : WithSubWord}
+  {wa1 wa2 wa3 : WithAssert}
   {scP1 : semCallParams (wsw := wsw1) (pT := pT1)}
   {scP2 : semCallParams (wsw := wsw2) (pT := pT2)}
   {scP3 : semCallParams (wsw := wsw3) (pT := pT3)}
@@ -1791,6 +1797,7 @@ Context
 Let wiequiv_f_trans' :=
   wiequiv_f_trans
     (wsw1 := wsw1) (wsw2 := wsw2) (wsw3 := wsw3)
+    (wa1 := wa1) (wa2 := wa2) (wa3 := wa3)
     (scP1 := scP1) (scP2 := scP2) (scP3 := scP3)
     (dc1 := dc1) (dc2 := dc2) (dc3 := dc3)
     (p1 := p1) (p2 := p2) (p3 := p3)
diff --git a/proofs/lang/psem_of_sem_proof.v b/proofs/lang/psem_of_sem_proof.v
index 01411ea4e6..f61f74bcc4 100644
--- a/proofs/lang/psem_of_sem_proof.v
+++ b/proofs/lang/psem_of_sem_proof.v
@@ -364,6 +364,7 @@ Proof.
   + move=> ????; apply wequiv_syscall_rel_eq_core with checker_st_eq tt => //.
     move=> [???] [???] ? [<- <- <-]; rewrite /fexec_syscall /=.
     by t_xrbindP => -[[??]?] /= /hsyscall -> [<-] /=; eauto.
+  + by move=> a ii; apply wequiv_assert_rel_eq with checker_st_eq.
   + by move=> > hc1 hc2 ii; apply wequiv_if_rel_eq with checker_st_eq tt tt tt.
   + by move=> > hc ii; apply wequiv_for_rel_eq with checker_st_eq tt tt.
   + by move=> > hc hc' ii; apply wequiv_while_rel_eq with checker_st_eq tt.
diff --git a/proofs/lang/relational_logic.v b/proofs/lang/relational_logic.v
index 4e8223b4bc..fce7af338a 100644
--- a/proofs/lang/relational_logic.v
+++ b/proofs/lang/relational_logic.v
@@ -505,6 +505,12 @@ Qed.
 
 End IRESULT.
 
+Section WITHASSERT.
+
+Context {wa1 wa2 : WithAssert}.
+Notation isem_fun1 := (isem_fun (wsw:=wsw1) (dc:=dc1) (ep:=ep) (spp:=spp) (wa:=wa1) (sip:=sip) (pT:=pT1) (scP:= scP1)).
+Notation isem_fun2 := (isem_fun (wsw:=wsw2) (dc:=dc2) (ep:=ep) (spp:=spp) (wa:=wa2) (sip:=sip) (pT:=pT2) (scP:= scP2)).
+
 Section WEQUIV_CORE.
 
 Context {E E0 : Type -> Type} {sem_F1 : sem_Fun1 E} {sem_F2 : sem_Fun2 E}
@@ -528,15 +534,15 @@ Definition wequiv_f_ii (P : relPreF) ii1 ii2 (fn1 fn2 : funname) (Q:relPostF) :=
 Definition wequiv_f_body (P : relPreF) (fn1 fn2 : funname) (Q:relPostF) :=
   wkequiv_io
     (P fn1 fn2)
-      (isem_fun_body (dc:=dc1) (sem_F:=sem_F1) p1 ev1 fn1)
-      (isem_fun_body (dc:=dc2) (sem_F:=sem_F2) p2 ev2 fn2)
+      (isem_fun_body (wa:=wa1) (dc:=dc1) (sem_F:=sem_F1) p1 ev1 fn1)
+      (isem_fun_body (wa:=wa2) (dc:=dc2) (sem_F:=sem_F2) p2 ev2 fn2)
     (Q fn1 fn2).
 
 Definition wequiv (pre:rel_c) (c1 c2 : cmd) (post : rel_c) :=
   wkequiv
     pre
-     (isem_cmd_ (dc:=dc1) (sem_F:=sem_F1) p1 ev1 c1)
-     (isem_cmd_ (dc:=dc2) (sem_F:=sem_F2) p2 ev2 c2)
+     (isem_cmd_ (wa:=wa1) (dc:=dc1) (sem_F:=sem_F1) p1 ev1 c1)
+     (isem_cmd_ (wa:=wa2) (dc:=dc2) (sem_F:=sem_F2) p2 ev2 c2)
     post.
 
 Lemma wequiv_weaken P1 P2 Q1 Q2 c1 c2 :
@@ -731,6 +737,83 @@ Proof.
   by rewrite /errcutoff /is_error /subevent /resum /fromErr mid12.
 Qed.
 
+Lemma wequiv_assert_esem (P Q : rel_c) ii1 a1 c2 :
+  wrequiv P (fun (s:estate1) => Let _ := sem_assert (wsw:=wsw1) (wa:=wa1) (p_globs p1) s a1 in ok s)
+            (esem (wa:=wa2) p2 ev2 c2) Q ->
+  wequiv P [:: MkI ii1 (Cassert a1)] c2 Q.
+Proof.
+  move=> h s t hP /=; rewrite /isem_assert.
+  case heq: sem_assert => [s' | e] /=.
+  + rewrite bind_ret_r.
+    have [|t' /esem_i_bodyP -> hQ /=] := h s t s hP.
+    + by rewrite heq.
+    by rewrite bind_ret_l; apply xrutt.xrutt_Ret.
+  rewrite bind_ret_r bind_vis; apply xrutt_CutL => //.
+  by rewrite /errcutoff /is_error /subevent /resum /fromErr mid12.
+Qed.
+
+Lemma wequiv_assert (P Q : rel_c) ii1 a1 ii2 a2 :
+  (assert_allowed (WithAssert:=wa1) ->
+   assert_allowed (WithAssert:=wa2) /\
+   forall s1 s2,
+     P s1 s2 ->
+     sem_cond (p_globs p1) a1.2 s1 = ok true ->
+     sem_cond (p_globs p2) a2.2 s2 = ok true /\ Q s1 s2) ->
+  wequiv P [:: MkI ii1 (Cassert a1)] [:: MkI ii2 (Cassert a2)] Q.
+Proof.
+  move=> hcond; apply wequiv_assert_esem => s t s' hP /=.
+  rewrite /sem_assert; t_xrbindP.
+  move=> /hcond [-> {}hcond] b1 hsem1 hb1 _ <-; rewrite hb1 in hsem1 => {hb1 b1}.
+  by have [-> hQ /=] := hcond _ _ hP hsem1; exists t.
+Qed.
+
+Lemma sem_cond_uincl P e1 e2 :
+  wrequiv P (fun (s:estate1) => sem_pexpr true (p_globs p1) s e1)
+            (fun (s:estate2) => sem_pexpr true (p_globs p2) s e2) value_uincl ->
+  wrequiv P (sem_cond (p_globs p1) e1) (sem_cond (p_globs p2) e2) eq.
+Proof.
+  move=> he; apply: wrequiv_bind wrequiv_to_bool; apply he.
+Qed.
+
+Lemma wequiv_assert_uincl (P Q : rel_c) ii1 a1 ii2 a2 :
+  (assert_allowed (WithAssert:=wa1) ->
+     assert_allowed (WithAssert:=wa2) /\
+     wrequiv P (fun s => sem_pexpr true (p_globs p1) s a1.2)
+               (fun s => sem_pexpr true (p_globs p2) s a2.2) value_uincl) ->
+  (assert_allowed (WithAssert:=wa1) ->
+   assert_allowed (WithAssert:=wa2) ->
+   forall s1 s2,
+     P s1 s2 ->
+     sem_pexpr true (p_globs p1) s1 a1.2 = ok (Vbool true) ->
+     sem_pexpr true (p_globs p2) s2 a2.2 = ok (Vbool true) ->
+     Q s1 s2) ->
+  wequiv P [:: MkI ii1 (Cassert a1)] [:: MkI ii2 (Cassert a2)] Q.
+Proof.
+  move=> hcond hweak; apply wequiv_assert => haa1.
+  have [haa2 h] := hcond haa1; split => //.
+  move=> s1 s2 hP hsem1.
+  have [o2 hsem2 ?]:= sem_cond_uincl h hP hsem1; subst o2; split => //.
+  by apply hweak => //;[ move: hsem1 | move: hsem2]; rewrite /sem_cond; t_xrbindP => ? -> /to_boolI ->.
+Qed.
+
+Lemma wequiv_assert_eq (P Q : rel_c) ii1 a1 ii2 a2 :
+  (assert_allowed (WithAssert:=wa1) ->
+     assert_allowed (WithAssert:=wa2) /\
+     wrequiv P (fun s => sem_pexpr true (p_globs p1) s a1.2)
+               (fun s => sem_pexpr true (p_globs p2) s a2.2) eq) ->
+  (assert_allowed (WithAssert:=wa1) ->
+   assert_allowed (WithAssert:=wa2) ->
+   forall s1 s2,
+     P s1 s2 ->
+     sem_pexpr true (p_globs p1) s1 a1.2 = ok (Vbool true) ->
+     sem_pexpr true (p_globs p2) s2 a2.2 = ok (Vbool true) ->
+     Q s1 s2) ->
+  wequiv P [:: MkI ii1 (Cassert a1)] [:: MkI ii2 (Cassert a2)] Q.
+Proof.
+  move=> hcond; apply wequiv_assert_uincl => /hcond [? he]; split => //.
+  by apply: wrequiv_weaken he => // > ->.
+Qed.
+
 Section ST_REL.
 
 Context (D:Type).
@@ -846,15 +929,6 @@ Proof.
   by case: (b) (hc b _ _ hP').
 Qed.
 
-Lemma sem_cond_uincl P e1 e2 :
-  wrequiv P (fun (s:estate1) => sem_pexpr true (p_globs p1) s e1)
-            (fun (s:estate2) => sem_pexpr true (p_globs p2) s e2) value_uincl ->
-  wrequiv P (sem_cond (p_globs p1) e1) (sem_cond (p_globs p2) e2) eq.
-Proof.
-  move=> he; rewrite /sem_cond.
-  apply: wrequiv_bind wrequiv_to_bool; apply he.
-Qed.
-
 Lemma wequiv_if_uincl P Q ii1 e1 c1 c1' ii2 e2 c2 c2' :
   wrequiv P (fun (s:estate1) => sem_pexpr true (p_globs p1) s e1)
             (fun (s:estate2) => sem_pexpr true (p_globs p2) s e2) value_uincl ->
@@ -1219,6 +1293,23 @@ Proof.
   by apply/wkequiv_bind_ret_left/wkequiv_iresult_left.
 Qed.
 
+Lemma wequiv_assert_left P Q ii a :
+  (assert_allowed (WithAssert:=wa1) ->
+   forall s t, P s t -> sem_pexpr true (p_globs p1) s a.2 = ok (Vbool true) -> Q s t) ->
+  wequiv P [::MkI ii (Cassert a)] [::] Q.
+Proof.
+  move=> h; rewrite /wequiv /=.
+  apply/wkequiv_bind_ret_left.
+  move=> s1 s2 hP; rewrite /isem_assert.
+  case heq: sem_assert => [ []| e] /=.
+  + rewrite bind_ret_l.
+    move: heq; rewrite /sem_assert /sem_cond; t_xrbindP => hwa [] // v he /to_boolI ? _ _; subst v.
+    by apply/xrutt_Ret/h.
+  rewrite /Exception.throw bind_vis.
+  apply xrutt_CutL => //.
+  by rewrite /errcutoff /is_error /subevent /resum /fromErr mid12.
+Qed.
+
 Section REL.
 
 Context {D:Type}.
@@ -1327,6 +1418,16 @@ Proof.
   by apply: ucheck_lvalsP hxs v1 v2 hu.
 Qed.
 
+Lemma wequiv_assert_rel_uincl d de ii1 a1 ii2 a2 :
+  (assert_allowed (WithAssert:=wa1) → assert_allowed (WithAssert:=wa2)) ->
+  check_es d [::a1.2] [::a2.2] de ->
+  wequiv (R d) [:: MkI ii1 (Cassert a1)] [:: MkI ii2 (Cassert a2)] (R de).
+Proof.
+  move=> hassert hes; apply wequiv_assert_uincl.
+  + move=> /hassert ?; split => //; apply: ucheck_eP hes.
+  by move=> _ _ + + + _ _; apply: check_esP_rel hes.
+Qed.
+
 Lemma wequiv_if_rel_uincl_R d de d1 d2 d' ii e c1 c2 ii' e' c1' c2' :
   check_es d [::e] [::e'] de ->
   (forall s1 s2, R d1 s1 s2 -> R d' s1 s2) ->
@@ -1468,6 +1569,17 @@ Proof.
   by apply: echeck_lvalsP hxs v.
 Qed.
 
+Lemma wequiv_assert_rel_eq d de ii1 a1 ii2 a2 :
+  (assert_allowed (WithAssert:=wa1) → assert_allowed (WithAssert:=wa2)) ->
+  check_es d [::a1.2] [::a2.2] de ->
+  wequiv (R d) [:: MkI ii1 (Cassert a1)] [:: MkI ii2 (Cassert a2)] (R de).
+Proof.
+  move=> hassert hes.
+  apply wequiv_assert_eq.
+  + by move=> /hassert ?; split => //; apply: echeck_eP hes.
+  by move=> _ _ + + + _ _; apply: check_esP_rel hes.
+Qed.
+
 Lemma wequiv_if_rel_eq_R d de d1 d2 d' ii e c1 c2 ii' e' c1' c2' :
   check_es d [::e] [::e'] de ->
   (forall s1 s2, R d1 s1 s2 -> R d' s1 s2) ->
@@ -1718,7 +1830,7 @@ Definition EventRels_and2 : EventRels E0 :=
 
 Lemma whoare_wequiv1 (P Q : rel_c) (P1 Q1 : Pred_c (wsw:=wsw1)) c1 c2:
   (forall s1 s2, P s1 s2 -> P1 s1) ->
-  hoare (wsw:=wsw1) (dc:=dc1) (iEr := invErrT) p1 ev1 P1 c1 Q1 ->
+  hoare (wsw:=wsw1) (wa:=wa1) (dc:=dc1) (iEr := invErrT) p1 ev1 P1 c1 Q1 ->
   wequiv p1 p2 ev1 ev2 P c1 c2 Q ->
   wequiv (rE0 := EventRels_and1) p1 p2 ev1 ev2 P c1 c2 (fun s1 s2 => Q1 s1 /\ Q s1 s2).
 Proof.
@@ -1769,7 +1881,7 @@ Lemma wequiv_write1 (P Q : rel_c) c1 c2:
      (fun s1 s2 => s1_.(evm) =[\ write_c c1] s1.(evm) /\ Q s1 s2)).
 Proof.
   move=> /wkequivP' h s1_; apply/wkequivP' => s1__ s2_.
-  have /(_ s1_) hw := [elaborate it_writeP (dc:=dc1) p1 ev1 c1 ].
+  have /(_ s1_) hw := [elaborate it_writeP (wa:=wa1) (dc:=dc1) p1 ev1 c1 ].
   have h_ : forall s1 s2, (s1 = s1_ /\ s2 = s2_) /\ P s1 s2 -> s1 = s1_.
   + by move=> ?? [] [].
   have {h_ h}:= whoare_wequiv1 h_ hw (h s1_ s2_).
@@ -1787,7 +1899,7 @@ Lemma wequiv_write2 (P Q : rel_c) c1 c2:
      (fun s1 s2 => s2_.(evm) =[\ write_c c2] s2.(evm) /\ Q s1 s2)).
 Proof.
   move=> /wkequivP' h s2_; apply/wkequivP' => s1_ s2__.
-  have /(_ s2_) hw := [elaborate it_writeP (dc:=dc2) p2 ev2 c2 ].
+  have /(_ s2_) hw := [elaborate it_writeP (wa:=wa2) (dc:=dc2) p2 ev2 c2 ].
   have h_ : forall s1 s2, (s1 = s1_ /\ s2 = s2_) /\ P s1 s2 -> s2 = s2_.
   + by move=> ?? [] [].
   have {h_ h}:= whoare_wequiv2 h_ hw (h s1_ s2_).
@@ -1851,9 +1963,9 @@ Proof.
   by case: mfun1 => // ?; case: mfun1.
 Qed.
 
-Notation isem_fun_def1 := (isem_fun_def (wsw:=wsw1) (dc:=dc1) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT1) (scP:= scP1) (sem_F:=sem_F1)).
+Notation isem_fun_def1 := (isem_fun_def (wsw:=wsw1) (wa:=wa1) (dc:=dc1) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT1) (scP:= scP1) (sem_F:=sem_F1)).
 
-Notation isem_fun_def2 := (isem_fun_def (wsw:=wsw2) (dc:=dc2) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT2) (scP:= scP2) (sem_F:=sem_F2)).
+Notation isem_fun_def2 := (isem_fun_def (wsw:=wsw2) (wa:=wa2) (dc:=dc2) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT2) (scP:= scP2) (sem_F:=sem_F2)).
 
 Notation wiequiv_f rpreF fn1 fn2 rpostF :=
    (wkequiv_io (rpreF fn1 fn2) (isem_fun_def1 p1 ev1 fn1) (isem_fun_def2 p2 ev2 fn2) (rpostF fn1 fn2)).
@@ -1898,9 +2010,9 @@ Definition wequiv_fun_body_hyp_rec (RPreF:relPreF) fn1 fn2 (RPostF:relPostF) :=
           , wequiv (sem_F1 := sem_F1 fn1) (sem_F2 := sem_F2 fn2) (rE0:=relEvent_recCall spec) p1 p2 ev1 ev2 P fd1.(f_body) fd2.(f_body) Q
           & wrequiv Q (finalize_funcall (dc:=dc1) fd1) (finalize_funcall (dc:=dc2) fd2) (RPostF fn1 fn2 fs1 fs2)].
 
-Notation isem_fun_def1 := (isem_fun_def (wsw:=wsw1) (dc:=dc1) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT1) (scP:= scP1) (sem_F:=sem_F1)).
+Notation isem_fun_def1 := (isem_fun_def (wsw:=wsw1) (wa:=wa1) (dc:=dc1) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT1) (scP:= scP1) (sem_F:=sem_F1)).
 
-Notation isem_fun_def2 := (isem_fun_def (wsw:=wsw2) (dc:=dc2) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT2) (scP:= scP2) (sem_F:=sem_F2)).
+Notation isem_fun_def2 := (isem_fun_def (wsw:=wsw2) (wa:=wa2) (dc:=dc2) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT2) (scP:= scP2) (sem_F:=sem_F2)).
 
 Notation wiequiv_f rpreF fn1 fn2 rpostF :=
    (wkequiv_io (rpreF fn1 fn2) (isem_fun_def1 p1 ev1 fn1) (isem_fun_def2 p2 ev2 fn2) (rpostF fn1 fn2)).
@@ -1933,8 +2045,8 @@ Definition wequiv_rec_ir P i1 ii1 i2 ii2 Q :=
 
 Definition wiequiv_f rpreF fn1 fn2 rpostF :=
    (wkequiv_io (rpreF fn1 fn2)
-      (isem_fun (wsw:=wsw1) (dc:=dc1) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT1) (scP:= scP1) p1 ev1 fn1)
-      (isem_fun (wsw:=wsw2) (dc:=dc2) (ep:=ep) (spp:=spp) (sip:=sip) (pT:=pT2) (scP:= scP2) p2 ev2 fn2)
+      (isem_fun1 p1 ev1 fn1)
+      (isem_fun2 p2 ev2 fn2)
      (rpostF fn1 fn2)).
 
 Lemma wequiv_fun_get fn1 fn2 Pf Qf :
@@ -1962,6 +2074,25 @@ Qed.
 
 End WEQUIV_FUN.
 
+End WITHASSERT.
+
+Section NOASSERT.
+
+Context {E E0 : Type -> Type} {sem_F1 : sem_Fun1 E} {sem_F2 : sem_Fun2 E}
+    {wE: with_Error E E0} {rE0 : EventRels E0}.
+
+Context (p1 : prog1) (p2 : prog2) (ev1: extra_val_t1) (ev2 : extra_val_t2).
+
+Lemma wequiv_noassert ii a c P Q :
+  wequiv p1 p2 ev1 ev2 P [:: MkI ii (Cassert a)] c Q.
+Proof.
+  move=> s1 s2 _ /=.
+  rewrite bind_ret_r /isem_assert /= /Exception.throw bind_vis; apply xrutt_CutL => //.
+  by rewrite /errcutoff /is_error /subevent /resum /fromErr mid12.
+Qed.
+
+End NOASSERT.
+
 End RELATIONAL.
 
 Arguments wequiv_fun_rec {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.
@@ -2056,6 +2187,7 @@ Context
   {E E0 : Type -> Type}
   {wE : with_Error E E0}
   {wsw1 wsw2 wsw3 : WithSubWord}
+  {wa1 wa2 wa3 : WithAssert}
   {scP1 : semCallParams (wsw := wsw1) (pT := pT1)}
   {scP2 : semCallParams (wsw := wsw2) (pT := pT2)}
   {scP3 : semCallParams (wsw := wsw3) (pT := pT3)}
@@ -2081,16 +2213,19 @@ Notation EPost13 := (EPostRel (rE0 := rE13)).
 Notation wiequiv_f12 :=
   (wiequiv_f
      (scP1 := scP1) (scP2 := scP2)
+     (wa1 := wa1) (wa2 := wa2)
      (dc1 := dc1) (dc2 := dc2)
      (rE0 := rE12)).
 Notation wiequiv_f23 :=
   (wiequiv_f
      (scP1 := scP2) (scP2 := scP3)
+     (wa1 := wa2) (wa2 := wa3)
      (dc1 := dc2) (dc2 := dc3)
      (rE0 := rE23)).
 Notation wiequiv_f13 :=
   (wiequiv_f
      (scP1 := scP1) (scP2 := scP3)
+     (wa1 := wa1) (wa2 := wa3)
      (dc1 := dc1) (dc2 := dc3)
      (rE0 := rE13)).
 
diff --git a/proofs/lang/sem_one_varmap.v b/proofs/lang/sem_one_varmap.v
index f0700bf4af..8b34181605 100644
--- a/proofs/lang/sem_one_varmap.v
+++ b/proofs/lang/sem_one_varmap.v
@@ -267,6 +267,7 @@ Lemma sem_iE ii k s i s' :
          exec_syscall (semCallParams:= sCP_stack) s.(escs) s.(emem) o ves = ok (scs, m, vs) &
          write_lvals true gd {| escs := scs; emem := m; evm := vm_after_syscall s.(evm) |}
            (to_lvals (syscall_sig o).(scs_vout)) vs = ok s']
+  | Cassert _ => False
   | Cif e c1 c2 =>
     exists2 b, sem_pexpr true gd s e = ok (Vbool b) & sem k s (if b then c1 else c2) s'
   | Cwhile a c e ei c' =>
diff --git a/proofs/lang/sem_params.v b/proofs/lang/sem_params.v
index df5a7e5df8..b715c05a24 100644
--- a/proofs/lang/sem_params.v
+++ b/proofs/lang/sem_params.v
@@ -56,3 +56,9 @@ Class SemInstrParams (asm_op syscall_state : Type) := mk_sip
 Existing Instances _asmop _sc_sem | 1000.
 
 Arguments mk_sip {_ _ _ _}.
+
+Class WithAssert := { assert_allowed : bool }.
+Definition noassert : WithAssert := {| assert_allowed := false |}.
+Definition withassert : WithAssert := {| assert_allowed := true |}.
+
+#[global] Existing Instances noassert | 1000.
diff --git a/proofs/lang/utils.v b/proofs/lang/utils.v
index da89ba8b9e..2820e45a8e 100644
--- a/proofs/lang/utils.v
+++ b/proofs/lang/utils.v
@@ -4,7 +4,7 @@ From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
 From mathcomp Require Import fintype finfun.
 From Coq.Unicode Require Import Utf8.
-From Coq Require Import ZArith Zwf Setoid Morphisms CMorphisms CRelationClasses.
+From Coq Require Import ZArith Zwf Setoid Morphisms CMorphisms CRelationClasses String.
 Require Import xseq oseq.
 From mathcomp Require Import word_ssrZ.
 
@@ -214,8 +214,11 @@ Lemma map_errP eT1 eT2 aT (f : eT1 -> eT2) (r : result eT1 aT) x :
 Proof. by case: r => //= ? [->]. Qed.
 Arguments map_errP {_ _ _ _ _ _}.
 
+Definition assertion_label := string.
+
 Variant error :=
- | ErrOob | ErrAddrUndef | ErrAddrInvalid | ErrStack | ErrType | ErrArith | ErrSemUndef.
+ | ErrOob | ErrAddrUndef | ErrAddrInvalid | ErrStack | ErrType | ErrArith | ErrSemUndef
+ | ErrAssert of assertion_label.
 
 Definition exec t := result error t.
 
@@ -500,6 +503,9 @@ Lemma mapM_ok {eT} {A B:Type} (f: A -> B) (l:list A) :
   mapM (eT:=eT) (fun x => ok (f x)) l = ok (map f l).
 Proof. by elim l => //= ?? ->. Qed.
 
+Definition sndM eT aT bT cT (f : bT -> result eT cT) (ab : aT * bT) : result eT (aT * cT) :=
+  Let c := f ab.2 in ok (ab.1, c).
+
 Section FOLDM.
 
   Context (eT aT bT:Type) (f:aT -> bT -> result eT bT).