diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
index a80d1008d..cf0796cd7 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
@@ -14,6 +14,8 @@
 
 package dev.cel.verifier;
 
+import static com.google.common.base.Preconditions.checkArgument;
+
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.ImmutableSortedSet;
@@ -111,8 +113,8 @@ Set<Expr<?>> getInputVariables() {
    * Binds an identifier name in the symbol table to an already-translated value. Used to bind
    * reserved policy symbols such as 'rule.result' to the composed policy graph.
    */
-  void bindSymbol(String varName, TranslatedValue value) {
-    context.bindSymbol(varName, value);
+  void bindSymbol(String varName, TranslatedValue value, CelAbstractSyntaxTree ast) {
+    context.bindSymbol(varName, value, ast);
   }
 
   TranslatedValue translate(CelAbstractSyntaxTree ast) {
@@ -439,6 +441,15 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
     long exprId = expr.id();
     String functionName = call.function();
     ImmutableList<CelExpr> argsAst = call.args();
+    if (functionName.equals(Operator.OPTIONAL_SELECT.getFunction())) {
+      checkArgument(
+          !call.target().isPresent()
+              && argsAst.size() == 2
+              && argsAst.get(1).constantOrDefault().getKind() == CelConstant.Kind.STRING_VALUE,
+          "Malformed AST: operator %s expects an operand and a field name",
+          Operator.OPTIONAL_SELECT);
+      return structTranslator.translateSelect(expr, ast);
+    }
 
     List<TranslatedValue> args = new ArrayList<>();
 
@@ -453,42 +464,41 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
 
     return operatorTranslator
         .translateFunctionCall(functionName, args, exprId, ast)
-        .map(
-            tv -> {
-              if (mayEmbedArgs(functionName, ast.getTypeOrThrow(exprId))) {
-                propagateTruncatedTypeConstraint(
-                    tv.z3Expr(), Iterables.transform(args, TranslatedValue::z3Expr));
-              }
-              return TranslatedValue.create(tv.z3Expr(), expr, typeSystem, tv.isApproximate());
-            })
-        .orElseGet(
-            () -> {
-              // Uninterpreted function
-              Sort[] argSorts = new Sort[args.size()];
-              Arrays.fill(argSorts, 0, args.size(), typeSystem.celValueSort());
-              FuncDecl<?> funcDecl =
-                  typeSystem.internFuncDecl(
-                      uninterpretedFunctionSymbol(exprId, ast),
-                      argSorts,
-                      typeSystem.celValueSort());
-
-              Expr<?>[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new);
-              Expr<?> callRes = ctx.mkApp(funcDecl, exprArgs);
-              context.addConstraint(
-                  typeConstraintGenerator.createTypeConstraint(callRes, exprId, ast));
-              context.addConstraint(ctx.mkNot(typeSystem.isUnknown(callRes)));
-              context.addConstraint(ctx.mkNot(typeSystem.isError(callRes)));
-
-              // The solver picks the result freely, so a model depending on it is never exact.
-              return TranslatedValue.propagateStrict(
-                  ctx,
-                  typeSystem,
-                  functionName,
-                  callRes,
-                  Optional.of(expr),
-                  /* baseTaint= */ context.recordCallApproximation(functionName, ctx.mkTrue()),
-                  args);
-            });
+        .map(tv -> {
+          if (mayEmbedArgs(functionName, ast.getTypeOrThrow(exprId))) {
+            propagateTruncatedTypeConstraint(
+                tv.z3Expr(), Iterables.transform(args, TranslatedValue::z3Expr));
+          }
+          return TranslatedValue.create(tv.z3Expr(), expr, typeSystem, tv.isApproximate());
+        })
+        .orElseGet(() -> {
+          // Uninterpreted function
+          Sort[] argSorts = new Sort[args.size()];
+          Arrays.fill(argSorts, 0, args.size(), typeSystem.celValueSort());
+          FuncDecl<?> funcDecl =
+              typeSystem.internFuncDecl(
+                  uninterpretedFunctionSymbol(exprId, ast), argSorts, typeSystem.celValueSort());
+
+          Expr<?>[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new);
+          Expr<?> callRes = ctx.mkApp(funcDecl, exprArgs);
+          // A narrowed result's static type doesn't constrain it.
+          if (!context.mayBeNarrowed(expr, ast)) {
+            context.addConstraint(
+                typeConstraintGenerator.createTypeConstraint(callRes, exprId, ast));
+          }
+          context.addConstraint(ctx.mkNot(typeSystem.isUnknown(callRes)));
+          context.addConstraint(ctx.mkNot(typeSystem.isError(callRes)));
+
+          // The solver picks the result freely, so a model depending on it is never exact.
+          return TranslatedValue.propagateStrict(
+              ctx,
+              typeSystem,
+              functionName,
+              callRes,
+              Optional.of(expr),
+              /* baseTaint= */ context.recordCallApproximation(functionName, ctx.mkTrue()),
+              args);
+        });
   }
 
   /**
diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
index 900821e92..24c748287 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
@@ -267,7 +267,7 @@ CelVerificationResult verifyImplication(
 
       for (Map.Entry<String, CelAbstractSyntaxTree> entry : boundSymbols.entrySet()) {
         TranslatedValue tv = translator.translate(entry.getValue());
-        translator.bindSymbol(entry.getKey(), tv);
+        translator.bindSymbol(entry.getKey(), tv, entry.getValue());
       }
 
       TranslatedValue assumeTv = translator.translate(assumeAst);
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
index 379fba20a..27016ac8d 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
@@ -187,13 +187,32 @@ private TranslatedValue translateDynamicComprehension(
             ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit))));
     context.addUnmodeledResult(isTruncated);
 
-    if (isAllMacro(comp) || isExistsMacro(comp)) {
-      return unrollAllAndExists(
-          celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
-    } else {
-      return unrollMapAndFilter(
-          celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
+    TranslatedValue result =
+        isAllMacro(comp) || isExistsMacro(comp)
+            ? unrollAllAndExists(
+                celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv)
+            : unrollMapAndFilter(
+                celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
+    // Only for speed: a range that isn't narrowed always has its static kind.
+    if (!context.mayBeNarrowed(comp.iterRange(), ast)) {
+      return result;
     }
+    // The type checker may have narrowed the range's type (e.g. `dyn_var.orValue([1])` is typed
+    // list(int)), so it may be the other kind, or not a list or map at all.
+    BoolExpr isListOrMap = ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange));
+    BoolExpr isOtherKind =
+        context.recordApproximation(
+            "comprehensions over `dyn` values", ctx.mkAnd(ctx.mkNot(isValidRange), isListOrMap));
+    context.addUnmodeledResult(isOtherKind);
+    BoolExpr isNotRange = ctx.mkNot(ctx.mkOr(isListOrMap, typeSystem.isErrorOrUnknown(iterRange)));
+    return TranslatedValue.create(
+        CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
+            .addCase(isOtherKind, mkParameterizedUnknown(celExpr, ast))
+            .addCase(isNotRange, typeSystem.mkError())
+            .build(result.z3Expr()),
+        celExpr,
+        typeSystem,
+        CelZ3Exprs.mkOrFlattened(ctx, result.isApproximate(), isOtherKind));
   }
 
   private <T> T withIterationScope(
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
index e48f1d33b..caa1c8335 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
@@ -177,15 +177,6 @@ Optional<TranslatedValue> translateFunctionCall(
             CelZ3Exprs.mkOrFlattened(
                 ctx, currentApprox, ctx.mkAnd(isList, CelZ3Exprs.mkOrFlattened(ctx, taints)));
       }
-    } else if (op == Operator.OPTIONAL_SELECT) {
-      // A chained optional select (e.g. `a.?b.?c`) selects from the value of an optional operand.
-      Expr<?> operand = z3Args.get(0);
-      Expr<?> target =
-          ctx.mkITE(
-              typeSystem.isOptional(operand),
-              typeSystem.getOptionalValue(typeSystem.getOptionalRef(operand)),
-              operand);
-      currentApprox = CelZ3Exprs.mkOrFlattened(ctx, currentApprox, context.isTruncatedMap(target));
     }
 
     return Optional.of(
@@ -335,9 +326,11 @@ private TranslatedValue translateOperatorCall(
       case LOGICAL_OR:
         return translateLogicalAndOr(args, false);
       case LOGICAL_NOT:
-        return translateLogicalNot(args, ast);
+        return translateLogicalNot(args);
       case NEGATE:
-        return translateNegate(args.get(0), ast);
+        // NegateAxiom handles the overloads the type checker picked; other kinds error.
+        return TranslatedValue.propagateStrict(
+            ctx, typeSystem, op.getFunction(), typeSystem.mkError(), args);
       case EQUALS:
         return translateEquality(
             args.get(0), args.get(1), ast, /* isEquals= */ true, /* shallow= */ false);
@@ -359,11 +352,11 @@ private TranslatedValue translateOperatorCall(
         return TranslatedValue.propagateStrict(
             ctx, typeSystem, op.getFunction(), typeSystem.mkError(), args);
       case INDEX:
-        return translateIndex(args, ast, false);
+        return translateIndex(args, ast, /* isOptional= */ false);
       case OPTIONAL_INDEX:
-        return translateIndex(args, ast, true);
+        return translateIndex(args, ast, /* isOptional= */ true);
       case CONDITIONAL:
-        return translateConditional(args, ast);
+        return translateConditional(args);
       case NOT_STRICTLY_FALSE:
       case OLD_NOT_STRICTLY_FALSE:
         return translateNotStrictlyFalse(args);
@@ -432,48 +425,17 @@ private TranslatedValue translateBinaryLogicalAndOr(
     return TranslatedValue.create(resultZ3, typeSystem, resultTaint);
   }
 
-  private TranslatedValue translateLogicalNot(
-      List<TranslatedValue> args, CelAbstractSyntaxTree ast) {
+  private TranslatedValue translateLogicalNot(List<TranslatedValue> args) {
     TranslatedValue arg = args.get(0);
-    CelType type = extractAstTypeOrDefault(arg, ast);
-
-    Expr<?> baseResult = typeSystem.wrapBool(ctx.mkNot((BoolExpr) arg.unwrapZ3Bool()));
-    if (!type.equals(SimpleType.BOOL)) {
-      baseResult = typeSystem.withRuntimeError(baseResult, ctx.mkNot(arg.isZ3Bool()));
-    }
+    Expr<?> baseResult =
+        typeSystem.withRuntimeError(
+            typeSystem.wrapBool(ctx.mkNot((BoolExpr) arg.unwrapZ3Bool())),
+            ctx.mkNot(arg.isZ3Bool()));
 
     return TranslatedValue.propagateStrict(
         ctx, typeSystem, Operator.LOGICAL_NOT.getFunction(), baseResult, args);
   }
 
-  private TranslatedValue translateNegate(TranslatedValue arg, CelAbstractSyntaxTree ast) {
-    CelType type = extractAstTypeOrDefault(arg, ast);
-    Expr<?> z3Expr = arg.z3Expr();
-
-    Expr<?> result;
-    if (type.equals(SimpleType.INT)) {
-      ArithExpr intNeg = ctx.mkUnaryMinus(typeSystem.getInt(z3Expr));
-      result =
-          typeSystem.withRuntimeError(
-              typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg));
-    } else if (type.equals(SimpleType.DOUBLE)) {
-      result = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr)));
-    } else {
-      ArithExpr intNeg = ctx.mkUnaryMinus(typeSystem.getInt(z3Expr));
-      Expr<?> intResult =
-          typeSystem.withRuntimeError(
-              typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg));
-      Expr<?> doubleResult = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr)));
-      result =
-          CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
-              .addCase(typeSystem.isInt(z3Expr), intResult)
-              .addCase(typeSystem.isDouble(z3Expr), doubleResult)
-              .build(typeSystem.mkError());
-    }
-    return TranslatedValue.propagateStrict(
-        ctx, typeSystem, Operator.NEGATE.getFunction(), result, arg);
-  }
-
   private BoolExpr isNumeric(Expr<?> arg) {
     return ctx.mkOr(typeSystem.isInt(arg), typeSystem.isUint(arg), typeSystem.isDouble(arg));
   }
