diff --git a/src/mo_def/arrange.ml b/src/mo_def/arrange.ml
index 22da9f70a56..bd59ab545a0 100644
--- a/src/mo_def/arrange.ml
+++ b/src/mo_def/arrange.ml
@@ -116,6 +116,7 @@ module Make (Cfg : Config) = struct
     | AssertE (Loop_entry, e)    -> "Loop_entry" $$ [exp e]
     | AssertE (Loop_continue, e) -> "Loop_continue" $$ [exp e]
     | AssertE (Loop_exit, e)     -> "Loop_exit" $$ [exp e]
+    | AssertE (Loop_invariant, e)-> "Loop_invariant" $$ [exp e]
     | AssertE (Concurrency s, e) -> "Concurrency"^s $$ [exp e]
     | AnnotE (e, t)       -> "AnnotE"  $$ [exp e; typ t]
     | OptE e              -> "OptE"    $$ [exp e]
diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml
index a23421ea6ed..ab86ff75226 100644
--- a/src/mo_def/syntax.ml
+++ b/src/mo_def/syntax.ml
@@ -201,7 +201,7 @@ and exp' =
 *)
 
 and assert_kind =
-  | Runtime | Static | Invariant | Precondition | Postcondition | Concurrency of string | Loop_entry | Loop_continue | Loop_exit
+  | Runtime | Static | Invariant | Precondition | Postcondition | Concurrency of string | Loop_entry | Loop_continue | Loop_exit | Loop_invariant
 
 and dec_field = dec_field' Source.phrase
 and dec_field' = {dec : dec; vis : vis; stab: stab option}
diff --git a/src/mo_frontend/assertions.mly b/src/mo_frontend/assertions.mly
index ca7d40ca5e4..f1e937d47bc 100644
--- a/src/mo_frontend/assertions.mly
+++ b/src/mo_frontend/assertions.mly
@@ -40,6 +40,8 @@ let is_verification () =
     { is_verification () &&& AssertE(Static, e) @? at $sloc }
   | ASSERT COLON INVARIANT e=exp_nest
     { is_verification () &&& AssertE(Invariant, e) @? at $sloc }
+  | ASSERT COLON LOOP COLON INVARIANT e=exp_nest
+    { is_verification () &&& AssertE(Loop_invariant, e) @? at $sloc }
   | ASSERT COLON FUNC e=exp_nest
     { is_verification () &&& AssertE(Precondition, e) @? at $sloc }
   | ASSERT COLON RETURN e=exp_nest
diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
index 6e514e0e46f..2536f074003 100644
--- a/src/viper/pretty.ml
+++ b/src/viper/pretty.ml
@@ -152,9 +152,10 @@ and pp_stmt' ppf = function
       pp_exp exp1
       pp_seqn s1
       pp_seqn s2
-  | WhileS (exp, _, s) -> (* TODO: Invariant *)
-    fprintf ppf "@[<v 2>while (%a) {@ %a}@]"
+  | WhileS (exp, invs, s) ->
+    fprintf ppf "@[<v 2>while (%a)@;@[<v 0>%a@]@;%a@]"
       pp_exp exp
+      (pp_print_list pp_loop_inv) invs
       pp_seqn s
   | VarAssignS (id, exp) ->
     fprintf ppf "@[<v 2>%s := %a@]"
@@ -216,6 +217,9 @@ and pp_fldacc ppf fldacc =
   | (exp1, id) ->
     fprintf ppf "@[(%a).%s@]" pp_exp exp1 id.it
 
+and pp_loop_inv ppf inv =
+    fprintf ppf "invariant %a" pp_exp inv
+
 let prog_mapped file p =
     marks := [];
     let b = Buffer.create 16 in
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
index 37efb5479dc..d32b476048e 100644
--- a/src/viper/trans.ml
+++ b/src/viper/trans.ml
@@ -88,6 +88,18 @@ let rec extract_invariants : item list -> (par -> invariants -> invariants) = fu
         :: extract_invariants p self es
   | _ :: p -> extract_invariants p
 
+let rec extract_loop_invariants (e : M.exp) : (M.exp list * M.exp) =
+  match e with
+  | { it = M.BlockE ds; _ } ->
+    let (invs, ds') = extract_loop_invariants' ds [] in
+    (invs, { e with it = M.BlockE ds' })
+  | _ -> ([], e)
+and extract_loop_invariants' (ds : M.dec list) (acc : M.exp list) : (M.exp list * M.dec list) =
+  match ds with
+  | M.({ it = ExpD ({ it = AssertE (Loop_invariant, inv); _ }); _ }) :: ds ->
+      extract_loop_invariants' ds (inv :: acc)
+  | _ -> (List.rev acc, ds)
+
 let rec extract_concurrency (seq : seqn) : stmt' list * seqn =
   let open List in
   let extr (concs, stmts) s : stmt' list * stmt list =
@@ -390,8 +402,10 @@ and stmt ctxt (s : M.exp) : seqn =
                               !!(MacroCall("$Inv", self ctxt at))))));
         ])
   | M.WhileE(e, s1) ->
