diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
index 68315907a..86d9dd62b 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
@@ -925,7 +925,7 @@ module MessageBody {
       + UInt64ToSeq(length)
   }
 
-  function method WriteFramedMessageBody(
+  opaque function method WriteFramedMessageBody(
     body: FramedMessage
   )
     :(ret: seq<uint8>)
@@ -933,27 +933,37 @@ module MessageBody {
     //= type=implication
     //# The final frame
     //# MUST be the last frame.
-    ensures ret == WriteMessageRegularFrames(body.regularFrames)
-      + Frames.WriteFinalFrame(body.finalFrame)
+    //ensures ret == WriteMessageRegularFrames(body.regularFrames)
+    //  + Frames.WriteFinalFrame(body.finalFrame)
   {
     WriteMessageRegularFrames(body.regularFrames) + Frames.WriteFinalFrame(body.finalFrame)
   }
+  lemma AboutWriteFramedMessageBody(body: FramedMessage)
+    ensures WriteFramedMessageBody(body) == WriteMessageRegularFrames(body.regularFrames) + Frames.WriteFinalFrame(body.finalFrame)
+  {
+    reveal WriteFramedMessageBody();
+  }
 
-  function method WriteMessageRegularFrames(
+  opaque function method WriteMessageRegularFrames(
     frames: MessageRegularFrames
   )
     :(ret: seq<uint8>)
-    ensures if |frames| == 0 then
-      ret == []
-    else
-      ret == WriteMessageRegularFrames(Seq.DropLast(frames))
-      + Frames.WriteRegularFrame(Seq.Last(frames))
   {
     if |frames| == 0 then []
     else
       WriteMessageRegularFrames(Seq.DropLast(frames))
       + Frames.WriteRegularFrame(Seq.Last(frames))
   }
+  // Unroll the function at most once
+  lemma AboutWriteMessageRegularFrames(frames: MessageRegularFrames)
+    ensures WriteMessageRegularFrames(frames) ==
+      if |frames| == 0 then []
+    else
+      WriteMessageRegularFrames(Seq.DropLast(frames))
+      + Frames.WriteRegularFrame(Seq.Last(frames))
+  {
+    reveal WriteMessageRegularFrames();
+  }
 
   function method {:recursive} {:vcs_split_on_every_assert} ReadFramedMessageBody(
     buffer: ReadableBuffer,
@@ -1034,22 +1044,29 @@ module MessageBody {
       var res := Success(SuccessfulRead(nextRegularFrames, regularFrame.tail));
       assert CorrectlyRead(buffer, res, WriteMessageRegularFrames) by {
         reveal CorrectlyReadRange();
-
-        var tail := res.value.tail;
-        var readRange := WriteMessageRegularFrames(res.value.data);
-        assert buffer.bytes == tail.bytes;
-        assert buffer.start <= tail.start <= |buffer.bytes|;
-        assert buffer.bytes[buffer.start..] == tail.bytes[buffer.start..];
-        assert readRange <= buffer.bytes[buffer.start..];
-        assert tail.start == buffer.start + |readRange|;
+        var tail := regularFrame.tail;
+        var f := WriteMessageRegularFrames;
+        var readRange := WriteMessageRegularFrames(nextRegularFrames);
+        assert readRange == f(nextRegularFrames);
+        AboutWriteMessageRegularFrames(nextRegularFrames);
+        assert && buffer.bytes == tail.bytes
+              && buffer.start <= tail.start <= |buffer.bytes|
+              && buffer.bytes[buffer.start..] == tail.bytes[buffer.start..]
+              && readRange <= buffer.bytes[buffer.start..]
+              && tail.start == buffer.start + |readRange|;
+        // Trivial evidence above but helps reduce brittleness by reducing the assertion below from 1.65MRU
+        // down to 550kRU
+        assert CorrectlyReadRange(buffer, regularFrame.tail, WriteMessageRegularFrames(nextRegularFrames));
       }
-
-      ReadFramedMessageBody(
+      assert CorrectlyReadRange(buffer, regularFrame.tail, buffer.bytes[buffer.start..regularFrame.tail.start]);
+      var res := ReadFramedMessageBody(
         buffer,
         header,
         nextRegularFrames,
         regularFrame.tail
-      )
+      );
+      assert CorrectlyRead(buffer, res, WriteFramedMessageBody);
+      res
     else
       //= compliance/client-apis/decrypt.txt#2.7.4
       //# If the first 4 bytes
@@ -1078,7 +1095,14 @@ module MessageBody {
       assert {:split_here} true;
       assert CorrectlyRead(continuation, Success(finalFrame), Frames.WriteFinalFrame);
       assert {:split_here} true;
-      Success(SuccessfulRead(body, finalFrame.tail))
+      var res := Success(SuccessfulRead(body, finalFrame.tail));
+      assert CorrectlyRead(buffer, res, WriteFramedMessageBody) by {
+        reveal CorrectlyReadRange();
+        AboutWriteFramedMessageBody(body);
+        assert CorrectlyReadRange(buffer, res.value.tail, WriteFramedMessageBody(res.value.data));
+        assert CorrectlyReadRange(buffer, finalFrame.tail, WriteFramedMessageBody(body));
+      }
+      res
   }
 
   function WriteNonFramedMessageBody(
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/Frames.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/Frames.dfy
index 91940cab3..d5b57d431 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/Frames.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Serialize/Frames.dfy
@@ -137,7 +137,7 @@ module Frames {
 
   const SAFE_MAX_ENCRYPT := 0xFFFFFFFE0 // 2^36 - 32
 
-  function method WriteRegularFrame(
+  opaque function method WriteRegularFrame(
     regularFrame: RegularFrame
   )
     :(ret: seq<uint8>)
@@ -191,6 +191,7 @@ module Frames {
 
     assert CorrectlyReadRange(buffer, authTag.tail, WriteRegularFrame(regularFrame)) by {
       CorrectlyReadByteRange(buffer, sequenceNumber.tail, WriteUint32(sequenceNumber.data));
+      reveal WriteRegularFrame();
       AppendToCorrectlyReadByteRange(buffer, sequenceNumber.tail, iv.tail, Write(iv.data));
       AppendToCorrectlyReadByteRange(buffer, iv.tail, encContent.tail, Write(encContent.data));
       AppendToCorrectlyReadByteRange(buffer, encContent.tail, authTag.tail, Write(authTag.data));
@@ -198,7 +199,7 @@ module Frames {
     Success(SuccessfulRead(regularFrame, authTag.tail))
   }
 
-  function method WriteFinalFrame(
+  opaque function method WriteFinalFrame(
     finalFrame: FinalFrame
   )
     :(ret: seq<uint8>)
@@ -276,6 +277,7 @@ module Frames {
 
     assert CorrectlyReadRange(buffer, authTag.tail, WriteFinalFrame(finalFrame)) by {
       reveal CorrectlyReadRange();
+      reveal WriteFinalFrame();
       // It seems that Dafny can find a solution pretty fast.
       // But I leave this here in case there is some problem later.
       // CorrectlyReadByteRange(buffer, finalFrameSignal.tail, WriteUint32(finalFrameSignal.data));