@@ -564,14 +526,14 @@ private BoolExpr getNumericEquality(
       boolean approximateIntDouble) {
     if (arg0.isNumericConstant()) {
       return getNumericEqualityWithConstant(
-          arg1.z3Expr(), arg0.celExpr().get().constant(), extractAstTypeOrDefault(arg1, ast));
+          arg1.z3Expr(), arg0.celExpr().get().constant(), trustedType(arg1, ast));
     } else if (arg1.isNumericConstant()) {
       return getNumericEqualityWithConstant(
-          arg0.z3Expr(), arg1.celExpr().get().constant(), extractAstTypeOrDefault(arg0, ast));
+          arg0.z3Expr(), arg1.celExpr().get().constant(), trustedType(arg0, ast));
     }
 
-    CelType type0 = extractAstTypeOrDefault(arg0, ast);
-    CelType type1 = extractAstTypeOrDefault(arg1, ast);
+    CelType type0 = trustedType(arg0, ast);
+    CelType type1 = trustedType(arg1, ast);
     if (isStaticallyKnown(type0) && isStaticallyKnown(type1) && type0.kind() == type1.kind()) {
       return getStaticallyKnownNumericEquality(arg0.z3Expr(), type0, arg1.z3Expr());
     }
@@ -952,8 +914,11 @@ private TranslatedValue translateEquality(
     Expr<?> z3Arg0 = arg0.z3Expr();
     Expr<?> z3Arg1 = arg1.z3Expr();
 
-    CelType type0 = extractAstTypeOrDefault(arg0, ast);
-    CelType type1 = extractAstTypeOrDefault(arg1, ast);
+    // A literal's kind is known even if its type may be narrowed.
+    CelType trusted0 = trustedType(arg0, ast);
+    CelType trusted1 = trustedType(arg1, ast);
+    CelType type0 = isContainerLiteral(arg0) ? extractAstTypeOrDefault(arg0, ast) : trusted0;
+    CelType type1 = isContainerLiteral(arg1) ? extractAstTypeOrDefault(arg1, ast) : trusted1;
 
     BoolExpr equality;
     List<BoolExpr> taints = new ArrayList<>();
@@ -961,7 +926,7 @@ private TranslatedValue translateEquality(
       taints.add(mayObserveTruncatedTypeConstraint(ast, arg0, arg1));
     }
 
-    if (isNumericType(type0) && isNumericType(type1)) {
+    if (isNumericType(trusted0) && isNumericType(trusted1)) {
       equality = getNumericEquality(arg0, arg1, ast, taints, /* approximateIntDouble= */ false);
     } else {
       BoolExpr bothLists = ctx.mkAnd(typeSystem.isList(z3Arg0), typeSystem.isList(z3Arg1));
@@ -993,12 +958,12 @@ private TranslatedValue translateEquality(
                     ctx.mkITE(bothLists, unrollListEquality(arg0, arg1, ast, taints), structuralEq);
           } else if (type0.kind() == CelKind.MAP || type1.kind() == CelKind.MAP) {
             BoolExpr mapEquality =
-                isExact(type0, type1)
+                isExact(trusted0, trusted1)
                         && (arg0.isLiteral(ExprKind.Kind.MAP) || arg1.isLiteral(ExprKind.Kind.MAP))
                     ? mapEqualityAtLiteralKeys(arg0, arg1)
                     : unrollMapEquality(arg0, arg1, ast, taints);
             structuralEq = (BoolExpr) ctx.mkITE(bothMaps, mapEquality, structuralEq);
-          } else if (!isStaticallyKnown(type0) && !isStaticallyKnown(type1)) {
+          } else if (!isStaticallyKnown(trusted0) && !isStaticallyKnown(trusted1)) {
             // Performance only: a side with a known type isn't a list or map here.
             // TODO: Unless the type checker narrowed it, e.g. `(int_list +
             // dyn_var)[0]`.
@@ -1034,7 +999,7 @@ private TranslatedValue translateEquality(
   }
 
   private Expr<?> buildListIndex(
-      Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, boolean isOptional) {
+      Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, BoolExpr returnOptional) {
     Expr<?> listRef = typeSystem.getListRef(lhsTrans);
     SeqExpr<?> seq = typeSystem.getSeq(listRef);
     Expr<?> index = typeSystem.getInt(rhsTrans);
@@ -1043,31 +1008,37 @@ private Expr<?> buildListIndex(
             ctx.mkGe((ArithExpr) index, ctx.mkInt(0)),
             ctx.mkLt((ArithExpr) index, ctx.mkLength(seq)));
 
-    return finishIndex(inBounds, ctx.mkNth(seq, (ArithExpr) index), typeGuard, isOptional);
+    return finishIndex(inBounds, ctx.mkNth(seq, (ArithExpr) index), typeGuard, returnOptional);
   }
 
   private Expr<?> buildMapIndex(
-      Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, boolean isOptional) {
+      Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, BoolExpr returnOptional) {
     ImmutableList<CelZ3TypeSystem.EqualKey> equalKeys = typeSystem.equalKeys(rhsTrans);
     return finishIndex(
         typeSystem.hasEqualKey(lhsTrans, equalKeys),
         typeSystem.valueAtEqualKey(lhsTrans, equalKeys),
         typeGuard,
-        isOptional);
+        returnOptional);
   }
 
-  // Returns val where found, or else an error (or an empty optional).
-  private Expr<?> finishIndex(BoolExpr found, Expr<?> val, BoolExpr typeGuard, boolean isOptional) {
+  // Returns val where found, or else an error, as an optional (empty if not found) where
+  // returnOptional holds.
+  private Expr<?> finishIndex(
+      BoolExpr found, Expr<?> val, BoolExpr typeGuard, BoolExpr returnOptional) {
     context.constrainValidValue(ctx.mkAnd(typeGuard, found), val);
-    if (isOptional) {
-      Expr<?> resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val);
-      context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val));
-      context.addConstraint(typeSystem.optHasValue(resultOptRef));
-      return ctx.mkITE(found, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
+    Expr<?> plain = ctx.mkITE(found, val, typeSystem.mkError());
+    // Performance only: skips building an optional that isn't returned.
+    if (returnOptional.isFalse()) {
+      return plain;
     }
-    return ctx.mkITE(found, val, typeSystem.mkError());
+    Expr<?> optional = ctx.mkITE(found, context.mkOptionalOf(val), typeSystem.mkOptionalNone());
+    return returnOptional.isTrue() ? optional : ctx.mkITE(returnOptional, optional, plain);
   }
 
+  /**
+   * Translates {@code lhs[rhs]}, or {@code lhs[?rhs]} if isOptional. An optional lhs is indexed
+   * optionally (e.g. {@code optional.of([])[0]} is {@code optional.none()}).
+   */
   private TranslatedValue translateIndex(
       List<TranslatedValue> args, CelAbstractSyntaxTree ast, boolean isOptional) {
     TranslatedValue lhs = args.get(0);
@@ -1081,8 +1052,10 @@ private TranslatedValue translateIndex(
     BoolExpr isLhsOpt = ctx.mkFalse();
     BoolExpr lhsHasValue = ctx.mkFalse();
     BoolExpr shouldEvaluate = ctx.mkTrue();
+    BoolExpr returnOptional = isOptional ? ctx.mkTrue() : ctx.mkFalse();
 
-    if (isOptional) {
+    // Performance only: an lhs of a known type other than optional isn't one.
+    if (lhsType instanceof OptionalType || !isStaticallyKnown(lhsType)) {
       isLhsOpt = typeSystem.isOptional(lhsTrans);
       Expr<?> optRef = typeSystem.getOptionalRef(lhsTrans);
       lhsHasValue = typeSystem.optHasValue(optRef);
@@ -1092,21 +1065,24 @@ private TranslatedValue translateIndex(
 
       if (lhsType instanceof OptionalType) {
         lhsType = lhsType.parameters().get(0);
+        returnOptional = ctx.mkTrue();
+      } else if (!isOptional) {
+        returnOptional = isLhsOpt;
       }
     }
 
     TranslatedValue element =
         buildAndConstrainIndex(
-            lhsTrans, rhsTrans, lhsType, isLhsTypeGuaranteed, shouldEvaluate, isOptional);
-    Expr<?> actualValue = element.z3Expr();
-
-    if (isOptional) {
-      actualValue =
-          ctx.mkITE(
-              ctx.mkAnd(isLhsOpt, ctx.mkNot(lhsHasValue)),
-              typeSystem.mkOptionalNone(),
-              actualValue);
-    }
+            lhsTrans, rhsTrans, lhsType, isLhsTypeGuaranteed, shouldEvaluate, returnOptional);
+    // An empty optional gives an empty optional, unless no overload takes the index (e.g. a string
+    // indexing an optional list).
+    BoolExpr takesIndex =
+        lhsType.kind() == CelKind.LIST ? typeSystem.isInt(rhsTrans) : ctx.mkTrue();
+    Expr<?> actualValue =
+        ctx.mkITE(
+            CelZ3Exprs.mkAndFlattened(ctx, isLhsOpt, ctx.mkNot(lhsHasValue), takesIndex),
+            typeSystem.mkOptionalNone(),
+            element.z3Expr());
 
     String opName =
         isOptional ? Operator.OPTIONAL_INDEX.getFunction() : Operator.INDEX.getFunction();
@@ -1137,7 +1113,7 @@ private TranslatedValue buildAndConstrainIndex(
       CelType lhsType,
       boolean isLhsTypeGuaranteed,
       BoolExpr shouldEvaluate,
-      boolean isOptional) {
+      BoolExpr returnOptional) {
     CelType expectedElemType = null;
     if (lhsType.kind() == CelKind.LIST) {
       expectedElemType = ((ListType) lhsType).elemType();
@@ -1146,20 +1122,22 @@ private TranslatedValue buildAndConstrainIndex(
     }
 
     if (expectedElemType != null) {
-      Expr<?> actualValue;
-      if (lhsType.kind() == CelKind.MAP) {
-        actualValue = buildMapIndex(lhsTrans, rhsTrans, shouldEvaluate, isOptional);
-      } else {
-        BoolExpr isIntIndex = typeSystem.isInt(rhsTrans);
-        actualValue =
-            ctx.mkITE(
-                isIntIndex,
-                buildListIndex(
-                    lhsTrans, rhsTrans, ctx.mkAnd(shouldEvaluate, isIntIndex), isOptional),
-                typeSystem.mkError());
-      }
-
-      CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType;
+      // The static type picks the overload, which errors on the other kind if it was narrowed.
+      BoolExpr takesIndex =
+          lhsType.kind() == CelKind.MAP
+              ? typeSystem.isMap(lhsTrans)
+              : ctx.mkAnd(typeSystem.isList(lhsTrans), typeSystem.isInt(rhsTrans));
+      BoolExpr guard = ctx.mkAnd(shouldEvaluate, takesIndex);
+      Expr<?> actualValue =
+          ctx.mkITE(
+              takesIndex,
+              lhsType.kind() == CelKind.MAP
+                  ? buildMapIndex(lhsTrans, rhsTrans, guard, returnOptional)
+                  : buildListIndex(lhsTrans, rhsTrans, guard, returnOptional),
+              typeSystem.mkError());
+
+      CelType finalType =
+          returnOptional.isTrue() ? OptionalType.create(expectedElemType) : expectedElemType;
       BoolExpr isDefined = ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue)));
       BoolExpr typeConstraint =
           typeConstraintGenerator.createTypeConstraintForType(actualValue, finalType);
@@ -1182,27 +1160,22 @@ private TranslatedValue buildAndConstrainIndex(
 
     return TranslatedValue.create(
         CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
-            .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
-            .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
+            .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, returnOptional))
+            .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, returnOptional))
             .build(typeSystem.mkError()),
         typeSystem,
         ctx.mkFalse());
   }
 
-  private TranslatedValue translateConditional(
-      List<TranslatedValue> args, CelAbstractSyntaxTree ast) {
+  private TranslatedValue translateConditional(List<TranslatedValue> args) {
     TranslatedValue cond = args.get(0);
     TranslatedValue trueBranch = args.get(1);
     TranslatedValue falseBranch = args.get(2);
-    CelType condType = extractAstTypeOrDefault(cond, ast);
 
     BoolExpr condTrue = ctx.mkAnd(cond.isZ3Bool(), (BoolExpr) cond.unwrapZ3Bool());
 
-    BoolExpr hasError = cond.isZ3Error();
+    BoolExpr hasError = ctx.mkNot(cond.isZ3Bool());
     BoolExpr hasUnknown = cond.isZ3Unknown();
-    if (!condType.equals(SimpleType.BOOL)) {
-      hasError = ctx.mkOr(hasError, ctx.mkNot(cond.isZ3Bool()));
-    }
 
     Expr<?> unknownResult =
         typeSystem.isParameterizingUnknowns()
@@ -1243,6 +1216,12 @@ private static CelType extractAstTypeOrDefault(TranslatedValue val, CelAbstractS
     return val.celExpr().map(node -> ast.getTypeOrThrow(node.id())).orElse(SimpleType.DYN);
   }
 
+  // The static type of val unless the type checker may have narrowed it (e.g. `dyn_var.orValue(1)`
+  // is typed int). Overloads are still picked by static types.
+  private CelType trustedType(TranslatedValue val, CelAbstractSyntaxTree ast) {
+    return val.celExpr().map(e -> context.trustedType(e, ast)).orElse(SimpleType.DYN);
+  }
+
   /**
    * Returns the type that {@code val} is guaranteed to conform to at runtime: a constant's, the
    * declared type of an input variable, or else dyn. Global constraints may only be derived from
@@ -1300,9 +1279,11 @@ private static boolean hasStructuralEquality(CelType type) {
     }
   }
 
+  // A wrapper's kind is its value's, but it may also be null.
   private static boolean isNumericType(CelType type) {
     CelKind kind = type.kind();
-    return kind == CelKind.INT || kind == CelKind.UINT || kind == CelKind.DOUBLE;
+    return !(type instanceof NullableType)
+        && (kind == CelKind.INT || kind == CelKind.UINT || kind == CelKind.DOUBLE);
   }
 
   /**
@@ -1312,7 +1293,7 @@ private static boolean isNumericType(CelType type) {
    */
   private BoolExpr mayObserveTruncatedTypeConstraint(
       CelAbstractSyntaxTree ast, TranslatedValue... args) {
-    if (Arrays.stream(args).allMatch(arg -> isConcrete(extractAstTypeOrDefault(arg, ast)))) {
+    if (Arrays.stream(args).allMatch(arg -> isConcrete(trustedType(arg, ast)))) {
       return ctx.mkFalse();
     }
     return context.recordUnrollLimitApproximation(
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
index 11cc36191..00ee7e7f2 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
@@ -26,6 +26,7 @@
 import com.microsoft.z3.SeqExpr;
 import dev.cel.common.CelAbstractSyntaxTree;
 import dev.cel.common.ast.CelExpr;
+import dev.cel.common.ast.CelExpr.ExprKind;
 import dev.cel.common.internal.ProtoTimeUtils;
 import dev.cel.common.types.CelKind;
 import dev.cel.common.types.CelType;
@@ -536,13 +537,41 @@ private FieldAccess getMsgAccess(Expr<?> operand, String field, BoolExpr typeGua
     return new FieldAccess(presence, value);
   }
 
+  /**
+   * Translates {@code e.f}, {@code has(e.f)} or {@code e.?f} (an optional of {@code e.f} if {@code
+   * has(e.f)}, else empty).
+   */
   TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
-    CelExpr.CelSelect select = celExpr.select();
+    boolean isOptional = celExpr.getKind() == ExprKind.Kind.CALL;
+    CelExpr operandExpr = isOptional ? celExpr.call().args().get(0) : celExpr.select().operand();
+    String field =
+        isOptional
+            ? celExpr.call().args().get(1).constant().stringValue()
+            : celExpr.select().field();
+    boolean testOnly = !isOptional && celExpr.select().testOnly();
     long exprId = celExpr.id();
-    TranslatedValue operandTv = translateExpr(select.operand(), ast);
+    TranslatedValue operandTv = translateExpr(operandExpr, ast);
     Expr<?> operand = operandTv.z3Expr();
-    String field = select.field();
-    CelType operandType = extractAstTypeOrDefault(ast, select.operand().id());
+    CelType operandType = context.trustedType(operandExpr, ast);
+    // Selecting from an optional selects from its value optionally (e.g. `optional.of({}).a` is
+    // `optional.none()`). Performance only: an operand of a known type other than optional isn't.
+    boolean mayBeOptional =
+        operandType instanceof OptionalType
+            || !CelZ3OperatorTranslator.isStaticallyKnown(operandType);
+    BoolExpr isOptionalOperand = ctx.mkFalse();
+    BoolExpr hasValue = ctx.mkFalse();
+    BoolExpr shouldEvaluate = ctx.mkTrue();
+    if (mayBeOptional) {
+      Expr<?> optRef = typeSystem.getOptionalRef(operand);
+      isOptionalOperand = typeSystem.isOptional(operand);
+      hasValue = typeSystem.optHasValue(optRef);
+      shouldEvaluate = (BoolExpr) ctx.mkITE(isOptionalOperand, hasValue, ctx.mkTrue());
+      operand = ctx.mkITE(isOptionalOperand, typeSystem.getOptionalValue(optRef), operand);
+    }
+    if (operandType instanceof OptionalType) {
+      // Performance only: reads the value by its static type.
+      operandType = operandType.parameters().get(0);
+    }
 
     Expr<?> presenceResult;
     Expr<?> valueResult;
@@ -550,11 +579,11 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
     BoolExpr presenceError = ctx.mkFalse();
 
     if (operandType instanceof MapType) {
-      FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkTrue());
+      FieldAccess mapAcc = getMapAccess(operand, field, shouldEvaluate);
       presenceResult = mapAcc.presence;
       valueResult = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
     } else if (operandType.kind() == CelKind.STRUCT) {
-      FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkTrue());
+      FieldAccess msgAcc = getMsgAccess(operand, field, shouldEvaluate);
       presenceResult = msgAcc.presence;
       Expr<?> defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId));
       valueResult = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal);
@@ -563,8 +592,8 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
       BoolExpr isMap = typeSystem.isMap(operand);
       BoolExpr isMessage = typeSystem.isMessage(operand);
 
-      FieldAccess mapAcc = getMapAccess(operand, field, isMap);
-      FieldAccess msgAcc = getMsgAccess(operand, field, isMessage);
+      FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkAnd(shouldEvaluate, isMap));
+      FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkAnd(shouldEvaluate, isMessage));
 
       presenceResult =
           CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
@@ -590,13 +619,13 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
           msgRead.addCase(isType, typeSystem.mkError());
           continue;
         }
