diff --git a/.github/workflows/compfuzzci.yaml b/.github/workflows/compfuzzci.yaml
new file mode 100644
index 00000000000..5541e4ed44f
--- /dev/null
+++ b/.github/workflows/compfuzzci.yaml
@@ -0,0 +1,90 @@
+name: CompFuzzCI
+on:
+  pull_request:
+    branches:
+      - master
+    types: [opened, closed, synchronize, reopened]
+  issues:
+    branches:
+      - master
+    types: [opened, closed, reopened]
+  
+jobs:
+  FuzzOnPR:
+    if: github.event_name == 'pull_request' && (github.event.action == 'opened' || github.event.action == 'reopened' || github.event.action == 'synchronize') && github.event.pull_request.base.ref == 'master'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'fuzz.yaml',
+                  ref: 'main',
+                  inputs: {
+                      commit: '${{ github.event.pull_request.head.sha }}',
+                      main_commit: '${{github.event.pull_request.base.sha}}',
+                      branch: '${{github.event.pull_request.head.ref}}',
+                      duration: '3600',
+                      instance: '5'
+                  }
+              })
+  UpdatePRClosed:
+    if: github.event_name == 'pull_request' && github.event.action == 'closed'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_pr_close.yaml',
+                  ref: 'main',
+                  inputs: {
+                      pr_number: '${{github.event.number}}'
+                  }
+              })
+  UpdateIssueOpened:
+    if: github.event_name == 'issues' && (github.event.action == 'opened' || github.event.action == 'reopened')  && github.event.pull_request.base.ref == 'master'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_issue_open.yaml',
+                  ref: 'main',
+                  inputs: {
+                      issue_number: '${{github.event.issue.number}}',
+                      issuer: '${{github.event.issue.user.login}}',
+                      commit: ${{ github.sha }}                
+                  }
+              })
+  UpdateIssueClosed:
+    if: github.event_name == 'issues' && github.event.action == 'closed'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_issue_close.yaml',
+                  ref: 'main',
+                  inputs: {
+                      issue_number: '${{github.event.issue.number}}'
+                  }
+              })
\ No newline at end of file
diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
index 26227fae09a..ef97d0be06f 100644
--- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
+++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
@@ -363,7 +363,7 @@ public void PrintStatement(Statement stmt, int indent) {
           wr.Write(" ");
         }
         PrintUpdateRHS(s, indent);
-        wr.Write(";");
+        PrintBy(s);
 
       } else if (stmt is CallStmt) {
         // Most calls are printed from their concrete syntax given in the input. However, recursive calls to
@@ -395,8 +395,7 @@ public void PrintStatement(Statement stmt, int indent) {
           wr.Write(" ");
           PrintUpdateRHS(s.Update, indent);
         }
-        wr.Write(";");
-
+        PrintBy(s.Update);
       } else if (stmt is VarDeclPattern) {
         var s = (VarDeclPattern)stmt;
         if (s.tok is AutoGeneratedToken) {
@@ -455,6 +454,20 @@ public void PrintStatement(Statement stmt, int indent) {
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
       }
+
+      void PrintBy(ConcreteUpdateStatement statement) {
+        BlockStmt proof = statement switch {
+          UpdateStmt updateStmt => updateStmt.Proof,
+          AssignOrReturnStmt returnStmt => returnStmt.Proof,
+          _ => null
+        };
+        if (proof != null) {
+          wr.Write(" by ");
+          PrintStatement(proof, indent);
+        } else {
+          wr.Write(";");
+        }
+      }
     }
 
     private void PrintHideReveal(HideRevealStmt revealStmt) {
diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
index f165d89b5f3..c7b1b971f80 100644
--- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
+++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
@@ -1,8 +1,11 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.Immutable;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using DafnyCore;
+using DafnyCore.Options;
 using Microsoft.Dafny.Auditor;
 using Microsoft.Dafny.Compilers;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -25,6 +28,18 @@ public enum ImplementationKind {
 public record Implements(ImplementationKind Kind, ModuleQualifiedId Target);
 
 public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable<ModuleDefinition>, IHasSymbolChildren {
+
+  public static readonly Option<bool> LegacyModuleNames = new("--legacy-module-names",
+    @"
+Generate module names in the older A_mB_mC style instead of the current A.B.C scheme".TrimStart()) {
+    IsHidden = true
+  };
+
+  static ModuleDefinition() {
+    DafnyOptions.RegisterLegacyUi(LegacyModuleNames, DafnyOptions.ParseBoolean, "Compilation options", legacyName: "legacyModuleNames", defaultValue: false);
+    OptionRegistry.RegisterOption(LegacyModuleNames, OptionScope.Translation);
+  }
+
   public IToken BodyStartTok = Token.NoToken;
   public IToken TokenWithTrailingDocString = Token.NoToken;
   public string DafnyName => NameNode.StartToken.val; // The (not-qualified) name as seen in Dafny source code
@@ -215,11 +230,15 @@ public string GetCompileName(DafnyOptions options) {
       if (IsBuiltinName) {
         compileName = Name;
       } else if (EnclosingModule is { TryToAvoidName: false }) {
-        // Include all names in the module tree path, to disambiguate when compiling
-        // a flat list of modules.
-        // Use an "underscore-escaped" character as a module name separator, since
-        // underscores are already used as escape characters in SanitizeName()
-        compileName = EnclosingModule.GetCompileName(options) + options.Backend.ModuleSeparator + NonglobalVariable.SanitizeName(Name);
+        if (options.Get(LegacyModuleNames)) {
+          compileName = SanitizedName;
+        } else {
+          // Include all names in the module tree path, to disambiguate when compiling
+          // a flat list of modules.
+          // Use an "underscore-escaped" character as a module name separator, since
+          // underscores are already used as escape characters in SanitizeName()
+          compileName = EnclosingModule.GetCompileName(options) + options.Backend.ModuleSeparator + NonglobalVariable.SanitizeName(Name);
+        }
       } else {
         compileName = NonglobalVariable.SanitizeName(Name);
       }
diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs
index 0b6199ae2bb..a598f530af8 100644
--- a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs
+++ b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs
@@ -9,6 +9,7 @@ public class AssignOrReturnStmt : ConcreteUpdateStatement, ICloneable<AssignOrRe
   public readonly ExprRhs Rhs; // this is the unresolved RHS, and thus can also be a method call
   public readonly List<AssignmentRhs> Rhss;
   public readonly AttributedToken KeywordToken;
+  public readonly BlockStmt Proof;
   [FilledInDuringResolution] public readonly List<Statement> ResolvedStatements = new List<Statement>();
   public override IEnumerable<Statement> SubStatements => ResolvedStatements;
   public override IToken Tok {
@@ -22,7 +23,7 @@ public override IToken Tok {
     }
   }
 
-  public override IEnumerable<INode> Children => ResolvedStatements;
+  public override IEnumerable<INode> Children => ResolvedStatements.Concat(Proof?.Children ?? new List<INode>());
   public override IEnumerable<Statement> PreResolveSubStatements => Enumerable.Empty<Statement>();
 
   [ContractInvariantMethod]
@@ -43,13 +44,14 @@ public AssignOrReturnStmt(Cloner cloner, AssignOrReturnStmt original) : base(clo
     Rhs = (ExprRhs)cloner.CloneRHS(original.Rhs);
     Rhss = original.Rhss.ConvertAll(cloner.CloneRHS);
     KeywordToken = cloner.AttributedTok(original.KeywordToken);
+    Proof = cloner.CloneBlockStmt(original.Proof);
 
     if (cloner.CloneResolvedFields) {
       ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList();
     }
   }
 
-  public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs rhs, AttributedToken keywordToken, List<AssignmentRhs> rhss)
+  public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs rhs, AttributedToken keywordToken, List<AssignmentRhs> rhss, BlockStmt proof = null)
     : base(rangeToken, lhss) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(lhss != null);
@@ -59,6 +61,7 @@ public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs
     Rhs = rhs;
     Rhss = rhss;
     KeywordToken = keywordToken;
+    Proof = proof;
   }
 
   public override IEnumerable<Expression> PreResolveSubExpressions {
@@ -190,6 +193,8 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
       return;
     }
 
+    ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext);
+
     Expression lhsExtract = null;
     if (expectExtract) {
       if (resolutionContext.CodeContext is Method caller && caller.Outs.Count == 0 && KeywordToken == null) {
@@ -285,7 +290,7 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract,
       }
     }
     // " temp, ... := MethodOrExpression, ...;"
-    UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2);
+    UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2, Proof);
     if (expectExtract) {
       up.OriginalInitialLhs = Lhss.Count == 0 ? null : Lhss[0];
     }
