diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
index 1815fce4d36..25ee5592cfc 100644
--- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
+++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
@@ -596,7 +596,7 @@ public ModuleSignature RegisterTopLevelDecls(Resolver resolver, bool useImports)
         Contract.Assert(preMemberErrs != resolver.reporter.Count(ErrorLevel.Error) || !defaultClassDecl.Members.Except(members.Values).Any());
 
         foreach (MemberDecl m in members.Values) {
-          Contract.Assert(!m.HasStaticKeyword);
+          Contract.Assert(!m.HasStaticKeyword || Attributes.Contains(m.Attributes, "opaque_reveal"));
           if (m is Function or Method or ConstantField) {
             sig.StaticMembers[m.Name] = m;
           }
diff --git a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs
index cbb67150d15..90f26714bf9 100644
--- a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs
+++ b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs
@@ -82,6 +82,8 @@ protected void ProcessOpaqueClassMembers(TopLevelDeclWithMembers c) {
     foreach (var member in c.Members.Where(member => member is Function or ConstantField)) {
       if (!Attributes.Contains(member.Attributes, "opaque") && !member.IsOpaque) {
         // Nothing to do
+      } else if (member is Function { Body: null }) {
+        // Nothing to do
       } else if (!RefinementToken.IsInherited(member.tok, c.EnclosingModuleDefinition)) {
         GenerateRevealLemma(member, newDecls);
       }
@@ -135,16 +137,19 @@ private void GenerateRevealLemma(MemberDecl m, List<MemberDecl> newDecls) {
     lemma_attrs = new Attributes("opaque_reveal", new List<Expression>(), lemma_attrs);
     lemma_attrs = new Attributes("verify", new List<Expression>() { new LiteralExpr(m.tok, false) }, lemma_attrs);
     var ens = new List<AttributedExpression>();
-    if (m is ConstantField c && c.Rhs != null) {
+
+    var isStatic = true;
+    if (m is ConstantField { Rhs: not null } c) {
       ens.Add(new AttributedExpression(new BinaryExpr(c.tok, BinaryExpr.Opcode.Eq, new NameSegment(c.Tok, c.Name, null), c.Rhs)));
+      isStatic = m.HasStaticKeyword;
     }
     Method reveal;
     if (m is TwoStateFunction) {
-      reveal = new TwoStateLemma(m.RangeToken, m.NameNode.Prepend("reveal_"), m.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
+      reveal = new TwoStateLemma(m.RangeToken, m.NameNode.Prepend("reveal_"), isStatic, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
         new Specification<FrameExpression>(new List<FrameExpression>(), null), ens,
         new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, null);
     } else {
-      reveal = new Lemma(m.RangeToken, m.NameNode.Prepend("reveal_"), m.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
+      reveal = new Lemma(m.RangeToken, m.NameNode.Prepend("reveal_"), isStatic, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
         new Specification<FrameExpression>(new List<FrameExpression>(), null), ens,
         new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, null);
     }
diff --git a/Test/git-issues/git-issue-4176.dfy b/Test/git-issues/git-issue-4176.dfy
new file mode 100644
index 00000000000..2e56dbf61fd
--- /dev/null
+++ b/Test/git-issues/git-issue-4176.dfy
@@ -0,0 +1,19 @@
+// RUN: %baredafny verify %args %s > %t
+// RUN: %diff "%s.expect" "%t"
+
+method test(c: Class) {
+    reveal Class.P();
+    reveal Class.Q();
+    reveal f();
+    
+    assert c.P();
+    assert c.Q();
+    assert f();
+}
+
+class Class {
+  opaque function P() : bool { true }
+  opaque twostate function Q() : bool { true }
+}
+
+opaque function f() : bool { true }
\ No newline at end of file
diff --git a/Test/git-issues/git-issue-4176.dfy.expect b/Test/git-issues/git-issue-4176.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Test/git-issues/git-issue-4176.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/docs/dev/4176.fix b/docs/dev/4176.fix
new file mode 100644
index 00000000000..a833fe503fe
--- /dev/null
+++ b/docs/dev/4176.fix
@@ -0,0 +1 @@
+Revealing opaque instance functions can now be done statically
\ No newline at end of file
diff --git a/docs/dev/reveal-opaque-instance-functions.feat b/docs/dev/reveal-opaque-instance-functions.feat
new file mode 100644
index 00000000000..27a13f44397
--- /dev/null
+++ b/docs/dev/reveal-opaque-instance-functions.feat
@@ -0,0 +1 @@
+It is now possible to reveal an instance function of a class by a static reveal, without the need of an object of that class.
\ No newline at end of file