-        if (select.testOnly()) {
+        if (testOnly) {
           continue;
         }
         CelType fieldType = declared.get().type();
         context.addConstraint(
             ctx.mkImplies(
-                ctx.mkAnd(isMessage, isType, msgAcc.presence),
+                ctx.mkAnd(shouldEvaluate, isMessage, isType, msgAcc.presence),
                 typeConstraintGenerator.createTypeConstraintForType(msgAcc.value, fieldType)));
         msgRead.addCase(
             isType, ctx.mkITE(msgAcc.presence, msgAcc.value, getDefaultValueForType(fieldType)));
@@ -605,7 +634,10 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
       unmodeledMessage =
           context.recordApproximation(
               "messages of types the type provider doesn't declare",
-              ctx.mkAnd(isMessage, ctx.mkNot(CelZ3Exprs.mkOrFlattened(ctx, isModeledType))));
+              ctx.mkAnd(
+                  shouldEvaluate,
+                  isMessage,
+                  ctx.mkNot(CelZ3Exprs.mkOrFlattened(ctx, isModeledType))));
       Expr<?> mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
       // Testing an undeclared field, or a field of something other than a map or message, errors.
       presenceError =
@@ -622,12 +654,33 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
               .build(typeSystem.mkError());
     }
 
+    // has(e.f), else e.f, or for e.?f and an optional e, an optional of e.f if has(e.f).
     Expr<?> fieldAccess =
