diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.expected
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql
new file mode 100644
index 00000000000..946930f29d1
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/AllLiveReachable.ql
@@ -0,0 +1,17 @@
+/**
+ * Checks that every live (non-dead) annotation in the test function's
+ * own scope is reachable from the function entry in the CFG.
+ * Annotations in nested scopes (generators, async, lambdas, comprehensions)
+ * have separate CFGs and are excluded from this check.
+ */
+
+import python
+import TimerUtils
+
+from TimerCfgNode a, TestFunction f
+where
+  not a.isDead() and
+  f = a.getTestFunction() and
+  a.getScope() = f and
+  not f.getEntryNode().getBasicBlock().reaches(a.getBasicBlock())
+select a, "Unreachable live annotation; entry of $@ does not reach this node", f, f.getName()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.expected
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql
new file mode 100644
index 00000000000..8f84e206218
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/BasicBlockAnnotationGap.ql
@@ -0,0 +1,26 @@
+/**
+ * Checks that within a basic block, if a node is annotated then its
+ * successor is also annotated (or excluded). A gap in annotations
+ * within a basic block indicates a missing annotation, since there
+ * are no branches to justify the gap.
+ *
+ * Nodes with exceptional successors are excluded, as the exception
+ * edge leaves the basic block and the normal successor may be dead.
+ */
+
+import python
+import TimerUtils
+
+from TimerCfgNode a, ControlFlowNode succ
+where
+  exists(BasicBlock bb, int i |
+    a = bb.getNode(i) and
+    succ = bb.getNode(i + 1)
+  ) and
+  not succ instanceof TimerCfgNode and
+  not isUnannotatable(succ.getNode()) and
+  not isTimerMechanism(succ.getNode(), a.getTestFunction()) and
+  not exists(a.getAnExceptionalSuccessor()) and
+  succ.getNode() instanceof Expr
+select a, "Annotated node followed by unannotated $@ in the same basic block", succ,
+  succ.getNode().toString()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.expected
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql
new file mode 100644
index 00000000000..456ebf447da
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/ContiguousTimestamps.ql
@@ -0,0 +1,18 @@
+/**
+ * Checks that timestamps form a contiguous sequence {0, 1, ..., max}
+ * within each test function. Every integer in the range must appear
+ * in at least one annotation (live or dead).
+ */
+
+import python
+import TimerUtils
+
+from TestFunction f, int missing, int maxTs, TimerAnnotation maxAnn
+where
+  maxTs = max(TimerAnnotation a | a.getTestFunction() = f | a.getATimestamp()) and
+  maxAnn.getTestFunction() = f and
+  maxAnn.getATimestamp() = maxTs and
+  missing = [0 .. maxTs] and
+  not exists(TimerAnnotation a | a.getTestFunction() = f and a.getATimestamp() = missing)
+select f, "Missing timestamp " + missing + " (max is $@)", maxAnn.getTimestampExpr(maxTs),
+  maxTs.toString()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.expected
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql
new file mode 100644
index 00000000000..64f0c3ba186
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoBackwardFlow.ql
@@ -0,0 +1,19 @@
+/**
+ * Checks that time never flows backward between consecutive timer annotations
+ * in the CFG. For each pair of consecutive annotated nodes (A -> B), there must
+ * exist timestamps a in A and b in B with a < b.
+ */
+
+import python
+import TimerUtils
+
+from TimerCfgNode a, TimerCfgNode b, int minA, int maxB
+where
+  nextTimerAnnotation(a, b) and
+  not a.isDead() and
+  not b.isDead() and
+  minA = min(a.getATimestamp()) and
+  maxB = max(b.getATimestamp()) and
+  minA >= maxB
+select a, "Backward flow: $@ flows to $@ (max timestamp $@)", a.getTimestampExpr(minA),
+  minA.toString(), b, b.getNode().toString(), b.getTimestampExpr(maxB), maxB.toString()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.expected
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql
new file mode 100644
index 00000000000..59b68020638
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/NoSharedReachable.ql
@@ -0,0 +1,23 @@
+/**
+ * Checks that two annotations sharing a timestamp value are on
+ * mutually exclusive CFG paths (neither can reach the other).
+ */
+
+import python
+import TimerUtils
+
+from TimerCfgNode a, TimerCfgNode b, int ts
+where
+  a != b and
+  not a.isDead() and
+  not b.isDead() and
+  a.getTestFunction() = b.getTestFunction() and
+  ts = a.getATimestamp() and
+  ts = b.getATimestamp() and
+  (
+    a.getBasicBlock().strictlyReaches(b.getBasicBlock())
+    or
+    exists(BasicBlock bb, int i, int j | a = bb.getNode(i) and b = bb.getNode(j) and i < j)
+  )
+select a, "Shared timestamp $@ but this node reaches $@", a.getTimestampExpr(ts), ts.toString(), b,
+  b.getNode().toString()
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.expected b/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.expected
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql b/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql
new file mode 100644
index 00000000000..8147062664f
--- /dev/null
+++ b/python/ql/test/library-tests/ControlFlow/evaluation-order/StrictForward.ql
@@ -0,0 +1,25 @@
+/**
+ * Stronger version of NoBackwardFlow: for consecutive annotated nodes
+ * A -> B that both have a single timestamp (non-loop code) and B does
+ * NOT dominate A (forward edge), requires max(A) < min(B).
+ */
+
+import python
+import TimerUtils
+
+from TimerCfgNode a, TimerCfgNode b, int maxA, int minB
+where
+  nextTimerAnnotation(a, b) and
+  not a.isDead() and
+  not b.isDead() and
+  // Only apply to non-loop code (single timestamps on both sides)
+  strictcount(a.getATimestamp()) = 1 and
+  strictcount(b.getATimestamp()) = 1 and
+  // Forward edge: B does not strictly dominate A (excludes loop back-edges
+  // but still checks same-basic-block pairs)
+  not b.getBasicBlock().strictlyDominates(a.getBasicBlock()) and
+  maxA = max(a.getATimestamp()) and
+  minB = min(b.getATimestamp()) and
+  maxA >= minB
+select a, "Strict forward violation: $@ flows to $@", a.getTimestampExpr(maxA), "timestamp " + maxA,
+  b.getTimestampExpr(minB), "timestamp " + minB