diff --git a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs
index cc3fe0507f1..0b61df6ab30 100644
--- a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs
+++ b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs
@@ -8,6 +8,7 @@ public class UpdateStmt : ConcreteUpdateStatement, ICloneable<UpdateStmt>, ICanR
   public readonly List<AssignmentRhs> Rhss;
   public readonly bool CanMutateKnownState;
   public Expression OriginalInitialLhs = null;
+  public readonly BlockStmt Proof;
 
   public override IToken Tok {
     get {
@@ -22,7 +23,7 @@ public override IToken Tok {
   }
 
   [FilledInDuringResolution] public List<Statement> ResolvedStatements;
-  public override IEnumerable<Statement> SubStatements => Children.OfType<Statement>();
+  public override IEnumerable<Statement> SubStatements => Children.OfType<Statement>().Concat(Proof != null ? Proof.SubStatements : new List<Statement>());
 
   public override IEnumerable<Expression> NonSpecificationSubExpressions =>
     ResolvedStatements == null ? Rhss.SelectMany(r => r.NonSpecificationSubExpressions) : Enumerable.Empty<Expression>();
@@ -45,26 +46,29 @@ public UpdateStmt Clone(Cloner cloner) {
   public UpdateStmt(Cloner cloner, UpdateStmt original) : base(cloner, original) {
     Rhss = original.Rhss.Select(cloner.CloneRHS).ToList();
     CanMutateKnownState = original.CanMutateKnownState;
+    Proof = cloner.CloneBlockStmt(original.Proof);
     if (cloner.CloneResolvedFields) {
       ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList();
     }
   }
 
-  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss)
+  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, BlockStmt proof = null)
     : base(rangeToken, lhss) {
     Contract.Requires(cce.NonNullElements(lhss));
     Contract.Requires(cce.NonNullElements(rhss));
     Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
     Rhss = rhss;
     CanMutateKnownState = false;
+    Proof = proof;
   }
-  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate)
+  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate, BlockStmt proof = null)
     : base(rangeToken, lhss) {
     Contract.Requires(cce.NonNullElements(lhss));
     Contract.Requires(cce.NonNullElements(rhss));
     Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
     Rhss = rhss;
     CanMutateKnownState = mutate;
+    Proof = proof;
   }
 
   public override IEnumerable<Expression> PreResolveSubExpressions {
@@ -123,6 +127,9 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
       resolver.ResolveAttributes(rhs, resolutionContext);
     }
 
+    // resolve proof
+    ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext);
+
     // figure out what kind of UpdateStmt this is
     if (firstEffectfulRhs == null) {
       if (Lhss.Count == 0) {
@@ -178,7 +185,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
         foreach (var ll in Lhss) {
           resolvedLhss.Add(ll.Resolved);
         }
-        CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok);
+        CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok, Proof);
         a.OriginalInitialLhs = OriginalInitialLhs;
         ResolvedStatements.Add(a);
       }
diff --git a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs
index fc52debc2a6..41348dae006 100644
--- a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs
+++ b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs
@@ -25,11 +25,12 @@ void ObjectInvariant() {
   public readonly ActualBindings Bindings;
   public List<Expression> Args => Bindings.Arguments;
   public Expression OriginalInitialLhs = null;
+  public readonly BlockStmt Proof;
 
   public Expression Receiver { get { return MethodSelect.Obj; } }
   public Method Method { get { return (Method)MethodSelect.Member; } }
 
-  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args, IToken overrideToken = null)
+  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args, IToken overrideToken = null, BlockStmt proof = null)
     : base(rangeToken) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(cce.NonNullElements(lhs));
@@ -41,6 +42,7 @@ public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr me
     this.MethodSelect = memSel;
     this.overrideToken = overrideToken;
     this.Bindings = new ActualBindings(args);
+    Proof = proof;
   }
 
   public CallStmt Clone(Cloner cloner) {
@@ -52,14 +54,15 @@ public CallStmt(Cloner cloner, CallStmt original) : base(cloner, original) {
     Lhs = original.Lhs.Select(cloner.CloneExpr).ToList();
     Bindings = new ActualBindings(cloner, original.Bindings);
     overrideToken = original.overrideToken;
+    Proof = cloner.CloneBlockStmt(original.Proof);
   }
 
   /// <summary>
   /// This constructor is intended to be used when constructing a resolved CallStmt. The "args" are expected
   /// to be already resolved, and are all given positionally.
   /// </summary>
-  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args)
-    : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e))) {
+  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args, BlockStmt proof = null)
+    : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e)), proof: proof) {
     Bindings.AcceptArgumentExpressionsAsExactParameterList();
   }
 
diff --git a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs
index 295803e9e6e..306f1d4815b 100644
--- a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs
+++ b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs
@@ -89,16 +89,7 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext co
 
     base.GenResolve(resolver, context);
 
-    if (Proof != null) {
-      // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave a the proof body
-      var prevLblStmts = resolver.EnclosingStatementLabels;
-      var prevLoopStack = resolver.LoopStack;
-      resolver.EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
-      resolver.LoopStack = new List<Statement>();
-      resolver.ResolveStatement(Proof, context);
-      resolver.EnclosingStatementLabels = prevLblStmts;
-      resolver.LoopStack = prevLoopStack;
-    }
+    ModuleResolver.ResolveByProof(resolver, Proof, context);
   }
 
   public bool HasAssertOnlyAttribute(out AssertOnlyKind assertOnlyKind) {
diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
index 7c9eaa7c000..d069d01cb73 100644
--- a/Source/DafnyCore/Dafny.atg
+++ b/Source/DafnyCore/Dafny.atg
@@ -2297,6 +2297,7 @@ UpdateStmt<out Statement/*!*/ s>
      List<AssignmentRhs> rhss = new List<AssignmentRhs>();
      Expression e;
      AssignmentRhs r;
+     BlockStmt proof = null;
      IToken x = Token.NoToken;
      IToken endTok = Token.NoToken;
      IToken startToken = Token.NoToken;
@@ -2334,10 +2335,16 @@ UpdateStmt<out Statement/*!*/ s>
       { "," Rhs<out r>             (. rhss.Add(r); .)
       }
     )
-    ";"                            (. endTok = t; .)
+    (
+      "by" BlockStmt<out proof, out _, out _>
+    | ";"
+    )
   | ":"                            (. SemErr(ErrorId.p_invalid_colon, new RangeToken(startToken, t), "invalid statement beginning here (is a 'label' keyword missing? or a 'const' or 'var' keyword?)"); .)
   | { Attribute<ref attrs> }       (. endToken = t; .)
-    ";"                            (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); .)   
+    (
+      "by" BlockStmt<out proof, out _, out _>
+    | ";"
+    )                              (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) }); .)
   | { Attribute<ref attrs> }       (. endToken = t; .)
                                    (. endTok = t; rhss.Add(new ExprRhs(e, attrs) { RangeToken = new RangeToken(e.StartToken, endToken) });
                                       SemErr(ErrorId.p_missing_semicolon, new RangeToken(startToken, t), "missing semicolon at end of statement");
@@ -2352,18 +2359,21 @@ UpdateStmt<out Statement/*!*/ s>
    { Attribute<ref attrs> }        (. exceptionRhs = new ExprRhs(exceptionExpr, attrs); .)
    { "," Rhs<out r>                (. rhss.Add(r); .)
    }
-   ";"                             (. endTok = t; .)
+   (
+     "by" BlockStmt<out proof, out _, out _>
+   | ";"                           (. endTok = t; .)
+   )                           
 )
   (. var rangeToken = new RangeToken(startToken, t);
      if (suchThat != null) {
        s = new AssignSuchThatStmt(rangeToken, lhss, suchThat, suchThatAssume, null);
      } else if (exceptionRhs != null) {
-       s = new AssignOrReturnStmt(rangeToken, lhss, exceptionRhs, keywordToken, rhss);
+       s = new AssignOrReturnStmt(rangeToken, lhss, exceptionRhs, keywordToken, rhss, proof);
      } else {
        if (lhss.Count == 0 && rhss.Count == 0) {
          s = new BlockStmt(rangeToken, new List<Statement>()); // error, give empty statement
        } else {
-         s = new UpdateStmt(rangeToken, lhss, rhss);
+         s = new UpdateStmt(rangeToken, lhss, rhss, proof);
        }
      }
   .)