-        select.testOnly()
+        testOnly
             ? typeSystem.withRuntimeError(typeSystem.wrapBool(presenceResult), presenceError)
             : valueResult;
+    Expr<?> chained = fieldAccess;
+    if (!testOnly && (isOptional || mayBeOptional)) {
+      chained =
+          ctx.mkITE(
+              presenceError,
+              typeSystem.mkError(),
+              ctx.mkITE(
+                  (BoolExpr) presenceResult,
+                  context.mkOptionalOf(valueResult),
+                  typeSystem.mkOptionalNone()));
+      fieldAccess = isOptional ? chained : valueResult;
+    }
+    if (mayBeOptional) {
+      Expr<?> empty = testOnly ? typeSystem.mkBool(false) : typeSystem.mkOptionalNone();
+      fieldAccess = ctx.mkITE(isOptionalOperand, ctx.mkITE(hasValue, chained, empty), fieldAccess);
+    }
 
-    context.addConstraint(typeConstraintGenerator.createTypeConstraint(fieldAccess, exprId, ast));
+    context.addConstraint(
+        ctx.mkOr(
+            typeSystem.isErrorOrUnknown(fieldAccess),
+            typeConstraintGenerator.createTypeConstraintForType(
+                fieldAccess, context.trustedType(celExpr, ast))));
 
     TranslatedValue result =
         TranslatedValue.propagateStrict(
@@ -636,9 +689,11 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
     return operandType.kind() == CelKind.STRUCT
         ? result
         : result.withApproximation(
-            CelZ3Exprs.mkOrFlattened(ctx, context.isTruncatedMap(operand), unmodeledMessage));
+            CelZ3Exprs.mkOrFlattened(
+                ctx, ctx.mkAnd(shouldEvaluate, context.isTruncatedMap(operand)), unmodeledMessage));
   }
 
