diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 807f198787..c90b380096 100644
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -1775,6 +1775,11 @@ func (ft *factsTable) flowLimit(v *Value) bool {
 		a := ft.limits[v.Args[0].ID]
 		b := ft.limits[v.Args[1].ID]
 		return ft.newLimit(v, a.mul(b.exp2(8), 8))
+	case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
+		a := ft.limits[v.Args[0].ID]
+		b := ft.limits[v.Args[1].ID]
+		// Underflow in the arithmetic below is ok, it gives to MaxUint64 which does nothing to the limit.
+		return ft.unsignedMax(v, minU(a.umax, b.umax-1))
 
 	case OpPhi:
 		// Compute the union of all the input phis.
@@ -1909,6 +1914,8 @@ func addLocalFacts(ft *factsTable, b *Block) {
 
 	// Add facts about individual operations.
 	for _, v := range b.Values {
+		// FIXME(go.dev/issue/68857): this loop only set up limits properly when b.Values is in topological order.
+		// flowLimit can also depend on limits given by this loop which right now is not handled.
 		switch v.Op {
 		case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
 			ft.update(b, v, v.Args[0], unsigned, lt|eq)
diff --git a/test/prove.go b/test/prove.go
index 8e65404431..a1aa67d472 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -1426,6 +1426,58 @@ func or64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
 	return int(z)
 }
 
+func mod64uWithSmallerDividendMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
+	a &= 0xff
+	b &= 0xfff
+
+	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
+
+	if ensureBothBranchesCouldHappen {
+		if z > bits.Len64(0xff) { // ERROR "Disproved Less64$"
+			return 42
+		}
+	} else {
+		if z <= bits.Len64(0xff) { // ERROR "Proved Leq64$"
+			return 1337
+		}
+	}
+	return z
+}
+func mod64uWithSmallerDivisorMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
+	a &= 0xfff
+	b &= 0x10 // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
+
+	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
+
+	if ensureBothBranchesCouldHappen {
+		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
+			return 42
+		}
+	} else {
+		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
+			return 1337
+		}
+	}
+	return z
+}
+func mod64uWithIdenticalMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
+	a &= 0x10
+	b &= 0x10 // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
+
+	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
+
+	if ensureBothBranchesCouldHappen {
+		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
+			return 42
+		}
+	} else {
+		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
+			return 1337
+		}
+	}
+	return z
+}
+
 //go:noinline
 func useInt(a int) {
 }