@@ -2463,6 +2473,7 @@ VarDeclStatement<.out Statement/*!*/ s.>
      ExprRhs exceptionRhs = null;
      Attributes attrs = null;
      Attributes tokenAttrs = null;
+     BlockStmt proof = null;
      IToken endTok;
      IToken startToken = null;
      s = dummyStmt;
@@ -2499,7 +2510,10 @@ VarDeclStatement<.out Statement/*!*/ s.>
       { "," Rhs<out r>               (. rhss.Add(r); .)
       }
     ]
-    SYNC ";"                         (. endTok = t; .)
+    SYNC ( "by"
+      BlockStmt<out proof, out _, out _>
+    | ";"                            (. endTok = t; .)
+    )
     (. ConcreteUpdateStatement update;
        var lhsExprs = new List<Expression>();
        if (isGhost || (rhss.Count == 0 && exceptionRhs == null && suchThat == null)) { // explicitly ghost or no init
@@ -2516,11 +2530,11 @@ VarDeclStatement<.out Statement/*!*/ s.>
        if (suchThat != null) {
          update = new AssignSuchThatStmt(updateRangeToken, lhsExprs, suchThat, suchThatAssume, attrs);
        } else if (exceptionRhs != null) {
-         update = new AssignOrReturnStmt(updateRangeToken, lhsExprs, exceptionRhs, keywordToken, rhss);
+         update = new AssignOrReturnStmt(updateRangeToken, lhsExprs, exceptionRhs, keywordToken, rhss, proof);
        } else if (rhss.Count == 0) {
          update = null;
        } else {
-         update = new UpdateStmt(updateRangeToken, lhsExprs, rhss);
+         update = new UpdateStmt(updateRangeToken, lhsExprs, rhss, proof);
        }
        s = new VarDeclStmt(rangeToken, lhss, update);
     .)
diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs
index 74acb94d988..d3d3eadbe7a 100644
--- a/Source/DafnyCore/Options/DafnyCommands.cs
+++ b/Source/DafnyCore/Options/DafnyCommands.cs
@@ -58,6 +58,7 @@ static DafnyCommands() {
     CommonOptionBag.AddCompileSuffix,
     CommonOptionBag.SystemModule,
     IExecutableBackend.TranslationRecords,
+    ModuleDefinition.LegacyModuleNames
   }.Concat(VerificationOptions).ToList();
 
   public static readonly IReadOnlyList<Option> ExecutionOptions = new Option[] {
diff --git a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs
index df6868accd8..149e330a040 100644
--- a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs
+++ b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs
@@ -145,6 +145,9 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
       var s = (UpdateStmt)stmt;
       s.ResolvedStatements.ForEach(ss => Visit(ss, mustBeErasable, proofContext));
       s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost);
+      if (s.Proof != null) {
+        Visit(s.Proof, true, "a call-by body");
+      }
 
     } else if (stmt is AssignOrReturnStmt) {
       var s = (AssignOrReturnStmt)stmt;
diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs
index 22d0c818442..18d48daf379 100644
--- a/Source/DafnyCore/Resolver/ModuleResolver.cs
+++ b/Source/DafnyCore/Resolver/ModuleResolver.cs
@@ -3311,6 +3311,21 @@ internal LetExpr LetVarIn(IToken tok, string name, Type tp, Expression rhs, Expr
       return LetPatIn(tok, lhs, rhs, body);
     }
 
+    internal static void ResolveByProof(INewOrOldResolver resolver, BlockStmt proof, ResolutionContext resolutionContext) {
+      if (proof == null) {
+        return;
+      }
+
+      // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave the proof body
+      var prevLblStmts = resolver.EnclosingStatementLabels;
+      var prevLoopStack = resolver.LoopStack;
+      resolver.EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
+      resolver.LoopStack = new List<Statement>();
+      resolver.ResolveStatement(proof, resolutionContext);
+      resolver.EnclosingStatementLabels = prevLblStmts;
+      resolver.LoopStack = prevLoopStack;
+    }
+
     /// <summary>
     ///  If expr.Lhs != null: Desugars "var x: T :- E; F" into "var temp := E; if temp.IsFailure() then temp.PropagateFailure() else var x: T := temp.Extract(); F"
     ///  If expr.Lhs == null: Desugars "         :- E; F" into "var temp := E; if temp.IsFailure() then temp.PropagateFailure() else                             F"
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
index 3764e520a4d..129978be951 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
+++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs
@@ -621,7 +621,8 @@ void ResolveAssignmentRhs(AssignmentRhs rhs, Statement enclosingStmt, Resolution
     /// errorCountBeforeCheckingStmt is passed in so that this method can determine if any resolution errors were found during
     /// LHS or RHS checking, because only if no errors were found is update.ResolvedStmt changed.
     /// </summary>
-    private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionContext, int errorCountBeforeCheckingStmt) {
+    private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionContext,
+      int errorCountBeforeCheckingStmt) {
       Contract.Requires(update != null);
       Contract.Requires(resolutionContext != null);
       IToken firstEffectfulRhs = null;
@@ -643,6 +644,7 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo
             isEffectful = false;
           }
         }
+
         if (isEffectful && firstEffectfulRhs == null) {
           firstEffectfulRhs = rhs.Tok;
         }
@@ -650,13 +652,17 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo
         ResolveAttributes(rhs, resolutionContext, false);
       }
 