+
   private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long id) {
     return ast.getType(id).orElse(SimpleType.DYN);
   }
diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
index fb6f7270d..686d43100 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
@@ -17,16 +17,24 @@
 import static com.google.common.collect.ImmutableList.toImmutableList;
 
 import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
 import com.microsoft.z3.BoolExpr;
 import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.Model;
+import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.Operator;
+import dev.cel.common.ast.CelBlock;
+import dev.cel.common.ast.CelExpr;
+import dev.cel.common.types.CelKind;
 import dev.cel.common.types.CelType;
 import dev.cel.common.types.SimpleType;
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collections;
 import java.util.HashMap;
+import java.util.HashSet;
+import java.util.IdentityHashMap;
 import java.util.LinkedHashMap;
 import java.util.LinkedHashSet;
 import java.util.List;
@@ -49,6 +57,8 @@ final class CelZ3TranslationContext {
   private final Map<String, List<BoolExpr>> approximationTerms;
   private final Map<String, TranslatedValue> symbolTable;
   private final Map<String, TranslatedValue> localScope;
+  private final IdentityHashMap<CelAbstractSyntaxTree, Set<Long>> narrowedExprIds;
+  private final Set<String> narrowedSymbols;
 
   Context ctx() {
     return ctx;
@@ -80,6 +90,14 @@ void constrainValidValue(BoolExpr guard, Expr<?> value) {
     addConstraint(ctx.mkImplies(guard, typeSystem.isValidValue(value)));
   }
 
+  /** Returns an optional holding {@code value}. */
+  Expr<?> mkOptionalOf(Expr<?> value) {
+    Expr<?> optRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), value);
+    addConstraint(ctx.mkEq(typeSystem.getOptionalValue(optRef), value));
+    addConstraint(typeSystem.optHasValue(optRef));
+    return typeSystem.mkOptionalOf(optRef);
+  }
+
   void addInputVariable(Expr<?> variable, CelType declaredType) {
     inputVariableTypes.put(variable, declaredType);
   }
@@ -94,6 +112,115 @@ CelType guaranteedType(Expr<?> value) {
     return inputVariableTypes.getOrDefault(value, SimpleType.DYN);
   }
 
