diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs
index 5d61f3aebb..5a90611bf4 100644
--- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs
+++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs
@@ -79,6 +79,14 @@ public static string ExprToString(DafnyOptions options, Expression expr, [CanBeN
       return wr.ToString();
     }
 
+    public static string ForallExprRangeToString(DafnyOptions options, ForallExpr expr,
+      [CanBeNull] PrintFlags printFlags = null) {
+      using var wr = new StringWriter();
+      var pr = new Printer(wr, options, printFlags: printFlags);
+      pr.PrintQuantifierDomain(expr.BoundVars, expr.Attributes, expr.Range);
+      return wr.ToString();
+    }
+
     public static string ExprListToString(DafnyOptions options, List<Expression> expressions, [CanBeNull] PrintFlags printFlags = null) {
       Contract.Requires(expressions != null);
       using var wr = new StringWriter();
diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs
index 0a07486e22..9d9b0b9ae9 100644
--- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs
+++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs
@@ -5,6 +5,7 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using Castle.Core.Internal;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 using Xunit;
 using Xunit.Abstractions;
@@ -108,14 +109,104 @@ method Dac(c: L)
 }");
     }
 
+    [Fact]
+    public async Task TestCalcIntroduction() {
+      await TestCodeAction(@"
+method Test() {
+  assert 1 =><= 2(>Insert a calc statement-> by {
+    calc {
+      1;
+      2;
+    }
+  }:::;<)
+}");
+    }
+
+    [Fact]
+    public async Task TestCalcIntroductionEquiv() {
+      await TestCodeAction(@"
+method Test() {
+  assert true <=><=> false(>Insert a calc statement-> by {
+    calc <==> {
+      true;
+      false;
+    }
+  }:::;<)
+}");
+    }
+
+    [Fact]
+    public async Task TestForallIntroduction() {
+      await TestCodeAction(@"
+method Test() {
+  assert for><all i | i % 4 == 1 :: i % 2 == 0(>Insert a forall statement-> by {
+    forall i: int | i % 4 == 1 ensures i % 2 == 0 {
+      assert i % 2 == 0;
+    }
+  }:::;<)
+}");
+    }
+
+    [Fact]
+    public async Task TestForallIntroductionFunction() {
+      await TestCodeAction(@"
+function Test(): int {
+  assert for><all i | i % 4 == 1 :: i % 2 == 0(>Insert a forall statement-> by {
+    forall i: int | i % 4 == 1 ensures i % 2 == 0 {
+      assert i % 2 == 0;
+    }
+  }:::;<)
+  1
+}");
+    }
+
     [Fact]
     public async Task GitIssue4401CorrectInsertionPlace() {
       await TestCodeAction(@"
 predicate P(i: int)
 
-method Test() {(>Insert explicit failing assertion->
-  assert exists x: int :: P(x);<)
-  var x :><| P(x);
+method Test() {
+  var x :><| P(x)(>Insert explicit failing assertion-> by {
+    assert exists x: int :: P(x);
+  }:::;<)
+}");
+    }
+
+    [Fact]
+    public async Task InsertIntoByStatement() {
+      await TestCodeAction(@"
+predicate P(i: int)
+
+function Test(i: int): int
+  requires P(i) {
+  i
+}
+
+method TestMethod() {
+  assert Test><(1) == 1 by {
+    (>Insert explicit failing assertion->assert P(1);
+    <)calc {
+      1;
+      1;
+    }
+  }
+}");
+    }
+
+    [Fact]
+    public async Task InsertIntoEmptyByStatement() {
+      await TestCodeAction(@"
+predicate P(i: int)
+
+function Test(i: int): int
+  requires P(i) {
+  i
+}
+
+method TestMethod() {
+  assert Test><(1) == 1 by {
+  (>Insert explicit failing assertion->  assert P(1);
+  <)}
 }");
     }
 
@@ -126,9 +217,10 @@ module Test {
   class TheTest {
     predicate P(i: int)
 
-    method Test() {(>Insert explicit failing assertion->
-      assert exists x: int :: P(x);<)
-      var x :><| P(x);
+    method Test() {
+      var x :><| P(x)(>Insert explicit failing assertion-> by {
+        assert exists x: int :: P(x);
+      }:::;<)
     }
   }
 }");
@@ -254,17 +346,50 @@ match e
     }
 
     [Fact]
-    public async Task ExplicitDivisionByZero() {
+    public async Task ExplicitDivisionByZeroFunction() {
       await TestCodeAction(@"
-method Foo(i: int)
+function Foo(i: int): int
 {
   (>Insert explicit failing assertion->assert i + 1 != 0;
   <)var x := 2>< / (i + 1); 
+  x
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionByZeroMethod() {
+      await TestCodeAction(@"
+method Foo(i: int)
+{
+  var x := 2>< / (i + 1)(>Insert explicit failing assertion-> by {
+    assert i + 1 != 0;
+  }:::;<)
 }");
     }
 
     [Fact]
-    public async Task ExplicitDivisionImp() {
+    public async Task ExplicitDivisionImpFunction() {
+      await TestCodeAction(@"
+function Foo(b: bool, i: int, j: int): bool
+{
+  var x := b ==> (>Insert explicit failing assertion->assert i + 1 != 0;
+                 <)2 ></ (i + 1) == j;
+  x
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionImpImpMethod() {
+      await TestCodeAction(@"
+method Foo(b: bool, i: int, j: int)
+{
+  var x := b ==> b ==> (>Insert explicit failing assertion->assert i + 1 != 0;
+                       <)2 ></ (i + 1) == j;
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionImpMethod() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
 {
@@ -278,28 +403,53 @@ public async Task ExplicitDivisionImp2() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
 {
-  (>Insert explicit failing assertion->assert i + 1 != 0;
-  <)var x := 2 ></ (i + 1) == j ==> b;
+  var x := 2 ></ (i + 1) == j ==> b(>Insert explicit failing assertion-> by {
+    assert i + 1 != 0;
+  }:::;<)
 }");
     }
 
     [Fact]
-    public async Task ExplicitDivisionAnd() {
+    public async Task ExplicitDivisionAndFunction() {
       await TestCodeAction(@"
-method Foo(b: bool, i: int, j: int)
+function Foo(b: bool, i: int, j: int): bool
 {
   var x := b && (>Insert explicit failing assertion->assert i + 1 != 0;
                 <)2 ></ (i + 1) == j;
+  x
 }");
     }
 
+
     [Fact]
-    public async Task ExplicitDivisionAnd2() {
+    public async Task ExplicitDivisionAndMethod() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
+{
+  var x := b && (>Insert explicit failing assertion->assert i + 1 != 0;
+                <)2 ></ (i + 1) == j;
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionAnd2Function() {
+      await TestCodeAction(@"
+function Foo(b: bool, i: int, j: int): bool
 {
   (>Insert explicit failing assertion->assert i + 1 != 0;
   <)var x := 2 ></ (i + 1) == j && b;
+  x
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionAnd2Method() {
+      await TestCodeAction(@"
+method Foo(b: bool, i: int, j: int)
+{
+  var x := 2 ></ (i + 1) == j && b(>Insert explicit failing assertion-> by {
+    assert i + 1 != 0;
+  }:::;<)
 }");
     }
 
@@ -319,35 +469,69 @@ public async Task ExplicitDivisionOr2() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
 {
-  (>Insert explicit failing assertion->assert i + 1 != 0;
-  <)var x := 2 ></ (i + 1) == j || b;
+  var x := 2 ></ (i + 1) == j || b(>Insert explicit failing assertion-> by {
+    assert i + 1 != 0;
+  }:::;<)
 }");
     }
 
-
-
     [Fact]
     public async Task ExplicitDivisionAddParentheses() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
+{
+  var x := 2 ></ match b case true => i + 1 case false => i - 1(>Insert explicit failing assertion-> by {
+    assert (match b case true => i + 1 case false => i - 1) != 0;
+  }:::;<)
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionAddParentheses2() {
+      await TestCodeAction(@"
+function Foo(b: bool, i: int, j: int): int
 {
   (>Insert explicit failing assertion->assert (match b case true => i + 1 case false => i - 1) != 0;
   <)var x := 2 ></ match b case true => i + 1 case false => i - 1;
+  x
 }");
     }
 
     [Fact]
-    public async Task ExplicitDivisionExp() {
+    public async Task ExplicitDivisionExpMethod() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
+{
+  var x := b <== 2 ></ (i + 1) == j(>Insert explicit failing assertion-> by {
+    assert i + 1 != 0;
+  }:::;<)
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionExpFunction() {
+      await TestCodeAction(@"
+function Foo(b: bool, i: int, j: int): int
 {
   (>Insert explicit failing assertion->assert i + 1 != 0;
   <)var x := b <== 2 ></ (i + 1) == j;
+  2
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionExp2Function() {
+      await TestCodeAction(@"
+function Foo(b: bool, i: int, j: int): bool
+{
+  var x := (>Insert explicit failing assertion->(assert i + 1 != 0;
+            2 / (i + 1) == j):::2 ></ (i + 1) == j<) <== b;
+  x
 }");
     }
 
     [Fact]
-    public async Task ExplicitDivisionExp2() {
+    public async Task ExplicitDivisionExp2Method() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
 {
@@ -357,7 +541,7 @@ method Foo(b: bool, i: int, j: int)
     }
 
     [Fact]
-    public async Task ExplicitDivisionByZeroFunction() {
+    public async Task ExplicitDivisionByZeroIfFunction() {
       await TestCodeAction(@"
 function Foo(i: int): int
 {
@@ -372,7 +556,7 @@ function Foo(i: int): int
 
 
     [Fact]
-    public async Task ExplicitDivisionByZeroFunctionLetExpr() {
+    public async Task ExplicitDivisionByZeroMatchFunctionLetExpr() {
       await TestCodeAction(@"
 function Foo(i: int): int
 {
@@ -410,7 +594,9 @@ private async Task TestCodeAction(string source) {
         out var ranges);
       var documentItem = await CreateOpenAndWaitForResolve(output);
       var diagnostics = await GetLastDiagnostics(documentItem);
-      Assert.Equal(ranges.Count, diagnostics.Length);
+      if (ranges.Count != diagnostics.Length) {
+        Assert.True(ranges.Count == diagnostics.Length, string.Join("\n", diagnostics.Select(d => d.ToString())));
+      }
 
       if (positions.Count != ranges.Count) {
         positions = ranges.Select(r => r.Range.Start).ToList();
@@ -441,8 +627,13 @@ private async Task TestCodeAction(string source) {
           }
         }
 
-        Assert.True(found,
-          $"Did not find the code action '{expectedTitle}'. Available were:{string.Join(",", otherTitles)}");
+        if (otherTitles.IsNullOrEmpty()) {
+          // Parsing gone wrong, we display diagnostics
+          Assert.True(false, output + "\n" + string.Join("\n", diagnostics.Select(d => d.ToString())));
+        } else {
+          Assert.True(found,
+            $"Did not find the code action '{expectedTitle}'. Available were:{string.Join(",", otherTitles)}");
+        }
       }
     }
 
diff --git a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs
index ca0fd8b272..5a46455056 100644
--- a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs
+++ b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs
@@ -40,18 +40,19 @@ public ImplicitFailingAssertionCodeActionProvider(ILogger<DafnyCodeActionHandler
     return node.StartToken.line > 0 ? new List<INode> { node } : null;
   }
 
-  class ExplicitAssertionDafnyCodeAction : DafnyCodeAction {
-    private readonly DafnyOptions options;
-    private readonly Expression failingImplicitAssertion;
-    private readonly Node program;
-    private readonly Range selection;
+  abstract class StatementInsertingCodeAction : DafnyCodeAction {
+    protected readonly DafnyOptions options;
+    protected readonly Expression failingImplicitAssertion;
+    protected readonly Node program;
+    protected readonly Range selection;
 
-    public ExplicitAssertionDafnyCodeAction(
+    public StatementInsertingCodeAction(
       DafnyOptions options,
       Node program,
       Expression failingImplicitAssertion,
-      Range selection
-      ) : base("Insert explicit failing assertion") {
+      Range selection,
+      string message
+    ) : base(message) {
       this.options = options;
       this.failingImplicitAssertion = failingImplicitAssertion;
       this.program = program;
@@ -59,57 +60,197 @@ Range selection
     }
 
     public override IEnumerable<DafnyCodeActionEdit> GetEdits() {
-      var nodesTillFailure = FindInnermostNodeIntersecting(program, selection);
+      var insertionNode = GetFarthestNodeBeforeWhichAssertionCanBeInserted(program, selection, out var nodesTillFailure, out var needsIsolation);
+      if (insertionNode == null || nodesTillFailure == null) {
+        return new DafnyCodeActionEdit[] { };
+      }
 
-      var suggestedEdits = new List<DafnyCodeActionEdit>();
-      var needsIsolation = false;
-      if (nodesTillFailure == null) {
-        return suggestedEdits.ToArray();
+      var canHaveByBlock = insertionNode is AssertStmt or VarDeclStmt or CallStmt;
+      var canReplaceSemicolonWithByBlock =
+        canHaveByBlock &&
+        insertionNode.EndToken is { val: ";" };
+      if (canReplaceSemicolonWithByBlock) {
+        // We can insert a by block to keep the proof limited
+        var start = insertionNode.StartToken;
+        var indentation = IndentationFormatter.Whitespace(Math.Max(start.col - 1, 0));
+        var indentation2 = indentation + "  ";
+        var block = " by {\n" +
+                    indentation2 + GetStatementToInsert(indentation2) + "\n" +
+                    indentation + "}";
+        return ReplaceWith(insertionNode.EndToken, block);
       }
 
-      INode? insertionNode = null;
-      for (var i = 0; i < nodesTillFailure.Count; i++) {
-        var node = nodesTillFailure[i];
-        var nextNode = i < nodesTillFailure.Count - 1 ? nodesTillFailure[i + 1] : null;
-        if (node is Statement or LetExpr &&
-            ((node is AssignStatement or AssignSuchThatStmt && nextNode is not VarDeclStmt) ||
-            (node is not AssignStatement && nextNode is not VarDeclStmt && nextNode is not AssignSuchThatStmt))) {
-          insertionNode = node;
-          break;
+      var braceAfterByToken = canHaveByBlock && insertionNode.OwnedTokens.FirstOrDefault(t => t.val == "by") is { Next: { val: "{" } b }
+        ? b
+        : null;
+      if (braceAfterByToken != null) {
+        var start = braceAfterByToken.Next;
+        var isEmptyBy = start.Next is { val: "}" };
+        var innerCol = isEmptyBy ? start.col + 1 : start.col - 1;
+        var indentation = IndentationFormatter.Whitespace(Math.Max(innerCol, 0));
+        var indentationStart = IndentationFormatter.Whitespace(Math.Max(start.col - 1, 0));
+        var assertStr = GetStatementToInsert(indentation) + "\n" + indentationStart;
+        if (isEmptyBy) {
+          assertStr = "  " + assertStr;
         }
+        return PrefixWithStatement(start, start, false, assertStr);
+      } else {
+        var start = insertionNode.StartToken;
+        var indentation = IndentationFormatter.Whitespace(Math.Max(start.col - 1 + (needsIsolation ? 1 : 0), 0));
+        var assertStr = GetStatementToInsert(indentation) + "\n" + indentation;
+        return PrefixWithStatement(insertionNode.StartToken, insertionNode.EndToken, needsIsolation, assertStr);
+      }
+    }
 
-        if (nextNode is TopLevelDecl or MemberDecl or ITEExpr or MatchExpr or NestedMatchExpr
-            or NestedMatchCase) {
-          insertionNode = node;
-          break;
-        }
+    // Returns the node before which an implicit assertion can be inserted that should fix a failing assertion
+    // nodesSinceFailures is a list of node where the first node is the innermost one whose Range intersects with the selection range, and then each next node is the parent of the previous node.
+    // needsIsolation indicates if that insertion node will require parentheses because of associativity
+    // For example:
+    //   B ==> 1 / x == y
+    // if x is not proved to be nonzero, the insertion point has to be after the implication and before the 1/x, either
+    //   B ==> assert x != 0; (1 / x == y)
+    //   B ==> (assert x != 0; 1 / x) == y
+    // We prefer the first one, because it does not require parentheses. Moreover, if it is a top-level assertion, such as in:
+    //   assert 1 / x == y;
+    // Then rather than having a weird
+    //   assert assert x != 0; 1 / x == y;
+    // we can actually detect that the insertion point is surrounded by a node that supports
+    // by clauses and nicely push the assertion there
+    //   assert 1 / x == y by {
+    //     assert x != 0;
+    //   }
 
-        if (nextNode is BinaryExpr { Op: var op } binaryExpr &&
-            ((op == BinaryExpr.Opcode.Imp && node == binaryExpr.E1) ||
-             (op == BinaryExpr.Opcode.Exp && node == binaryExpr.E1) ||
-             (op == BinaryExpr.Opcode.And && node == binaryExpr.E1) ||
-             (op == BinaryExpr.Opcode.Or && node == binaryExpr.E1))) {
-          insertionNode = node;
-          needsIsolation = (op == BinaryExpr.Opcode.Exp && node == binaryExpr.E1);
-          break;
+    public static INode? GetFarthestNodeBeforeWhichAssertionCanBeInserted(Node program, Range selection, out List<INode>? nodesSinceFailure, out bool needsIsolation) {
+      nodesSinceFailure = FindInnermostNodeIntersecting(program, selection);
+
+      needsIsolation = false;
+
+      INode? insertionNode = null;
+      if (nodesSinceFailure != null) {
+        for (var i = 0; i < nodesSinceFailure.Count; i++) {
+          var node = nodesSinceFailure[i];
+          var nextNode = i < nodesSinceFailure.Count - 1 ? nodesSinceFailure[i + 1] : null;
+          if (node is Statement or LetExpr &&
+              ((node is AssignStatement or AssignSuchThatStmt && nextNode is not VarDeclStmt) ||
+               (node is not AssignStatement && nextNode is not VarDeclStmt && nextNode is not AssignSuchThatStmt))) {
+            insertionNode = node;
+            break;
+          }
+
+          if (nextNode is TopLevelDecl or MemberDecl or ITEExpr or MatchExpr or NestedMatchExpr
+              or NestedMatchCase) { // Nodes that change the path condition
+            insertionNode = node;
+            break;
+          }
+
+          if (nextNode is BinaryExpr { Op: var op } binaryExpr &&
+              ((op == BinaryExpr.Opcode.Imp && node == binaryExpr.E1) ||
+               (op == BinaryExpr.Opcode.Exp && node == binaryExpr.E1) ||
+               (op == BinaryExpr.Opcode.And && node == binaryExpr.E1) ||
+               (op == BinaryExpr.Opcode.Or && node == binaryExpr.E1))) {
+            insertionNode = node;
+            needsIsolation = (op == BinaryExpr.Opcode.Exp && node == binaryExpr.E1);
+            break;
+          }
         }
+
+        insertionNode ??= nodesSinceFailure[0];
+      } else {
+        insertionNode = null;
       }
 
-      insertionNode ??= nodesTillFailure[0];
+      return insertionNode;
+    }
 
-      var start = insertionNode.StartToken;
-      var assertStr = $"{(needsIsolation ? "(" : "")}assert {Printer.ExprToString(options, failingImplicitAssertion, new PrintFlags(UseOriginalDafnyNames: true))};\n" +
-                      IndentationFormatter.Whitespace(Math.Max(start.col - 1 + (needsIsolation ? 1 : 0), 0));
-      suggestedEdits.Add(
-        new DafnyCodeActionEdit(
-          InsertBefore(start), assertStr));
+    /// Helper for subclasses to print an expression
+    protected string S(Expression e) {
+      return Printer.ExprToString(options, e, new PrintFlags(UseOriginalDafnyNames: true));
+    }
+
+    /// Emit code editing instructions to insert the given statement before the given insertion node
+    /// Wraps everything with parentheses if it requires isolationn, which is the case in expressions notably
+    protected static IEnumerable<DafnyCodeActionEdit> PrefixWithStatement(Token start, Token end, bool needsIsolation, string statement) {
+      if (needsIsolation) {
+        statement = "(" + statement;
+      }
+      var suggestedEdits = new List<DafnyCodeActionEdit> {
+        new (InsertBefore(start), statement)
+      };
       if (needsIsolation) {
         suggestedEdits.Add(new DafnyCodeActionEdit(
-            InsertAfter(insertionNode.EndToken), ")"));
+          InsertAfter(end), ")"));
       }
 
       return suggestedEdits.ToArray();
     }
+
+    /// Emit code editing instructions to insert the given statement before the given insertion node
+    /// Wraps everything with parentheses if it requires isolationn, which is the case in expressions notably
+    protected static IEnumerable<DafnyCodeActionEdit> ReplaceWith(Token tokenToReplace, string block) {
+      var suggestedEdits = new List<DafnyCodeActionEdit> {
+        new (Replace(tokenToReplace), block)
+      };
+
+      return suggestedEdits.ToArray();
+    }
+
+
+    protected abstract string GetStatementToInsert(string indentation);
+  }
+
+  class ExplicitAssertionDafnyCodeAction : StatementInsertingCodeAction {
+    public ExplicitAssertionDafnyCodeAction(
+      DafnyOptions options,
+      Node program,
+      Expression failingImplicitAssertion,
+      Range selection
+      ) : base(options, program, failingImplicitAssertion, selection, "Insert explicit failing assertion") {
+    }
+
+    protected override string GetStatementToInsert(string indentation) {
+      return $"assert {S(failingImplicitAssertion)};";
+    }
+  }
+
+  class BinaryExprToCalcStatementCodeAction : StatementInsertingCodeAction {
+    private readonly BinaryExpr failingExplicit;
+
+    public BinaryExprToCalcStatementCodeAction(
+      DafnyOptions options,
+      Node program,
+      BinaryExpr failingExplicit,
+      Range selection
+      ) : base(options, program, failingExplicit, selection, "Insert a calc statement") {
+      this.failingExplicit = failingExplicit;
+    }
+
+    protected override string GetStatementToInsert(string i) {
+      var op = failingExplicit.Op is BinaryExpr.Opcode.Iff ? "<==> " : "";
+      return /*
+         */$"calc {op}{{\n" +
+        $"{i}  {S(failingExplicit.E0)};\n" +
+        $"{i}  {S(failingExplicit.E1)};\n" +
+        $"{i}}}";
+    }
+  }
+
+  class ForallExprStatementCodeAction : StatementInsertingCodeAction {
+    private readonly ForallExpr failingExplicit;
+
+    public ForallExprStatementCodeAction(
+      DafnyOptions options,
+      Node program,
+      ForallExpr failingExplicit,
+      Range selection
+    ) : base(options, program, failingExplicit, selection, "Insert a forall statement") {
+      this.failingExplicit = failingExplicit;
+    }
+
+    protected override string GetStatementToInsert(string i) {
+      return "forall " + Printer.ForallExprRangeToString(options, failingExplicit) + " ensures " + S(failingExplicit.Term) + " {\n" +
+           $"{i}  assert {S(failingExplicit.Term)};\n" +
+           $"{i}}}";
+    }
   }
 
   protected override IEnumerable<DafnyCodeAction>? GetDafnyCodeActions(IDafnyCodeActionInput input,
@@ -118,25 +259,37 @@ public override IEnumerable<DafnyCodeActionEdit> GetEdits() {
       return null;
     }
 
-    var failingExpressions = new List<Expression>() { };
+    var implicitlyFailing = new List<Expression>() { };
+    var explicitlyFailing = new List<Expression>() { };
     input.VerificationTree?.Visit(tree => {
       if (tree is AssertionVerificationTree assertTree &&
           assertTree.Finished &&
-            assertTree.Range.Intersects(selection) &&
-            assertTree.StatusVerification is GutterVerificationStatus.Error or GutterVerificationStatus.Inconclusive &&
-            assertTree.GetAssertion()?.Description is ProofObligationDescription description &&
-            description.GetAssertedExpr(options) is { } assertedExpr) {
+          assertTree.Range.Intersects(selection) &&
+          assertTree.StatusVerification is GutterVerificationStatus.Error or GutterVerificationStatus.Inconclusive &&
+          assertTree.GetAssertion()?.Description is ProofObligationDescription description &&
+          description.GetAssertedExpr(options) is { } assertedExpr) {
         if (description.IsImplicit) {
-          failingExpressions.Add(assertedExpr);
+          implicitlyFailing.Add(assertedExpr);
+        } else {
+          explicitlyFailing.Add(assertedExpr);
         }
       }
     });
-    if (failingExpressions.Count == 0) {
+    if (implicitlyFailing.Count == 0 && explicitlyFailing.Count == 0) {
       return null;
     }
 
-    return failingExpressions.Select(failingExpression =>
+    IEnumerable<DafnyCodeAction> suggestedExplicitAssertions = implicitlyFailing.Select(failingExpression =>
       new ExplicitAssertionDafnyCodeAction(options, input.Program, failingExpression, selection)
     );
+    IEnumerable<DafnyCodeAction> suggestedCalcStatements =
+      explicitlyFailing.OfType<BinaryExpr>().Where(b => b.Op is BinaryExpr.Opcode.Eq or BinaryExpr.Opcode.Iff).Select(failingEquality =>
+      new BinaryExprToCalcStatementCodeAction(options, input.Program, failingEquality, selection));
+    IEnumerable<DafnyCodeAction> suggestedForallStatements = explicitlyFailing
+      .OfType<ForallExpr>()
+      .Select(failingForall =>
+      new ForallExprStatementCodeAction(options, input.Program, failingForall, selection));
+
+    return suggestedExplicitAssertions.Concat(suggestedCalcStatements).Concat(suggestedForallStatements);
   }
 }
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs b/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs
index 2160c09437..9faee207aa 100644
--- a/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs
+++ b/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs
@@ -37,6 +37,10 @@ public abstract class DafnyCodeActionProvider {
   protected static SourceOrigin InsertBefore(Token tok) {
     return new SourceOrigin(tok, null);
   }
+
+  protected static SourceOrigin Replace(Token tok) {
+    return new SourceOrigin(tok, tok);
+  }
   protected static SourceOrigin InsertAfter(IOrigin tok) {
     return new SourceOrigin(new Token(tok.line, tok.col + tok.val.Length) {
       pos = tok.pos + tok.val.Length,
diff --git a/docs/dev/news/code-actions.feat b/docs/dev/news/code-actions.feat
new file mode 100644
index 0000000000..787286ffa8
--- /dev/null
+++ b/docs/dev/news/code-actions.feat
@@ -0,0 +1,4 @@
+Support for code actions in the language server to:
+- Insert failing implicit assertions in a "by" clause by preference.
+- Insert forall statement for any forall expressions that could not be proved
+- Insert calc statement for any equality that cannot be proved.
\ No newline at end of file