+     let (invs, s1') = extract_loop_invariants s1 in
+     let invs' = List.map (fun inv -> exp ctxt inv) invs in
      !!([],
-        [ !!(WhileS(exp ctxt e, [], stmt ctxt s1)) ]) (* TODO: Invariant *)
+        [ !!(WhileS(exp ctxt e, invs', stmt ctxt s1')) ])
   | M.(AssignE({it = VarE x; _}, e2)) ->
      begin match Env.find x.it ctxt.ids with
      | Local ->
diff --git a/test/fail/ok/verification-asserts.tc.ok b/test/fail/ok/verification-asserts.tc.ok
index 49ea928a86e..f68f697131e 100644
--- a/test/fail/ok/verification-asserts.tc.ok
+++ b/test/fail/ok/verification-asserts.tc.ok
@@ -8,3 +8,4 @@ verification-asserts.mo:7.8-7.17: syntax error [M0001], unexpected token 'invari
   invariant <exp_nest>
   func <exp_nest>
   <nat> : async <exp_nest>
+  loop : invariant <exp_nest>
diff --git a/test/fail/verification-asserts.mo b/test/fail/verification-asserts.mo
index 6be7d479170..caf95146b4b 100644
--- a/test/fail/verification-asserts.mo
+++ b/test/fail/verification-asserts.mo
@@ -5,3 +5,4 @@ assert:return true;
 
 // `invariant` is a keyword in verification mode only
 assert:invariant true;
+assert:loop:invariant true;
\ No newline at end of file
diff --git a/test/viper/loop-invariant.mo b/test/viper/loop-invariant.mo
new file mode 100644
index 00000000000..a243b2460aa
--- /dev/null
+++ b/test/viper/loop-invariant.mo
@@ -0,0 +1,15 @@
+// @verify
+
+actor LoopInvariant {
+  public func double(n : Int) : async Int {
+    var i : Int = 0;
+    var j : Int = 0;
+    while (i < n) {
+      assert:loop:invariant (i * 2 == j);
+      assert:loop:invariant (j - i == i);
+      i := i + 1;
+      j := j + 2;
+    };
+    return j;
+  };
+}
\ No newline at end of file
diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok
index 7593736d04b..4db1a7a12b5 100644
--- a/test/viper/ok/invariant.vpr.ok
+++ b/test/viper/ok/invariant.vpr.ok
@@ -34,9 +34,10 @@ method loops($Self: Ref)
     ensures $Inv($Self)
     { var i: Int
       i := 0
-      while ((i > 0)) {
+      while ((i > 0))
+         
          { 
            i := (i + 1) 
-         }}
+         }
       label $Ret 
     }
diff --git a/test/viper/ok/loop-invariant.silicon.ok b/test/viper/ok/loop-invariant.silicon.ok
new file mode 100644
index 00000000000..d7ae1e8621c
--- /dev/null
+++ b/test/viper/ok/loop-invariant.silicon.ok
@@ -0,0 +1,2 @@
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@1.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@2.1)
diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok
new file mode 100644
index 00000000000..d222eeac074
--- /dev/null
+++ b/test/viper/ok/loop-invariant.vpr.ok
@@ -0,0 +1,31 @@
+define $Perm($Self) (true)
+define $Inv($Self) (true)
+method __init__($Self: Ref)
+    
+    requires $Perm($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { 
+       
+    }
+method double($Self: Ref, n: Int)
+     returns ($Res: Int)
+    requires $Perm($Self)
+    requires $Inv($Self)
+    ensures $Perm($Self)
+    ensures $Inv($Self)
+    { var i: Int
+      var j: Int
+      i := 0
+      j := 0
+      while ((i < n))
+         invariant ((i * 2) == j)
+         invariant ((j - i) == i)
+         { 
+           i := (i + 1)
+           j := (j + 2) 
+         }
+      $Res := j
+      goto $Ret
+      label $Ret 
+    }
diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok
index ba1c971ba66..81d6dcc7626 100644
--- a/test/viper/ok/simple-funs.vpr.ok
+++ b/test/viper/ok/simple-funs.vpr.ok
@@ -105,11 +105,12 @@ method factorial($Self: Ref, n: Int)
       var i: Int
       prod := 1
       i := n
-      while ((i > 0)) {
+      while ((i > 0))
+         
          { 
            prod := (prod * i)
            i := (i - 1) 
-         }}
+         }
       $Res := prod
       goto $Ret
       label $Ret