+  /**
+   * Whether the type checker may have narrowed the static type of {@code expr} by unifying a type
+   * parameter with dyn or null (e.g. {@code int_list + dyn_var} is typed list(int) but may hold
+   * doubles).
+   */
+  boolean mayBeNarrowed(CelExpr expr, CelAbstractSyntaxTree ast) {
+    return narrowedExprIds
+        .computeIfAbsent(
+            ast,
+            a -> {
+              Set<Long> ids = new HashSet<>();
+              collectNarrowed(a.getExpr(), a, ImmutableMap.of(), ids);
+              return ids;
+            })
+        .contains(expr.id());
+  }
+
+  /** The static type of {@code expr}, or dyn if the type checker may have narrowed it. */
+  CelType trustedType(CelExpr expr, CelAbstractSyntaxTree ast) {
+    return mayBeNarrowed(expr, ast)
+        ? SimpleType.DYN
+        : ast.getType(expr.id()).orElse(SimpleType.DYN);
+  }
+
+  // Adds expr to ids if it may be narrowed: a subexpression, or a variable it reads, is typed dyn
+  // or null, or is narrowed. Returns whether expr is either.
+  private boolean collectNarrowed(
+      CelExpr expr, CelAbstractSyntaxTree ast, Map<String, Boolean> boundVars, Set<Long> ids) {
+    boolean narrowed = false;
+    switch (expr.getKind()) {
+      case IDENT:
+        String name = expr.ident().name();
+        narrowed = boundVars.getOrDefault(name, narrowedSymbols.contains(name));
+        break;
+      case SELECT:
+        narrowed = collectNarrowed(expr.select().operand(), ast, boundVars, ids);
+        break;
+      case CALL:
+        CelExpr.CelCall call = expr.call();
+        ImmutableList<CelExpr> args = call.args();
+        if (call.function().equals(CelBlock.FUNCTION_NAME)) {
+          // `cel.@block([e0, e1, ...], result)` binds @index0 to e0, and so on.
+          Map<String, Boolean> scope = new HashMap<>(boundVars);
+          ImmutableList<CelExpr> slots = args.get(0).list().elements();
+          for (int i = 0; i < slots.size(); i++) {
+            scope.put(CelBlock.INDEX_PREFIX + i, collectNarrowed(slots.get(i), ast, scope, ids));
+          }
+          narrowed = collectNarrowed(args.get(1), ast, scope, ids);
+          break;
+        }
+        if (call.target().isPresent()) {
+          narrowed = collectNarrowed(call.target().get(), ast, boundVars, ids);
+        }
+        // The field name of `e.?f` isn't typed.
+        if (call.function().equals(Operator.OPTIONAL_SELECT.getFunction())) {
+          args = args.subList(0, 1);
+        }
+        for (CelExpr arg : args) {
+          narrowed |= collectNarrowed(arg, ast, boundVars, ids);
+        }
+        break;
+      case LIST:
+        for (CelExpr element : expr.list().elements()) {
+          narrowed |= collectNarrowed(element, ast, boundVars, ids);
+        }
+        break;
+      case MAP:
+        for (CelExpr.CelMap.Entry entry : expr.map().entries()) {
+          narrowed |= collectNarrowed(entry.key(), ast, boundVars, ids);
+          narrowed |= collectNarrowed(entry.value(), ast, boundVars, ids);
+        }
+        break;
+      case STRUCT:
+        for (CelExpr.CelStruct.Entry entry : expr.struct().entries()) {
+          narrowed |= collectNarrowed(entry.value(), ast, boundVars, ids);
+        }
+        break;
+      case COMPREHENSION:
+        // Its value is the result's, which reads the variables.
+        CelExpr.CelComprehension comp = expr.comprehension();
+        boolean range = collectNarrowed(comp.iterRange(), ast, boundVars, ids);
+        Map<String, Boolean> scope = new HashMap<>(boundVars);
+        scope.put(comp.iterVar(), range);
+        scope.put(comp.iterVar2(), range);
+        scope.put(comp.accuVar(), collectNarrowed(comp.accuInit(), ast, boundVars, ids));
+        // The accumulator also holds what each step computes.
+        if (collectNarrowed(comp.loopStep(), ast, scope, ids) && !scope.get(comp.accuVar())) {
+          scope.put(comp.accuVar(), true);
+          collectNarrowed(comp.loopStep(), ast, scope, ids);
+        }
+        collectNarrowed(comp.loopCondition(), ast, scope, ids);
+        narrowed = collectNarrowed(comp.result(), ast, scope, ids);
+        break;
+      default:
+        break;
+    }
+    if (narrowed) {
+      ids.add(expr.id());
+    }
+    return narrowed || involvesDynOrNull(ast.getType(expr.id()).orElse(SimpleType.DYN));
+  }
+
+  private static boolean involvesDynOrNull(CelType type) {
+    return type.kind().isDyn()
+        || type.kind().isTypeParam()
+        || type.kind() == CelKind.NULL_TYPE
+        || type.parameters().stream().anyMatch(CelZ3TranslationContext::involvesDynOrNull);
+  }
+
   /**
    * Whether {@code val} is a map with more keys than the unroll limit, beyond which its presence is
    * not linked to its keys.
@@ -169,8 +296,13 @@ BoolExpr hasUnmodeledResult() {
     return CelZ3Exprs.mkOrFlattened(ctx, unmodeledResults);
   }
 
-  void bindSymbol(String name, TranslatedValue value) {
+  /** Binds {@code name} to {@code value}, the result of {@code ast}. */
+  void bindSymbol(String name, TranslatedValue value, CelAbstractSyntaxTree ast) {
     localScope.put(name, value);
+    // Other expressions read it with its static type, which may be narrowed.
+    if (mayBeNarrowed(ast.getExpr(), ast) || involvesDynOrNull(ast.getResultType())) {
+      narrowedSymbols.add(name);
+    }
   }
 
   Optional<TranslatedValue> lookupSymbol(String name) {
@@ -212,5 +344,7 @@ <T> T withScope(String varName, TranslatedValue value, Supplier<T> action) {
     this.approximationTerms = new LinkedHashMap<>();
     this.symbolTable = new HashMap<>();
     this.localScope = new HashMap<>();
+    this.narrowedExprIds = new IdentityHashMap<>();
+    this.narrowedSymbols = new HashSet<>();
   }
 }