+      // resolve proof
+      ModuleResolver.ResolveByProof(this, update.Proof, resolutionContext);
+
       // figure out what kind of UpdateStmt this is
       if (firstEffectfulRhs == null) {
         if (update.Lhss.Count == 0) {
-          Contract.Assert(update.Rhss.Count == 1);  // guaranteed by the parser
+          Contract.Assert(update.Rhss.Count == 1); // guaranteed by the parser
           ReportError(update, "expected method call, found expression");
         } else if (update.Lhss.Count != update.Rhss.Count) {
-          ReportError(update, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment",
+          ReportError(update,
+            "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment",
             update.Lhss.Count, update.Rhss.Count);
         } else if (ErrorCount == errorCountBeforeCheckingStmt) {
           // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translate properly as multi-assignment)
@@ -669,7 +675,8 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo
       } else if (update.CanMutateKnownState) {
         if (1 < update.Rhss.Count) {
           ReportError(firstEffectfulRhs, "cannot have effectful parameter in multi-return statement.");
-        } else { // it might be ok, if it is a TypeRhs
+        } else {
+          // it might be ok, if it is a TypeRhs
           Contract.Assert(update.Rhss.Count == 1);
           if (methodCallInfo != null) {
             ReportError(methodCallInfo.Tok, "cannot have method call in return statement.");
@@ -689,12 +696,16 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo
       } else {
         // if there was an effectful RHS, that must be the only RHS
         if (update.Rhss.Count != 1) {
-          ReportError(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");
+          ReportError(firstEffectfulRhs,
+            "an update statement is allowed an effectful RHS only if there is just one RHS");
         } else if (methodCallInfo == null) {
           // must be a single TypeRhs
           if (update.Lhss.Count != 1) {
-            Contract.Assert(2 <= update.Lhss.Count);  // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
-            ReportError(update.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment",
+            Contract.Assert(2 <=
+                            update.Lhss
+                              .Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
+            ReportError(update.Lhss[1].tok,
+              "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment",
               update.Lhss.Count, update.Rhss.Count);
           } else if (ErrorCount == errorCountBeforeCheckingStmt) {
             var a = new AssignStmt(update.RangeToken, update.Lhss[0].Resolved, update.Rhss[0]);
@@ -703,7 +714,8 @@ private void ResolveUpdateStmt(UpdateStmt update, ResolutionContext resolutionCo
         } else if (ErrorCount == errorCountBeforeCheckingStmt) {
           // a call statement
           var resolvedLhss = update.Lhss.ConvertAll(ll => ll.Resolved);
-          var a = new CallStmt(update.RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok);
+          var a = new CallStmt(update.RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters,
+            methodCallInfo.Tok, update.Proof);
           a.OriginalInitialLhs = update.OriginalInitialLhs;
           update.ResolvedStatements.Add(a);
         }
@@ -929,6 +941,8 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r
         return;
       }
 
+      ModuleResolver.ResolveByProof(this, s.Proof, resolutionContext);
+
       Expression lhsExtract = null;
       if (expectExtract) {
         if (enclosingMethod.Outs.Count == 0 && s.KeywordToken == null) {
@@ -991,7 +1005,7 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r
         }
       }
       // " temp, ... := MethodOrExpression, ...;"
-      UpdateStmt up = new UpdateStmt(s.RangeToken, lhss2, rhss2);
+      UpdateStmt up = new UpdateStmt(s.RangeToken, lhss2, rhss2, s.Proof);
       if (expectExtract) {
         up.OriginalInitialLhs = s.Lhss.Count == 0 ? null : s.Lhss[0];
       }
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs
index b08bf91f8a4..6ba4aef2c77 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs
@@ -95,7 +95,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) {
             p.Label.E = etran.Old.TrExpr(p.E);
           } else {
             foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(false), p.E, etran, kind)) {
-              if (kind == MethodTranslationKind.Call && RefinementToken.IsInherited(s.Tok, currentModule)) {
+              if (kind == MethodTranslationKind.CallPre && RefinementToken.IsInherited(s.Tok, currentModule)) {
                 // this precondition was inherited into this module, so just ignore it
               } else {
                 req.Add(Requires(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment));
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
index bb8baa41705..1bf6968bfb8 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
@@ -193,13 +193,17 @@ void AddMethod_Top(Method m, bool isByMethod, bool includeAllMethods) {
       }
       // the method spec itself
       if (!isByMethod) {
-        sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.Call));
+        sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CallPre));
+        sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CallPost));
+
       }
       if (m is ExtremeLemma) {
         // Let the CoCall and Impl forms to use m.PrefixLemma signature and specification (and
         // note that m.PrefixLemma.Body == m.Body.
         m = ((ExtremeLemma)m).PrefixLemma;
-        sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CoCall));
+        sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CoCallPre));
+        sink.AddTopLevelDeclaration(AddMethod(m, MethodTranslationKind.CoCallPost));
+
       }
       if (!m.HasVerifyFalseAttribute && m.Body != null && InVerificationScope(m)) {
         // ...and its implementation
@@ -1696,6 +1700,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
       var ordinaryEtran = new ExpressionTranslator(this, predef, m.tok, m);
       ExpressionTranslator etran;
       var inParams = new List<Boogie.Variable>();
+      var bodyKind = kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation;
       if (m is TwoStateLemma) {
         var prevHeapVar = new Boogie.Formal(m.tok, new Boogie.TypedIdent(m.tok, "previous$Heap", predef.HeapType), true);
         var currHeapVar = new Boogie.Formal(m.tok, new Boogie.TypedIdent(m.tok, "current$Heap", predef.HeapType), true);
@@ -1710,49 +1715,48 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
 
       GenerateMethodParameters(m.tok, m, kind, etran, inParams, out var outParams);
 
-      var req = new List<Boogie.Requires>();
-      var mod = new List<Boogie.IdentifierExpr>();
-      var ens = new List<Boogie.Ensures>();
-      // FREE PRECONDITIONS
-      if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation || kind == MethodTranslationKind.OverrideCheck) {  // the other cases have no need for a free precondition
-        // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
-        req.Add(Requires(m.tok, true, null, etran.HeightContext(m), null, null, null));
-        if (m is TwoStateLemma) {
-          // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
-          var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
-          var a1 = HeapSucc(prevHeap, currHeap);
-          var a2 = FunctionCall(m.tok, BuiltinFunction.IsGoodHeap, null, currHeap);
-          req.Add(Requires(m.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null));
-        }
+      List<Boogie.Requires> GetRequires() {
+        var req = new List<Boogie.Requires>();
+        // FREE PRECONDITIONS
+        if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation || kind == MethodTranslationKind.OverrideCheck) {  // the other cases have no need for a free precondition
+          // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
+          req.Add(Requires(m.tok, true, null, etran.HeightContext(m), null, null, null));
+          if (m is TwoStateLemma) {
+            // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
+            var a0 = Boogie.Expr.Eq(prevHeap, ordinaryEtran.HeapExpr);
+            var a1 = HeapSucc(prevHeap, currHeap);
+            var a2 = FunctionCall(m.tok, BuiltinFunction.IsGoodHeap, null, currHeap);
+            req.Add(Requires(m.tok, true, null, BplAnd(a0, BplAnd(a1, a2)), null, null, null));
+          }
 
-        foreach (var typeBoundAxiom in TypeBoundAxioms(m.tok, Concat(m.EnclosingClass.TypeArgs, m.TypeArgs))) {
-          req.Add(Requires(m.tok, true, null, typeBoundAxiom, null, null, null));
+          foreach (var typeBoundAxiom in TypeBoundAxioms(m.tok, Concat(m.EnclosingClass.TypeArgs, m.TypeArgs))) {
+            req.Add(Requires(m.tok, true, null, typeBoundAxiom, null, null, null));
+          }
         }
-      }
-      if (m is TwoStateLemma) {
-        // Checked preconditions that old parameters really existed in previous state
-        var index = 0;
-        foreach (var formal in m.Ins) {
-          if (formal.IsOld) {
-            var dafnyFormalIdExpr = new IdentifierExpr(formal.tok, formal);
-            var pIdx = m.Ins.Count == 1 ? "" : " at index " + index;
-            var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'",
-              "in the two-state lemma's previous state" + PODesc.IsAllocated.HelperFormal(formal),
-              dafnyFormalIdExpr
-            );
-            var require = Requires(formal.tok, false, null, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap),
-              desc.FailureDescription, desc.SuccessDescription, null);
-            require.Description = desc;
-            req.Add(require);
+        if (m is TwoStateLemma) {
+          // Checked preconditions that old parameters really existed in previous state
+          var index = 0;
+          foreach (var formal in m.Ins) {
+            if (formal.IsOld) {
+              var dafnyFormalIdExpr = new IdentifierExpr(formal.tok, formal);
+              var pIdx = m.Ins.Count == 1 ? "" : " at index " + index;
+              var desc = new PODesc.IsAllocated($"argument{pIdx} for parameter '{formal.Name}'",
+                "in the two-state lemma's previous state" + PODesc.IsAllocated.HelperFormal(formal),
+                dafnyFormalIdExpr
+              );
+              var require = Requires(formal.tok, false, null, MkIsAlloc(etran.TrExpr(dafnyFormalIdExpr), formal.Type, prevHeap),
+                desc.FailureDescription, desc.SuccessDescription, null);
+              require.Description = desc;
+              req.Add(require);
+            }
+            index++;
           }
-          index++;
         }
-      }
-      mod.Add(ordinaryEtran.HeapCastToIdentifierExpr);
 
-      var bodyKind = kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation;
+        if (kind is MethodTranslationKind.SpecWellformedness or MethodTranslationKind.OverrideCheck) {
+          return req;
+        }
 
-      if (kind != MethodTranslationKind.SpecWellformedness && kind != MethodTranslationKind.OverrideCheck) {
         // USER-DEFINED SPECIFICATIONS
         var comment = "user-defined preconditions";
         foreach (var p in m.Req) {
@@ -1761,20 +1765,32 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
             // don't include this precondition here, but record it for later use
             p.Label.E = (m is TwoStateLemma ? ordinaryEtran : etran.Old).TrExpr(p.E);
           } else {
-            foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(m.ContainsHide), p.E, etran, kind)) {
+            foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(m.ContainsHide), p.E, etran,
+                       kind)) {
               if (s.IsOnlyChecked && bodyKind) {
                 // don't include in split
               } else if (s.IsOnlyFree && !bodyKind) {
                 // don't include in split -- it would be ignored, anyhow
               } else {
-                req.Add(RequiresWithDependencies(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment));
+                req.Add(
+                  RequiresWithDependencies(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment));
                 comment = null;
                 // the free here is not linked to the free on the original expression (this is free things generated in the splitting.)
               }
             }
           }
         }