diff --git a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
index 7ea52abc8..201739f66 100644
--- a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
+++ b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
@@ -199,6 +199,8 @@ private static String extractOpName(CelExpr expr) {
     switch (expr.exprKind().getKind()) {
       case SELECT:
         return "select_" + expr.select().field() + "_" + expr.select().testOnly();
+      case CALL: // e.?f
+        return "optional_select_" + expr.call().args().get(1).constant().stringValue();
       case STRUCT:
         StringBuilder structSb = new StringBuilder("struct_").append(expr.struct().messageName());
         for (CelExpr.CelStruct.Entry entry : expr.struct().entries()) {
diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
index dd983d36b..748b6f6ca 100644
--- a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
+++ b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java
@@ -20,12 +20,10 @@
 import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OF_NON_ZERO_VALUE;
 import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OR;
 import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OR_VALUE;
-import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_SELECT;
 import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_VALUE;
 
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableList;
-import com.microsoft.z3.ArrayExpr;
 import com.microsoft.z3.BoolExpr;
 import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;
@@ -33,7 +31,6 @@
 import com.microsoft.z3.SeqExpr;
 import dev.cel.common.CelFunctionDecl;
 import dev.cel.common.CelOverloadDecl;
-import dev.cel.verifier.CelZ3Exprs;
 import dev.cel.verifier.CelZ3TypeSystem;
 import java.util.Optional;
 
@@ -88,63 +85,6 @@ final class OptionalAxioms {
               (ctx, ts, sink, val, other) -> {
                 Expr<?> optRef = ts.getOptionalRef(val);
                 return Optional.of(ctx.mkITE(ts.optHasValue(optRef), val, other));
-              }),
-          createBinaryAxiom(
-              OPTIONAL_SELECT,
-              (ctx, ts, sink, operand, field) -> {
-                Expr<?> optRef = ts.getOptionalRef(operand);
-                BoolExpr isOpt = ts.isOptional(operand);
-                BoolExpr hasValue = ts.optHasValue(optRef);
-                Expr<?> actualOperand = ctx.mkITE(isOpt, ts.getOptionalValue(optRef), operand);
-
-                BoolExpr isMap = ts.isMap(actualOperand);
-                BoolExpr isMsg = ts.isMessage(actualOperand);
-                BoolExpr isValidTarget = ctx.mkOr(isMap, isMsg);
-
-                Expr<?> msgFieldZ3Str = ts.getString(field);
-                Expr<?> mapFieldCelVal = field;
-
-                Expr<?> msgRef = ts.getMessageRef(actualOperand);
-                Expr<?> mapRef = ts.getMapRef(actualOperand);
-
-                Expr<?> presence =
-                    CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
-                        .addCase(
-                            isMsg,
-                            ctx.mkSelect((ArrayExpr) ts.getMsgPresence(msgRef), msgFieldZ3Str))
-                        .addCase(
-                            isMap,
-                            ctx.mkSelect((ArrayExpr) ts.getMapPresence(mapRef), mapFieldCelVal))
-                        .build(ctx.mkFalse());
-
-                Expr<?> value =
-                    CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
-                        .addCase(
-                            isMsg, ctx.mkSelect((ArrayExpr) ts.getMsgValues(msgRef), msgFieldZ3Str))
-                        .addCase(
-                            isMap,
-                            ctx.mkSelect((ArrayExpr) ts.getMapValues(mapRef), mapFieldCelVal))
-                        .build(ts.mkError());
-
-                BoolExpr valNotError = ctx.mkNot(ctx.mkEq(value, ts.mkError()));
-                BoolExpr shouldEvaluate = (BoolExpr) ctx.mkITE(isOpt, hasValue, ctx.mkTrue());
-                sink.accept(
-                    ctx.mkImplies(
-                        CelZ3Exprs.mkAndFlattened(
-                            ctx, shouldEvaluate, isValidTarget, (BoolExpr) presence),
-                        valNotError));
-
-                Expr<?> resultOptRef = ctx.mkApp(ts.optionalOfRefFunc(), value);
-                sink.accept(ctx.mkEq(ts.getOptionalValue(resultOptRef), value));
-                sink.accept(ts.optHasValue(resultOptRef));
-
-                Expr<?> optionalResult =
-                    ctx.mkITE(
-                        (BoolExpr) presence, ts.mkOptionalOf(resultOptRef), ts.mkOptionalNone());
-
-                Expr<?> result = ctx.mkITE(isValidTarget, optionalResult, ts.mkError());
-                return Optional.of(
-                    ctx.mkITE(ctx.mkAnd(isOpt, ctx.mkNot(hasValue)), ts.mkOptionalNone(), result));
               }));
 
   private static BoolExpr isZeroValue(Context ctx, CelZ3TypeSystem ts, Expr<?> val) {
diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
index 8c18f4da9..1fa2f5947 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
@@ -450,6 +450,39 @@ public void verifyInvariants_restrictedDestinationsPolicy_verified() throws Exce
             "unrestricted_destination_allowed", CelVerificationResult.verified());
   }
 
+  @Test
+  public void verifyInvariants_narrowedVariable_violated() throws Exception {
+    Cel optionalCel =
+        CEL.toCelBuilder()
+            .addCompilerLibraries(CelOptionalLibrary.INSTANCE)
+            .addRuntimeLibraries(CelOptionalLibrary.INSTANCE)
+            .build();
+    CelPolicyVerifier verifier =
+        CelPolicyVerifierFactory.newVerifier(
+                CelPolicyCompilerFactory.newPolicyCompiler(optionalCel).build(),
+                CelVerifierFactory.newVerifier(optionalCel).build())
+            .build();
+    // variables.v is typed int, but is NaN for request = optional.of(0.0 / 0.0).
+    String policySource =
+        "name: narrowed_variable_policy\n" //
+            + "rule:\n" //
+            + "  match:\n" //
+            + "    - output: 'true'\n" //
+            + "verification:\n" //
+            + "  variables:\n" //
+            + "    - v: request.orValue(1)\n" //
+            + "  invariants:\n" //
+            + "    - id: variable_equals_itself\n" //
+            + "      assume: request.hasValue()\n" //
+            + "      assert: variables.v == variables.v";
+
+    ImmutableMap<String, CelVerificationResult> results =
+        verifier.verifyInvariants(PARSER.parse(policySource));
+
+    assertThat(results.get("variable_equals_itself").status())
+        .isEqualTo(VerificationStatus.VIOLATED);
+  }
+
   @Test
   public void verifyInvariants_invariantReferencesPolicyVariable_verified() throws Exception {
     String policySource =
@@ -554,12 +587,12 @@ public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws
     assertThat(results).containsKey("universal_no_unapproved_privileged_prod");
     assertThat(results.get("universal_no_unapproved_privileged_prod").status())
         .isEqualTo(VerificationStatus.VIOLATED);
+    // Either the admin or the owner bypass violates it.
     assertThat(results.get("universal_no_unapproved_privileged_prod").message())
-        .isEqualTo(
+        .containsMatch(
             "Invariant 'universal_no_unapproved_privileged_prod' violation detected."
                 + " Counterexample input:\n"
-                + "  is_admin = true\n"
-                + "  is_owner = false\n"
+                + "  is_admin = (true\n  is_owner = (true|false)|false\n  is_owner = true)\n"
                 + "  is_privileged = true\n"
                 + "  is_prod = true\n"
                 + "  has_approval = false");
diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
index 8951801f7..ec16bc917 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
@@ -58,6 +58,7 @@
 import dev.cel.optimizer.CelOptimizer;
 import dev.cel.optimizer.CelOptimizerFactory;
 import dev.cel.optimizer.optimizers.ConstantFoldingOptimizer;
+import dev.cel.optimizer.optimizers.SubexpressionOptimizer;
 import dev.cel.parser.CelMacro;
 import dev.cel.parser.CelStandardMacro;
 import dev.cel.verifier.CelVerificationResult.VerificationStatus;
@@ -161,6 +162,12 @@ private enum IsSatisfiableTestCase {
     SATISFIABLE("x > 5", "x = (?:[6-9]|[1-9]\\d+)"),
     DYNAMIC_ARITHMETIC("request == 1 && request + 2 == 3", "request = 1"),
     DYNAMIC_ARITHMETIC_UNARY("request == 1 && -request == -1", "request = 1"),
+    // The type checker narrows `dyn_var.orValue(1)` to int, but it may hold any value.
+    NARROWED_INT_NAN(
+        "dyn_var.orValue(1) != dyn_var.orValue(1)",
+        "dyn_var = optional\\.of\\(double\\(\"NaN\"\\)\\)"),
+    // Only checks that it's satisfiable: the range may be a list of strings.
+    NARROWED_LIST_RANGE("dyn_var.orValue([1]).exists(x, dyn(x) == 'a')", "dyn_var = "),
     GREATER_DOUBLE("d > 1.5", "d = "),
     LESS_EQUALS_UINT64("u <= 5u", "u = [0-5]u"),
     LESS_EQUALS_DOUBLE("d <= 5.5", "d = "),
@@ -704,6 +711,9 @@ private enum IsSatisfiableInconclusiveTestCase {
             + " && dyn_var != ([18446744073709551615u] + [])))"),
     // Well-known types are never messages, and other message types may have the field.
     DYN_MESSAGE_FIELD_OF_UNKNOWN_TYPE("type(dyn_var) != map && dyn_var.type_url == ''"),
+    // The type checker narrows the range to a list, but it may be a map.
+    NARROWED_LIST_RANGE_OF_MAP(
+        "type(dyn_var.orValue([1])) == map && dyn_var.orValue([1]).exists(x, true)"),
     MASKED_BY_BMC("int_list == [1, 2, 3, 4, 5, 6] ? int_list.exists(x, x == 42) : false"),
     MASKED_BY_BMC_ALL("int_list == [1, 2, 3, 4, 5, 6] ? int_list.all(x, x > 0) : false"),
     MASKED_BY_BMC_FILTER(
@@ -822,6 +832,15 @@ public void isSatisfiable_comprehensionZeroUnrollLimit_inconclusive() throws Exc
 
   private enum IsUnsatisfiableTestCase {
     DYN_MESSAGE_PRESENT_UNDECLARED_FIELD("dyn(test_all_types).unknown_field == 42"),
+    // `-` on `dyn_var.orValue(1)`, typed int, takes only the int overload, so a double errors.
+    NARROWED_INT_NEGATE_OVERLOAD(
+        "type(dyn_var.orValue(1)) == double && -dyn_var.orValue(1) == dyn(-1)"),
+    // The static type picks the overload of `_[_]` or `in`, which errors on the other kind.
+    NARROWED_LIST_INDEX_OF_MAP("dyn_var == optional.of({0: true}) && dyn_var.orValue([true])[0]"),
+    NARROWED_MAP_INDEX_OF_LIST("dyn_var == optional.of([true]) && dyn_var.orValue({0: true})[0]"),
+    NARROWED_MAP_IN_OF_LIST("dyn_var == optional.of([1]) && 1 in dyn_var.orValue({1: 2})"),
+    // A wrapper is null or an int.
+    NULLABLE_NULL_AND_ONE("nullable_int == null && nullable_int == 1"),
     REPEATED_FIELD_FROM_NON_LIST(
         "dyn_var == 42 && TestAllTypes{repeated_int64: dyn_var} == TestAllTypes{}"),
     UNSATISFIABLE("x > 5 && x < 3"),
@@ -1795,6 +1814,23 @@ private enum UnconditionalErrorTestCase {
         "dyn(TestAllTypes.NestedMessage{}).single_int64 == 0"
             + " || dyn(TestAllTypes.NestedMessage{}).single_int64 != 0"),
     MAP_MISSING_KEY("{'a': 1}['b'] == 0 || !({'a': 1}['b'] == 0)"),
+    OPTIONAL_SELECT_UNDECLARED_FIELD_OF_DYN_MESSAGE(
+        "dyn(TestAllTypes{}).?unknown_field.hasValue()"
+            + " || !dyn(TestAllTypes{}).?unknown_field.hasValue()"),
+    OPTIONAL_CHAINING_SELECT_UNDECLARED_FIELD(
+        "optional.of(dyn(TestAllTypes{})).unknown_field.hasValue()"
+            + " || !optional.of(dyn(TestAllTypes{})).unknown_field.hasValue()"),
+    // No overload indexes a list with a string, even an empty optional list.
+    OPTIONAL_LIST_INDEXED_BY_STRING(
+        "TestAllTypes{}.?repeated_int64[dyn('a')].hasValue()"
+            + " || !TestAllTypes{}.?repeated_int64[dyn('a')].hasValue()"),
+    OPTIONAL_LIST_OPTIONALLY_INDEXED_BY_STRING(
+        "TestAllTypes{}.?repeated_int64[?dyn('a')].hasValue()"
+            + " || !TestAllTypes{}.?repeated_int64[?dyn('a')].hasValue()"),
+    // A present optional's value must be a map or message to select from.
+    OPTIONAL_CHAINING_SELECT_FROM_NULL(
+        "{'null_key': dyn(null)}.?null_key.invalid.hasValue()"
+            + " || !{'null_key': dyn(null)}.?null_key.invalid.hasValue()"),
     COLLECTION_ERROR("{'a': 1 / 0} == {'a': 1 / 0}"),
     LIST_ERROR("[1 / 0] == [1 / 0]"),
     STRICT_LITERAL_ERROR("{'a': 1/0}.exists(k, k == 'a') == {'a': 1/0}.exists(k, k == 'a')"),
@@ -1871,7 +1907,12 @@ private enum MalformedAstTestCase {
         Operator.LESS,
         ImmutableList.of(
             CelExpr.newBuilder().setId(2).setConstant(CelConstant.ofValue(1L)).build()),
-        "expects 2 arguments, got 1");
+        "expects 2 arguments, got 1"),
+    OPTIONAL_SELECT(
+        Operator.OPTIONAL_SELECT,
+        ImmutableList.of(
+            CelExpr.newBuilder().setId(2).setConstant(CelConstant.ofValue(1L)).build()),
+        "expects an operand and a field name");
 
     final Operator operator;
     final ImmutableList<CelExpr> args;
@@ -1922,6 +1963,20 @@ public void verifyEquivalence_infinityConstants_notEquivalent() throws Exception
   }
 
   private enum IsAlwaysTrueViolationTestCase {
+    // The type checker narrows `dyn_var.orValue(...)` to the default's type.
+    NARROWED_MAP_LITERAL_EQUALITY(
+        "dyn_var == optional.of({'a': 1.0}) ? dyn_var.orValue(string_int_map) != {'a': 1} : true",
+        "Condition is not always true\\."),
+    // The type checker narrows `b ? test_all_types : null` to TestAllTypes.
+    NARROWED_NULL_FIELD(
+        "b || has((b ? test_all_types : null).single_int64)"
+            + " || !has((b ? test_all_types : null).single_int64)",
+        "Condition is not always true\\."),
+    NARROWED_MESSAGE_FIELD(
+        "dyn_var == optional.of(dyn_var2) && dyn_var2 == 42"
+            + " ? dyn_var.orValue(test_all_types).single_int64 == 0"
+            + " || dyn_var.orValue(test_all_types).single_int64 != 0 : true",
+        "Condition is not always true\\."),
     // `[NaN]` differs from itself.
     DYNAMIC_LIST_VARIABLE_EQUALITY("dyn_list == dyn_list", "dyn_list = \\[double\\(\"NaN\"\\)\\]"),
     DYNAMIC_MAP_VARIABLE_EQUALITY(
@@ -2301,8 +2356,8 @@ public void isAlwaysTrue_dynamicMapComprehensionNestedEquality_violated() throws
     // A looser timeout than the default: comparing a dyn map with a literal admits every numeric
     // representation of its keys and values, a state space that takes 5-25 s to explore remotely
     // (longer on GitHub runners).
-    // TODO: Restore 20 s once select on optionals is modeled (`request` may be
-    // `optional.none()`) and the slowdown since map literal key validation is recovered.
+    // TODO: Restore 20 s once the slowdown since map literal key validation is
+    // recovered.
     CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setTimeout(Duration.ofSeconds(60)));
 
     CelVerificationResult result = verifier.isAlwaysTrue(ast);
@@ -2811,6 +2866,30 @@ private enum EquivalenceTestCase {
     OPTIONAL_FIELD_SELECTION_MAP_COMPREHENSION(
         "{'a': 1, 'b': 2}.transformMap(k, v, v > 1, v).?b", "optional.of(2)"),
     OPTIONAL_FIELD_SELECTION_BINDER("cel.bind(m, {'a': 1}, m.?a)", "optional.of(1)"),
+    // Selecting from or indexing an optional does so optionally.
+    OPTIONAL_CHAINING_SELECT(
+        "optional.of({'c': {'index': 'goodbye'}}).c.index", "optional.of('goodbye')"),
+    OPTIONAL_CHAINING_SELECT_MISSING("optional.of({'c': {}}).c.missing", "optional.none()"),
+    OPTIONAL_CHAINING_SELECT_NONE("optional.none().c", "optional.none()"),
+    OPTIONAL_CHAINING_SELECT_OPTIONAL_VALUE(
+        "optional.of({'a': optional.of(1)}).a", "optional.of(optional.of(1))"),
+    OPTIONAL_CHAINING_HAS_PRESENT("has(optional.of({'c': 1}).c)", "true"),
+    OPTIONAL_CHAINING_HAS_ABSENT("has(optional.of({'c': 1}).d)", "false"),
+    OPTIONAL_CHAINING_HAS_NONE("has(optional.none().c)", "false"),
+    OPTIONAL_CHAINING_SELECT_PROTO3_ZERO(
+        "optional.of(TestAllTypes{single_int64: 0}).single_int64", "optional.none()"),
+    OPTIONAL_CHAINING_SELECT_UNSET_WRAPPER(
+        "optional.of(TestAllTypes{}).single_int64_wrapper", "optional.none()"),
+    OPTIONAL_CHAINING_INDEX("optional.of(['list-value'])[0]", "optional.of('list-value')"),
+    OPTIONAL_CHAINING_INDEX_MISSING("optional.of({'c': {}}).c['missing']", "optional.none()"),
+    OPTIONAL_CHAINING_INDEX_NONE("optional.none()[0]", "optional.none()"),
+    OPTIONAL_SELECT_THEN_INDEX(
+        "optional.of(TestAllTypes{repeated_string: ['foo']}).?repeated_string[0]",
+        "optional.of('foo')"),
+    OPTIONAL_CHAINING_DYN(
+        "dyn_var == optional.of({'a': [1]}) ? dyn_var.a[0] : optional.of(1)", "optional.of(1)"),
+    OPTIONAL_CHAINING_DYN_NONE(
+        "request == optional.none() ? request.l : optional.none()", "optional.none()"),
     JSON_VALUE_BOOL("google.protobuf.Value{bool_value: true}", "true"),
     JSON_VALUE_NUMBER("google.protobuf.Value{number_value: 1.0}", "1.0"),
     JSON_VALUE_NULL("google.protobuf.Value{null_value: 0}", "null"),
@@ -3927,6 +4006,21 @@ public void isAlwaysTrue_nanAndInfinityConstants_tautology(
     assertThat(VERIFIER.isAlwaysTrue(optimizedAst).status()).isEqualTo(VerificationStatus.VERIFIED);
   }
 
+  @Test
+  public void isSatisfiable_narrowedBlockIndex_satisfiable() throws Exception {
+    CelOptimizer optimizer =
+        CelOptimizerFactory.standardCelOptimizerBuilder(CEL)
+            .addAstOptimizers(SubexpressionOptimizer.getInstance())
+            .build();
+    // cel.@block([dyn_var.orValue(1)], @index0 != @index0), where @index0 is typed int.
+    CelAbstractSyntaxTree ast =
+        optimizer.optimize(CEL.compile("dyn_var.orValue(1) != dyn_var.orValue(1)").getAst());
+
+    CelVerificationResult result = VERIFIER_WITHOUT_ORACLE.isSatisfiable(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
+  }
+
   @Test
   public void translateFunctionCall_staticallyResolved_skipsDeadOverloads() throws Exception {
     CelFunctionDecl spyFuncDecl =