-        comment = "user-defined postconditions";
+        return req;
+      }
+
+      List<Boogie.Ensures> GetEnsures() {
+        var ens = new List<Boogie.Ensures>();
+        if (kind is MethodTranslationKind.SpecWellformedness or MethodTranslationKind.OverrideCheck) {
+          return ens;
+        }
+
+        // USER-DEFINED SPECIFICATIONS
+        var comment = "user-defined postconditions";
         foreach (var p in m.Ens) {
           var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes);
           AddEnsures(ens, Ensures(p.E.tok, true, p.E, etran.CanCallAssumption(p.E), errorMessage, successMessage, comment));
@@ -1794,7 +1810,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
             }
           }
         }
-        if (m is Constructor && kind == MethodTranslationKind.Call) {
+        if (m is Constructor && kind == MethodTranslationKind.CallPost) {
           var dafnyFresh = new OldExpr(Token.NoToken,
             new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Not,
               new UnaryOpExpr(Token.NoToken, UnaryOpExpr.Opcode.Allocated, new IdentifierExpr(Token.NoToken, "this"))));
@@ -1816,9 +1832,31 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
             }
           }
         }
+        return ens;
       }
 
+      var req = new List<Bpl.Requires>();
+      var mod = new List<Boogie.IdentifierExpr>();
+      var ens = new List<Ensures>();
+
       var name = MethodName(m, kind);
+      switch (kind) {
+        case MethodTranslationKind.CallPre:
+        case MethodTranslationKind.CoCallPre:
+          outParams = new List<Variable>();
+          req = GetRequires();
+          break;
+        case MethodTranslationKind.CallPost:
+        case MethodTranslationKind.CoCallPost:
+          mod.Add(ordinaryEtran.HeapCastToIdentifierExpr);
+          ens = GetEnsures();
+          break;
+        default:
+          req = GetRequires();
+          mod.Add(ordinaryEtran.HeapCastToIdentifierExpr);
+          ens = GetEnsures();
+          break;
+      }
       var proc = new Boogie.Procedure(m.tok, name, new List<Boogie.TypeVariable>(), inParams, outParams, false, req, mod, ens, etran.TrAttributes(m.Attributes, null));
       AddVerboseNameAttribute(proc, m.FullDafnyName, kind);
 
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
index 90d579f3715..692f9a0e5fd 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs
@@ -1793,20 +1793,17 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
         }
       }
 
-      MethodTranslationKind kind;
+      bool isCoCall = false;
       var callee = method;
       if (method is ExtremeLemma && isRecursiveCall) {
-        kind = MethodTranslationKind.CoCall;
+        isCoCall = true;
         callee = ((ExtremeLemma)method).PrefixLemma;
       } else if (method is PrefixLemma) {
         // an explicit call to a prefix lemma is allowed only inside the SCC of the corresponding greatest lemma,
         // so we consider this to be a co-call
-        kind = MethodTranslationKind.CoCall;
-      } else {
-        kind = MethodTranslationKind.Call;
+        isCoCall = true;
       }
 
-
       var ins = new List<Bpl.Expr>();
       if (callee is TwoStateLemma) {
         ins.Add(etran.OldAt(atLabel).HeapExpr);
@@ -2002,22 +1999,41 @@ void ProcessCallStmt(CallStmt cs, Dictionary<TypeParameter, Type> tySubst, Bpl.E
         }
       }
 
+      if (cs.Proof == null) {
+        AddCall(builder);
+      } else {
+        var callBuilder = new BoogieStmtListBuilder(this, options, builder.Context);
+        AddComment(callBuilder, cs, "call statement proof");
+        CurrentIdGenerator.Push();
+        TrStmt(cs.Proof, callBuilder, locals, etran);
+        CurrentIdGenerator.Pop();
+        AddCall(callBuilder);
+        PathAsideBlock(cs.Tok, callBuilder, builder);
+      }
+
+      void AddCall(BoogieStmtListBuilder callBuilder) {
+        callBuilder.Add(new CommentCmd($"ProcessCallStmt: Check precondition"));
+        // Make the call
+        AddReferencedMember(callee);
+        Bpl.CallCmd call = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPre : MethodTranslationKind.CallPre), ins, new List<Bpl.IdentifierExpr>());
+        proofDependencies?.AddProofDependencyId(call, tok, new CallDependency(cs));
+        if (
+          (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) ||
+          (module != currentModule && RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) {
+          // The call statement is inherited, so the refined module already checked that the precondition holds.  Note,
+          // preconditions are not allowed to be strengthened, except if they use a predicate whose body has been strengthened.
+          // But if the callee sits in a different module, then any predicate it uses will be treated as opaque (that is,
+          // uninterpreted) anyway, so the refined module will have checked the call precondition for all possible definitions
+          // of the predicate.
+          call.IsFree = true;
+        }
+        callBuilder.Add(call);
+      }
+
       builder.Add(new CommentCmd("ProcessCallStmt: Make the call"));
-      // Make the call
-      AddReferencedMember(callee);
-      Bpl.CallCmd call = Call(tok, MethodName(callee, kind), ins, outs);
-      proofDependencies?.AddProofDependencyId(call, tok, new CallDependency(cs));
-      if (
-        (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) ||
-        (module != currentModule && RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) {
-        // The call statement is inherited, so the refined module already checked that the precondition holds.  Note,
-        // preconditions are not allowed to be strengthened, except if they use a predicate whose body has been strengthened.
-        // But if the callee sits in a different module, then any predicate it uses will be treated as opaque (that is,
-        // uninterpreted) anyway, so the refined module will have checked the call precondition for all possible definitions
-        // of the predicate.
-        call.IsFree = true;
-      }
-      builder.Add(call);
+      CallCmd post = Call(tok, MethodName(callee, isCoCall ? MethodTranslationKind.CoCallPost : MethodTranslationKind.CallPost), ins, outs);
+      proofDependencies?.AddProofDependencyId(post, tok, new CallDependency(cs));
+      builder.Add(post);
 
       // Unbox results as needed
       for (int i = 0; i < Lhss.Count; i++) {
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs
index f006de8c232..e82c9da14f9 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs
@@ -2856,13 +2856,15 @@ Bpl.Function GetOrCreateFunction(Function f) {
     /// Note that SpecWellformedness and Implementation have procedure implementations
     /// but no callers, and vice versa for InterModuleCall, IntraModuleCall, and CoCall.
     /// </summary>
-    enum MethodTranslationKind { SpecWellformedness, Call, CoCall, Implementation, OverrideCheck }
+    enum MethodTranslationKind { SpecWellformedness, CallPre, CallPost, CoCallPre, CoCallPost, Implementation, OverrideCheck }
 
     private static readonly Dictionary<MethodTranslationKind, string> kindSanitizedPrefix =
       new() {
         { MethodTranslationKind.SpecWellformedness, "CheckWellFormed" },
-        { MethodTranslationKind.Call, "Call" },
-        { MethodTranslationKind.CoCall, "CoCall" },
+        { MethodTranslationKind.CallPre, "CallPre" },
+        { MethodTranslationKind.CallPost, "CallPost" },
+        { MethodTranslationKind.CoCallPre, "CoCallPre" },
+        { MethodTranslationKind.CoCallPost, "CoCallPost" },
         { MethodTranslationKind.Implementation, "Impl" },
         { MethodTranslationKind.OverrideCheck, "OverrideCheck" },
       };
@@ -2875,8 +2877,10 @@ static string MethodName(ICodeContext m, MethodTranslationKind kind) {
     private static readonly Dictionary<MethodTranslationKind, string> kindDescription =
       new Dictionary<MethodTranslationKind, string>() {
         {MethodTranslationKind.SpecWellformedness, "well-formedness"},
-        {MethodTranslationKind.Call, "call"},
-        {MethodTranslationKind.CoCall, "co-call"},
+        {MethodTranslationKind.CallPre, "call precondtion"},
+        {MethodTranslationKind.CallPost, "call postcondition"},
+        {MethodTranslationKind.CoCallPre, "co-call precondtion"},
+        {MethodTranslationKind.CoCallPost, "co-call postcondition"},
         {MethodTranslationKind.Implementation, "correctness"},
         {MethodTranslationKind.OverrideCheck, "override check"},
       };
@@ -4587,7 +4591,7 @@ List<SplitExprInfo> TrSplitExprForMethodSpec(BodyTranslationContext context, Exp
       var splits = new List<SplitExprInfo>();
       var applyInduction = kind == MethodTranslationKind.Implementation;
       bool splitHappened;  // we don't actually care
-      splitHappened = TrSplitExpr(context, expr, splits, true, int.MaxValue, kind != MethodTranslationKind.Call, applyInduction, etran);
+      splitHappened = TrSplitExpr(context, expr, splits, true, int.MaxValue, kind != MethodTranslationKind.CallPost, applyInduction, etran);
       return splits;
     }
 
diff --git a/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs b/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs
index d6844fa3c7b..9513ddb806f 100644
--- a/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs
+++ b/Source/DafnyTestGeneration/Inlining/AddImplementationForCallsRewriter.cs
@@ -15,13 +15,13 @@
 namespace DafnyTestGeneration.Inlining;
 
 /// <summary>
-/// Create implementations for all "Call$$" procedures by making them
+/// Create implementations for all "CallPost$$" procedures by making them
 /// call the respective "Impl$$ implementations. This allows to implement
 /// inlining of Dafny methods further down the road.
 /// </summary>
 public class AddImplementationsForCallsRewriter : ReadOnlyVisitor {
 
-  private const string CallPrefix = "Call$$";
+  private const string CallPrefix = "CallPost$$";
   private readonly DafnyOptions options;
   private List<Implementation> implsToAdd = new();
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy
index d3860e9ea4b..b8ec817b6e6 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy
@@ -1,18 +1,25 @@
-module {:options "--function-syntax:4"} LibraryModule {
+module {:options "--function-syntax:4"} CoolLibraryName {
 
-  function TimesTwo(x: nat): nat
-  {
-    x * 2
-  }
+  // Ensuring this module is not empty,
+  // or else it will be omitted from the translation record.
+  const FOO := 42
+
+  module LibraryModule {
 
-  datatype Result<+T, +E> = Success(value: T) | Failure(error: E)
+    function TimesTwo(x: nat): nat
+    {
+      x * 2
+    }
 
-  // Record type
-  datatype Pair<+T, +U> = Pair(first: T, second: U)
+    datatype Result<+T, +E> = Success(value: T) | Failure(error: E)
 
-  datatype NestedTypeConstructorRecord<+T> = First(value: Pair<T, T>)
-  datatype NestedTypeConstructorClass<+T> = First2(value: Pair<T, T>) | Second2(value: Pair<T, T>)
+    // Record type
+    datatype Pair<+T, +U> = Pair(first: T, second: U)
 
-  datatype NoTypeArgs = Success2 | Failure2
+    datatype NestedTypeConstructorRecord<+T> = First(value: Pair<T, T>)
+    datatype NestedTypeConstructorClass<+T> = First2(value: Pair<T, T>) | Second2(value: Pair<T, T>)
 
+    datatype NoTypeArgs = Success2 | Failure2
+
+  }
 }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/fromDafny42/usesTimesTwo-java/ConsumerModule/__default.java b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/fromDafny42/usesTimesTwo-java/ConsumerModule/__default.java
index 270c8e590ce..592e3a1aa86 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/fromDafny42/usesTimesTwo-java/ConsumerModule/__default.java
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/fromDafny42/usesTimesTwo-java/ConsumerModule/__default.java
@@ -12,7 +12,7 @@ public static void Main(dafny.DafnySequence<? extends dafny.DafnySequence<? exte
     java.math.BigInteger _0_n = java.math.BigInteger.ZERO;
     _0_n = java.math.BigInteger.valueOf(21L);
     java.math.BigInteger _1_TwoN = java.math.BigInteger.ZERO;
-    _1_TwoN = LibraryModule.__default.TimesTwo(_0_n);
+    _1_TwoN = CoolLibraryName_mLibraryModule.__default.TimesTwo(_0_n);
     System.out.print((dafny.DafnySequence.asUnicodeString("Two times ")).verbatimString());
     System.out.print(java.lang.String.valueOf(_0_n));
     System.out.print((dafny.DafnySequence.asUnicodeString(" is ")).verbatimString());
@@ -46,13 +46,13 @@ public static <__T> __T PickSomething(dafny.TypeDescriptor<__T> _td___T)
   }
   public static void MakeAResult()
   {
-    LibraryModule.Result<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _3_r;
-    _3_r = LibraryModule.Result.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create_Success(java.math.BigInteger.valueOf(42L));
+    CoolLibraryName_mLibraryModule.Result<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _3_r;
+    _3_r = CoolLibraryName_mLibraryModule.Result.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create_Success(java.math.BigInteger.valueOf(42L));
   }
   public static void MakeAPair()
   {
-    LibraryModule.Pair<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _4_p;
-    _4_p = LibraryModule.Pair.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create(java.math.BigInteger.ONE, dafny.DafnySequence.asUnicodeString("partridge in a pair tree"));
+    CoolLibraryName_mLibraryModule.Pair<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _4_p;
+    _4_p = CoolLibraryName_mLibraryModule.Pair.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create(java.math.BigInteger.ONE, dafny.DafnySequence.asUnicodeString("partridge in a pair tree"));
   }
   @Override
   public java.lang.String toString() {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo-oldDafnyCompatability.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo-oldDafnyCompatability.dfy
index 4817185edfe..99ef13d97d4 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo-oldDafnyCompatability.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo-oldDafnyCompatability.dfy
@@ -5,7 +5,7 @@
 
 // Java
 
-// RUN: %baredafny translate java --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy --legacy-data-constructors
+// RUN: %baredafny translate java --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy --legacy-data-constructors --legacy-module-names
 // RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java %S/Inputs/producer/timesTwo-java/**/*.java
 
 // Already run using Dafny 4.2: %baredafny translate java --output=%S/fromDafny42/usesTimesTwo --allow-warnings --library=%S/Inputs/producer/timesTwo.dfy %S/usesTimesTwo.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy
index 4cf9208e41d..f5e120978a4 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy
@@ -49,7 +49,7 @@ include "Inputs/producer/timesTwo.dfy"
 
 module ConsumerModule {
 
-  import opened LibraryModule
+  import opened CoolLibraryName.LibraryModule
 
   method Main() {
     var n := 21;
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy
new file mode 100644
index 00000000000..6d83e1da819
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy
@@ -0,0 +1,67 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --standard-libraries
+
+import opened Std.Wrappers
+
+opaque predicate P() { true }
+
+lemma ProveP() ensures P() {
+  reveal P();
+}
+
+method NeedsP()
+  requires P()
+{}
+
+method NeedsPAndReturns3() returns (r: int)
+  requires P()
+  ensures r == 3
+{ r := 3; }
+
+method NeedsPAndReturnsNone() returns (r: Option<int>)
+  requires P()
+{ r := None; }
+
+method A() {
+  NeedsP() by { ProveP(); }
+  assert P(); // Should fail
+}
+
+method B() {
+  var v: int;
+  v := NeedsPAndReturns3() by { reveal P(); }
+  assert P(); // Should fail
+}
+
+method C() {
+  assert p: P() by { ProveP(); }
+  var v := NeedsPAndReturns3() by { reveal p; }
+  assert v == 3;  // should pass
+  assert P(); // should fail
+}
+
+method D() returns (r: Option<int>){
+  var v: int;
+  v :- NeedsPAndReturnsNone() by {
+    match false {
+      case true => assert true;
+      case false => ProveP();
+    }
+  }
+  assert P(); // should fail
+  r := None;
+}
+
+method E() returns (r: Option<int>){
+  var v :- NeedsPAndReturnsNone() by { reveal P(); }
+  assert P(); //  should fail
+  r := None;
+}
+
+greatest predicate G(x: int) { x == 0 || G(x-2) }
+
+greatest lemma F(x: int)
+  ensures G(x)
+{
+  F(x-2) by { ProveP(); }
+  assert P(); // should fail
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect
new file mode 100644
index 00000000000..b4849841fcd
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallBy.dfy.expect
@@ -0,0 +1,8 @@
+CallBy.dfy(26,10): Error: assertion might not hold
+CallBy.dfy(32,10): Error: assertion might not hold
+CallBy.dfy(39,10): Error: assertion might not hold
+CallBy.dfy(50,10): Error: assertion might not hold
+CallBy.dfy(56,10): Error: assertion might not hold
+CallBy.dfy(66,10): Error: assertion might not hold
+
+Dafny program verifier finished with 3 verified, 6 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy
new file mode 100644
index 00000000000..31e5fe5fb51
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy
@@ -0,0 +1,16 @@
+// RUN: ! %verify --type-system-refresh %s > %t
+// RUN: %diff "%s.expect" "%t"
+
+predicate P() { true }
+
+method NeedsP()
+  requires P()
+{}
+
+method M()
+  ensures P()
+{
+  hide P;
+  NeedsP() by { reveal P(); }
+  assert P(); // should fail
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy.expect
new file mode 100644
index 00000000000..ef939499206
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByHide.dfy.expect
@@ -0,0 +1,3 @@
+CallByHide.dfy(15,10): Error: assertion might not hold
+
+Dafny program verifier finished with 0 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy
new file mode 100644
index 00000000000..b41b04b16ea
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy
@@ -0,0 +1,11 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"
+
+method M() {}
+
+method A() {
+  var i: int := 0;
+  M() by {
+    i := 1;
+    return;
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy.expect
new file mode 100644
index 00000000000..d6ed0c40058
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution0.dfy.expect
@@ -0,0 +1,3 @@
+CallByResolution0.dfy(8,6): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression
+CallByResolution0.dfy(9,4): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+2 resolution/type errors detected in CallByResolution0.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy
new file mode 100644
index 00000000000..334dacf2fa7
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy
@@ -0,0 +1,13 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"
+
+method M() {}
+
+method B() {
+  var i := 0;
+  while i < 3 {
+    M() by {
+      break;
+    }
+    i := i + 1;
+  }
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy.expect
new file mode 100644
index 00000000000..66d1c739208
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CallByResolution1.dfy.expect
@@ -0,0 +1,2 @@
+CallByResolution1.dfy(9,6): Error: a non-labeled 'break' statement is allowed only in loops
+1 resolution/type errors detected in CallByResolution1.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect
index e1e675464dc..bc7f9c7e992 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots0.run.legacy.dfy.expect
@@ -1,13 +1,13 @@
-Processing command (at Snapshots0.v0.dfy(4,10)) assert {:id "id1"} Lit(false);
+Processing command (at Snapshots0.v0.dfy(4,10)) assert {:id "id2"} Lit(false);
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors
-Processing call to procedure bar (call) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)):
+Processing call to procedure bar (call precondtion) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)):
+  >>> added after: a##cached##0 := a##cached##0 && true;
+Processing call to procedure bar (call postcondition) in implementation foo (correctness) (at Snapshots0.v1.dfy(3,6)):
   >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall $o: ref :: { $Heap[$o] } $o != null && $Unbox(read(call0old#AT#$Heap, $o, alloc)): bool ==> $Heap[$o] == call0old#AT#$Heap[$o]) && $HeapSucc(call0old#AT#$Heap, $Heap)))
-  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
-Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
-  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id5"} Lit(false);
+  >>> added after: a##cached##1 := a##cached##1 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
+Processing command (at Snapshots0.v1.dfy(4,10)) assert {:id "id7"} Lit(false);
   >>> MarkAsPartiallyVerified
 Snapshots0.v1.dfy(4,9): Error: assertion might not hold
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect
index a2ef2d3d341..6c278ab5388 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots1.run.legacy.dfy.expect
@@ -1,10 +1,10 @@
-Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id1"} Lit(false);
+Processing command (at Snapshots1.v0.dfy(4,10)) assert {:id "id2"} Lit(false);
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors
-Processing call to procedure N (call) in implementation M (correctness) (at Snapshots1.v1.dfy(3,4)):
+Processing call to procedure N (call postcondition) in implementation M (correctness) (at Snapshots1.v1.dfy(3,4)):
   >>> added after: a##cached##0 := a##cached##0 && false;
-Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id6"} Lit(false);
+Processing command (at Snapshots1.v1.dfy(4,10)) assert {:id "id8"} Lit(false);
   >>> DoNothingToAssert
 Snapshots1.v1.dfy(4,9): Error: assertion might not hold
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect
index 768491421f5..401acbc1f66 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots2.run.legacy.dfy.expect
@@ -1,31 +1,31 @@
-Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id1"} Lit(false);
+Processing command (at Snapshots2.v0.dfy(4,10)) assert {:id "id2"} Lit(false);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id5"} Lit(true);
+Processing command (at Snapshots2.v0.dfy(11,11)) assert {:id "id6"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id4"} _module.__default.P() <==> _module.__default.Q();
+Processing command (at Snapshots2.v0.dfy(11,15)) assert {:id "id5"} _module.__default.P() <==> _module.__default.Q();
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id8"} Lit(true);
+Processing command (at Snapshots2.v0.dfy(14,11)) assert {:id "id9"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id7"} _module.__default.Q() <==> Lit(_module.__default.R());
+Processing command (at Snapshots2.v0.dfy(14,15)) assert {:id "id8"} _module.__default.Q() <==> Lit(_module.__default.R());
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 3 verified, 0 errors
-Processing call to procedure N (call) in implementation M (correctness) (at Snapshots2.v1.dfy(3,4)):
+Processing call to procedure N (call postcondition) in implementation M (correctness) (at Snapshots2.v1.dfy(3,4)):
   >>> added after: a##cached##0 := a##cached##0 && false;
 Processing implementation P (well-formedness) (at Snapshots2.v1.dfy(10,11)):
   >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
 Processing implementation Q (well-formedness) (at Snapshots2.v1.dfy(13,11)):
   >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
-Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id12"} Lit(false);
+Processing command (at Snapshots2.v1.dfy(4,10)) assert {:id "id14"} Lit(false);
   >>> DoNothingToAssert
 Snapshots2.v1.dfy(4,9): Error: assertion might not hold
-Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id16"} Lit(true);
+Processing command (at Snapshots2.v1.dfy(11,11)) assert {:id "id18"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id15"} _module.__default.P() <==> _module.__default.Q();
+Processing command (at Snapshots2.v1.dfy(11,15)) assert {:id "id17"} _module.__default.P() <==> _module.__default.Q();
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id19"} Lit(true);
+Processing command (at Snapshots2.v1.dfy(14,11)) assert {:id "id21"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id18"} _module.__default.Q() <==> Lit(_module.__default.R());
+Processing command (at Snapshots2.v1.dfy(14,15)) assert {:id "id20"} _module.__default.Q() <==> Lit(_module.__default.R());
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 2 verified, 1 error
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect
index 5566f116ad4..8a6d82c8b15 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect
@@ -2,11 +2,11 @@ Snapshots5.v0.dfy(10,12): Warning: Could not find a trigger for this quantifier.
 Snapshots5.v0.dfy(13,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 Snapshots5.v0.dfy(20,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 Snapshots5.v0.dfy(26,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
-Processing command (at Snapshots5.v0.dfy(10,40)) assert {:id "id1"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0;
+Processing command (at Snapshots5.v0.dfy(10,40)) assert {:id "id2"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0;
   >>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(13,38)) assert {:id "id3"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3;
+Processing command (at Snapshots5.v0.dfy(13,38)) assert {:id "id5"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3;
   >>> DoNothingToAssert
-Processing command (at Snapshots5.v0.dfy(20,40)) assert {:id "id4"} (forall b#3_1: bool :: b#3_1 || !b#3_1) || 1 != 1;
+Processing command (at Snapshots5.v0.dfy(20,40)) assert {:id "id6"} (forall b#3_1: bool :: b#3_1 || !b#3_1) || 1 != 1;
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors
@@ -15,13 +15,13 @@ Snapshots5.v1.dfy(13,10): Warning: Could not find a trigger for this quantifier.
 Snapshots5.v1.dfy(20,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 Snapshots5.v1.dfy(22,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
 Snapshots5.v1.dfy(27,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
-Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id10"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0;
+Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id13"} (forall b#1_1: bool :: b#1_1 || !b#1_1) || 0 != 0;
   >>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id12"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3;
+Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id16"} (forall b#1: bool :: b#1 || !b#1) || 3 != 3;
   >>> MarkAsFullyVerified
-Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id13"} (exists b#3_1: bool :: Lit(true)) || 4 != 4;
+Processing command (at Snapshots5.v1.dfy(20,37)) assert {:id "id17"} (exists b#3_1: bool :: Lit(true)) || 4 != 4;
   >>> DoNothingToAssert
-Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id14"} (exists b#3: bool :: Lit(true)) || 5 != 5;
+Processing command (at Snapshots5.v1.dfy(22,35)) assert {:id "id18"} (exists b#3: bool :: Lit(true)) || 5 != 5;
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect
index 0b3564e7be2..114c1a89a2e 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots8.run.legacy.dfy.expect
@@ -3,40 +3,40 @@ Processing command (at Snapshots8.v0.dfy(2,37)) assert {:id "id0"} x#0 < 20 || L
   >>> DoNothingToAssert
 Processing command (at Snapshots8.v0.dfy(3,12)) assert {:id "id1"} x#0 < 10;
   >>> DoNothingToAssert
-Processing command (at Snapshots8.v0.dfy(4,8)) assert {:id "id4$id2$requires"} {:id "id2"} LitInt(0) <= call0formal#AT#y#0;
+Processing command (at Snapshots8.v0.dfy(4,8)) assert {:id "id5$id2$requires"} {:id "id2"} LitInt(0) <= call0formal#AT#y#0;
   >>> DoNothingToAssert
 Snapshots8.v0.dfy(3,11): Error: assertion might not hold
 Snapshots8.v0.dfy(4,7): Error: a precondition for this call could not be proved
 Snapshots8.v0.dfy(8,13): Related location: this is the precondition that could not be proved
-Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id8"} LitInt(2) <= z#0;
+Processing command (at Snapshots8.v0.dfy(13,13)) assert {:id "id9"} LitInt(2) <= z#0;
   >>> DoNothingToAssert
 Snapshots8.v0.dfy(17,9): Error: a postcondition could not be proved on this return path
 Snapshots8.v0.dfy(13,12): Related location: this is the postcondition that could not be proved
-Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id10"} u#0 != 53;
+Processing command (at Snapshots8.v0.dfy(23,12)) assert {:id "id11"} u#0 != 53;
   >>> DoNothingToAssert
 Snapshots8.v0.dfy(23,11): Error: assertion might not hold
-Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id11"} Lit(true);
+Processing command (at Snapshots8.v0.dfy(28,10)) assert {:id "id12"} Lit(true);
   >>> DoNothingToAssert
 
 Dafny program verifier finished with 1 verified, 4 errors
-Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id24"} u#0 != 53;
+Processing command (at Snapshots8.v1.dfy(30,17)) assert {:id "id26"} u#0 != 53;
   >>> RecycleError
 Snapshots8.v1.dfy(30,16): Error: assertion might not hold
-Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id12"} x#0 < 20 || LitInt(10) <= x#0;
+Processing command (at Snapshots8.v1.dfy(3,15)) assert {:id "id13"} x#0 < 20 || LitInt(10) <= x#0;
   >>> MarkAsFullyVerified
-Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id13"} x#0 < 10;
+Processing command (at Snapshots8.v1.dfy(5,17)) assert {:id "id14"} x#0 < 10;
   >>> RecycleError
-Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id17$id14$requires"} {:id "id14"} LitInt(0) <= call0formal#AT#y#0;
+Processing command (at Snapshots8.v1.dfy(6,8)) assert {:id "id19$id15$requires"} {:id "id15"} LitInt(0) <= call0formal#AT#y#0;
   >>> RecycleError
-Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id15"} x#0 == LitInt(7);
+Processing command (at Snapshots8.v1.dfy(7,12)) assert {:id "id17"} x#0 == LitInt(7);
   >>> DoNothingToAssert
 Snapshots8.v1.dfy(5,16): Error: assertion might not hold
 Snapshots8.v1.dfy(6,7): Error: a precondition for this call could not be proved
 Snapshots8.v1.dfy(12,20): Related location: this is the precondition that could not be proved
 Snapshots8.v1.dfy(7,11): Error: assertion might not hold
-Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id23"} Lit(true);
+Processing command (at Snapshots8.v1.dfy(23,12)) assert {:id "id25"} Lit(true);
   >>> DoNothingToAssert
-Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id21"} LitInt(2) <= z#0;
+Processing command (at Snapshots8.v1.dfy(19,13)) assert {:id "id23"} LitInt(2) <= z#0;
   >>> DoNothingToAssert
 Snapshots8.v1.dfy(24,9): Error: a postcondition could not be proved on this return path
 Snapshots8.v1.dfy(19,12): Related location: this is the postcondition that could not be proved
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy
index 9c23169829f..d1bc619d003 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy
@@ -467,8 +467,6 @@ assert heapExternalsZeroOrOneEdges(xedges);
       o.fields := o.fields[f := t];   ///who designed this fucking syntax?
 
       assert ObjectsAreValid({o});
-
-      assert edges(objects) == old( edges(objects) ) + {Edge(o,f,t)};
           
       var zedges := edges(objects);  //or could hand in if necessary?
       var zisos := justTheIsos(objects);
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
index efc7dd6b97d..1ba70097ea1 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
@@ -1,10 +1,10 @@
-git-issue-3855.dfy(801,0): Warning: attribute :ignore is deprecated
-git-issue-3855.dfy(801,11): Error: Verification of 'Memory.dynMove' timed out after <redacted> seconds
-git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved
+git-issue-3855.dfy(799,0): Warning: attribute :ignore is deprecated
+git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after <redacted> seconds
+git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved
 git-issue-3855.dfy(430,29): Related location: this is the precondition that could not be proved
-git-issue-3855.dfy(944,17): Error: a precondition for this call could not be proved
+git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved
 git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved
-git-issue-3855.dfy(1337,20): Error: a precondition for this call could not be proved
+git-issue-3855.dfy(1335,20): Error: a precondition for this call could not be proved
 git-issue-3855.dfy(434,36): Related location: this is the precondition that could not be proved
 
 Dafny program verifier finished with 101 verified, 3 errors, 1 time out
diff --git a/docs/DafnyRef/Statements.16.expect b/docs/DafnyRef/Statements.16.expect
new file mode 100644
index 00000000000..6bbd3b36f5b
--- /dev/null
+++ b/docs/DafnyRef/Statements.16.expect
@@ -0,0 +1,3 @@
+text.dfy(17,10): Error: assertion might not hold
+
+Dafny program verifier finished with 2 verified, 1 error
diff --git a/docs/DafnyRef/Statements.md b/docs/DafnyRef/Statements.md
index ef2fc664708..f85787e2e22 100644
--- a/docs/DafnyRef/Statements.md
+++ b/docs/DafnyRef/Statements.md
@@ -257,6 +257,38 @@ Note that the syntax
 
 is interpreted as a label in which the user forgot the `label` keyword.
 
+### 8.5.6. Method call with a `by` proof
+
+The purpose of this form of a method call is to seperate the called method's
+precondition and its proof from the rest of the correctness proof of the
+calling method.
+
+<!-- %check-verify Statements.16.expect -->
+```dafny
+opaque predicate P() { true }
+
+lemma ProveP() ensures P() {
+  reveal P();
+}
+
+method M(i: int) returns (r: int)
+  requires P()
+  ensures r == i
+{ r := i; }
+
+method C() {
+  var v := M(1/3) by { // We prove 3 != 0 outside of the by proof
+    ProveP();          // Prove precondtion  
+  }
+  assert v == 0;       // Use postcondition
+  assert P();          // Fails
+}
+```
+
+By placing the call to lemma `ProveP` inside of the by block, we can not use
+`P` after the method call. The well-formedness checks of the arguments to the
+method call are not subject to the separation.
+
 ## 8.6. Update with Failure Statement (`:-`) ([grammar](#g-update-with-failure-statement)) {#sec-update-with-failure-statement}
 
 See the subsections below for examples.
diff --git a/docs/dev/news/5662.feat b/docs/dev/news/5662.feat
new file mode 100644
index 00000000000..15c238b1d5e
--- /dev/null
+++ b/docs/dev/news/5662.feat
@@ -0,0 +1 @@
+Method calls get an optional by-proof that hides the precondtion and its proof