diff --git a/infer/src/nullsafe/AnnotatedField.ml b/infer/src/nullsafe/AnnotatedField.ml
index f08412951..721de14d0 100644
--- a/infer/src/nullsafe/AnnotatedField.ml
+++ b/infer/src/nullsafe/AnnotatedField.ml
@@ -56,12 +56,12 @@ let get tenv field_name class_typ =
          in
          let corrected_nullability =
            match nullability with
-           | AnnotatedNullability.DeclaredNonnull _ when is_enum_value ->
+           | AnnotatedNullability.UncheckedNonnull _ when is_enum_value ->
                (* Enum values are the special case - they can not be null. So we can strengten nullability.
                   Note that if it is nullable, we do NOT change nullability: in this case this is probably
                   not an enum value, but just a static field annotated as nullable.
                *)
-               AnnotatedNullability.Nonnull EnumValue
+               AnnotatedNullability.StrictNonnull EnumValue
            | _ ->
                nullability
          in
diff --git a/infer/src/nullsafe/AnnotatedNullability.ml b/infer/src/nullsafe/AnnotatedNullability.ml
index bd5a9c062..aa596a9d7 100644
--- a/infer/src/nullsafe/AnnotatedNullability.ml
+++ b/infer/src/nullsafe/AnnotatedNullability.ml
@@ -16,8 +16,8 @@ module F = Format
 
 type t =
   | Nullable of nullable_origin
-  | DeclaredNonnull of declared_nonnull_origin  (** See {!Nullability.t} for explanation *)
-  | Nonnull of nonnull_origin
+  | UncheckedNonnull of unchecked_nonnull_origin  (** See {!Nullability.t} for explanation *)
+  | StrictNonnull of strict_nonnull_origin
 [@@deriving compare]
 
 and nullable_origin =
@@ -31,7 +31,7 @@ and nullable_origin =
   | ModelledNullable  (** nullsafe knows it is nullable via its internal models *)
 [@@deriving compare]
 
-and declared_nonnull_origin =
+and unchecked_nonnull_origin =
   | AnnotatedNonnull
       (** The type is explicitly annotated as non nullable via one of nonnull annotations Nullsafe
           recognizes *)
@@ -39,7 +39,7 @@ and declared_nonnull_origin =
       (** Infer was run in mode where all not annotated (non local) types are treated as non
           nullable *)
 
-and nonnull_origin =
+and strict_nonnull_origin =
   | ModelledNonnull  (** nullsafe knows it is non-nullable via its internal models *)
   | StrictMode  (** under strict mode we consider non-null declarations to be trusted *)
   | PrimitiveType  (** Primitive types are non-nullable by language design *)
@@ -50,10 +50,10 @@ and nonnull_origin =
 let get_nullability = function
   | Nullable _ ->
       Nullability.Nullable
-  | DeclaredNonnull _ ->
-      Nullability.DeclaredNonnull
-  | Nonnull _ ->
-      Nullability.Nonnull
+  | UncheckedNonnull _ ->
+      Nullability.UncheckedNonnull
+  | StrictNonnull _ ->
+      Nullability.StrictNonnull
 
 
 let pp fmt t =
@@ -85,21 +85,21 @@ let pp fmt t =
   match t with
   | Nullable origin ->
       F.fprintf fmt "Nullable[%s]" (string_of_nullable_origin origin)
-  | DeclaredNonnull origin ->
-      F.fprintf fmt "DeclaredNonnull[%s]" (string_of_declared_nonnull_origin origin)
-  | Nonnull origin ->
-      F.fprintf fmt "Nonnull[%s]" (string_of_nonnull_origin origin)
+  | UncheckedNonnull origin ->
+      F.fprintf fmt "UncheckedNonnull[%s]" (string_of_declared_nonnull_origin origin)
+  | StrictNonnull origin ->
+      F.fprintf fmt "StrictNonnull[%s]" (string_of_nonnull_origin origin)
 
 
 let of_type_and_annotation ~is_strict_mode typ annotations =
-  if not (PatternMatch.type_is_class typ) then Nonnull PrimitiveType
+  if not (PatternMatch.type_is_class typ) then StrictNonnull PrimitiveType
   else if Annotations.ia_is_nullable annotations then
     let nullable_origin =
       if Annotations.ia_is_propagates_nullable annotations then AnnotatedPropagatesNullable
       else AnnotatedNullable
     in
     Nullable nullable_origin
-  else if is_strict_mode then Nonnull StrictMode
-  else if Annotations.ia_is_nonnull annotations then DeclaredNonnull AnnotatedNonnull
+  else if is_strict_mode then StrictNonnull StrictMode
+  else if Annotations.ia_is_nonnull annotations then UncheckedNonnull AnnotatedNonnull
     (* Currently, we treat not annotated types as nonnull *)
-  else DeclaredNonnull ImplicitlyNonnull
+  else UncheckedNonnull ImplicitlyNonnull
diff --git a/infer/src/nullsafe/AnnotatedNullability.mli b/infer/src/nullsafe/AnnotatedNullability.mli
index e3fc4db00..d9b372459 100644
--- a/infer/src/nullsafe/AnnotatedNullability.mli
+++ b/infer/src/nullsafe/AnnotatedNullability.mli
@@ -18,8 +18,8 @@ open! IStd
 
 type t =
   | Nullable of nullable_origin
-  | DeclaredNonnull of declared_nonnull_origin  (** See {!Nullability.t} for explanation *)
-  | Nonnull of nonnull_origin
+  | UncheckedNonnull of unchecked_nonnull_origin  (** See {!Nullability.t} for explanation *)
+  | StrictNonnull of strict_nonnull_origin
 [@@deriving compare]
 
 and nullable_origin =
@@ -33,7 +33,7 @@ and nullable_origin =
   | ModelledNullable  (** nullsafe knows it is nullable via its internal models *)
 [@@deriving compare]
 
-and declared_nonnull_origin =
+and unchecked_nonnull_origin =
   | AnnotatedNonnull
       (** The type is explicitly annotated as non nullable via one of nonnull annotations Nullsafe
           recognizes *)
@@ -41,7 +41,7 @@ and declared_nonnull_origin =
       (** Infer was run in mode where all not annotated (non local) types are treated as non
           nullable *)
 
-and nonnull_origin =
+and strict_nonnull_origin =
   | ModelledNonnull  (** nullsafe knows it is non-nullable via its internal models *)
   | StrictMode  (** under strict mode we consider non-null declarations to be trusted *)
   | PrimitiveType  (** Primitive types are non-nullable by language design *)
diff --git a/infer/src/nullsafe/AnnotatedSignature.ml b/infer/src/nullsafe/AnnotatedSignature.ml
index a6fe35951..db9463ac1 100644
--- a/infer/src/nullsafe/AnnotatedSignature.ml
+++ b/infer/src/nullsafe/AnnotatedSignature.ml
@@ -151,7 +151,7 @@ let mark_ia_nullability ia x = if x then mk_ia_nullable ia else ia
 let set_modelled_nullability_for_annotated_type annotated_type should_set_nullable =
   let nullability =
     if should_set_nullable then AnnotatedNullability.Nullable ModelledNullable
-    else AnnotatedNullability.Nonnull ModelledNonnull
+    else AnnotatedNullability.StrictNonnull ModelledNonnull
   in
   AnnotatedType.{annotated_type with nullability}
 
diff --git a/infer/src/nullsafe/AssignmentRule.ml b/infer/src/nullsafe/AssignmentRule.ml
index 61608654e..a9fe3c458 100644
--- a/infer/src/nullsafe/AssignmentRule.ml
+++ b/infer/src/nullsafe/AssignmentRule.ml
@@ -23,8 +23,8 @@ and function_info =
 
 let is_whitelisted_assignment ~is_strict_mode ~lhs ~rhs =
   match (is_strict_mode, lhs, rhs) with
-  | false, Nullability.Nonnull, Nullability.DeclaredNonnull ->
-      (* We allow DeclaredNonnull -> Nonnull conversion outside of strict mode for better adoption.
+  | false, Nullability.StrictNonnull, Nullability.UncheckedNonnull ->
+      (* We allow UncheckedNonnull -> StrictNonnull conversion outside of strict mode for better adoption.
          Otherwise using strictified classes in non-strict context becomes a pain because
          of extra warnings.
       *)
@@ -78,7 +78,7 @@ let bad_param_description
             "`null`"
         | Nullability.Nullable ->
             "nullable"
-        | Nullability.Nonnull | Nullability.DeclaredNonnull ->
+        | Nullability.StrictNonnull | Nullability.UncheckedNonnull ->
             Logging.die InternalError "Invariant violation: unexpected nullability"
       in
       Format.asprintf "%a is %s" MF.pp_monospaced actual_param_expression nullability_descr
@@ -131,7 +131,11 @@ let bad_param_description
 
 
 let is_declared_nonnull_to_nonnull ~lhs ~rhs =
-  match (lhs, rhs) with Nullability.Nonnull, Nullability.DeclaredNonnull -> true | _ -> false
+  match (lhs, rhs) with
+  | Nullability.StrictNonnull, Nullability.UncheckedNonnull ->
+      true
+  | _ ->
+      false
 
 
 let get_issue_type = function
@@ -171,7 +175,7 @@ let violation_description {is_strict_mode; lhs; rhs} ~assignment_location assign
                 "`null`"
             | Nullable ->
                 "a nullable"
-            | Nonnull | DeclaredNonnull ->
+            | StrictNonnull | UncheckedNonnull ->
                 Logging.die InternalError "Invariant violation: unexpected nullability"
           in
           Format.asprintf "%a is declared non-nullable but is assigned %s%s." MF.pp_monospaced
@@ -185,7 +189,7 @@ let violation_description {is_strict_mode; lhs; rhs} ~assignment_location assign
                 "`null`"
             | Nullable ->
                 "a nullable value"
-            | Nonnull | DeclaredNonnull ->
+            | StrictNonnull | UncheckedNonnull ->
                 Logging.die InternalError "Invariant violation: unexpected nullability"
           in
           Format.asprintf "%a: return type is declared non-nullable but the method returns %s%s."
diff --git a/infer/src/nullsafe/DereferenceRule.ml b/infer/src/nullsafe/DereferenceRule.ml
index 521fe281f..f82436297 100644
--- a/infer/src/nullsafe/DereferenceRule.ml
+++ b/infer/src/nullsafe/DereferenceRule.ml
@@ -19,9 +19,9 @@ let check ~is_strict_mode nullability =
   match nullability with
   | Nullability.Nullable | Nullability.Null ->
       Error {is_strict_mode; nullability}
-  | Nullability.DeclaredNonnull ->
+  | Nullability.UncheckedNonnull ->
       if is_strict_mode then Error {is_strict_mode; nullability} else Ok ()
-  | Nullability.Nonnull ->
+  | Nullability.StrictNonnull ->
       Ok ()
 
 
@@ -40,7 +40,7 @@ let violation_description {nullability} ~dereference_location dereference_type
     ~nullable_object_descr ~nullable_object_origin =
   let module MF = MarkupFormatter in
   match nullability with
-  | Nullability.DeclaredNonnull ->
+  | Nullability.UncheckedNonnull ->
       (* This can happen only in strict mode.
          This type of violation is more subtle than the normal case because, so it should be rendered in a special way *)
       ErrorRenderingUtils.get_strict_mode_violation_issue ~bad_usage_location:dereference_location
@@ -91,7 +91,7 @@ let violation_description {nullability} ~dereference_location dereference_type
         | Nullability.Nullable ->
             Format.sprintf "%s is nullable and is not locally checked for null when %s%s"
               what_is_dereferred_str action_descr suffix
-        | Nullability.DeclaredNonnull | Nullability.Nonnull ->
+        | Nullability.UncheckedNonnull | Nullability.StrictNonnull ->
             Logging.die InternalError "Invariant violation: unexpected nullability"
       in
       (description, IssueType.eradicate_nullable_dereference, dereference_location)
diff --git a/infer/src/nullsafe/ErrorRenderingUtils.mli b/infer/src/nullsafe/ErrorRenderingUtils.mli
index ba69791f5..f504de6bf 100644
--- a/infer/src/nullsafe/ErrorRenderingUtils.mli
+++ b/infer/src/nullsafe/ErrorRenderingUtils.mli
@@ -15,7 +15,7 @@ val is_object_nullability_self_explanatory : object_expression:string -> TypeOri
 
 val get_strict_mode_violation_issue :
   bad_usage_location:Location.t -> TypeOrigin.t -> string * IssueType.t * Location.t
-(** Situation when we tried to use DeclaredNonnull as Nonnull. This is disallowed only in strict
-    mode. Returns a tuple (error message, issue type, error location). NOTE: Location of the error
-    will be NOT in the place when the value is used (that is [bad_usage_location]), but where the
-    value is first obtained from. *)
+(** Situation when we tried to use UncheckedNonnull as StrictNonnull. This is disallowed only in
+    strict mode. Returns a tuple (error message, issue type, error location). NOTE: Location of the
+    error will be NOT in the place when the value is used (that is [bad_usage_location]), but where
+    the value is first obtained from. *)
diff --git a/infer/src/nullsafe/InferredNullability.ml b/infer/src/nullsafe/InferredNullability.ml
index 9f141a71e..136b54b44 100644
--- a/infer/src/nullsafe/InferredNullability.ml
+++ b/infer/src/nullsafe/InferredNullability.ml
@@ -14,7 +14,7 @@ let create origin = {nullability= TypeOrigin.get_nullability origin; origin}
 let get_nullability {nullability} = nullability
 
 let is_nonnull_or_declared_nonnull {nullability} =
-  match nullability with Nonnull | DeclaredNonnull -> true | _ -> false
+  match nullability with StrictNonnull | UncheckedNonnull -> true | _ -> false
 
 
 let to_string {nullability} = Printf.sprintf "[%s]" (Nullability.to_string nullability)
diff --git a/infer/src/nullsafe/InheritanceRule.ml b/infer/src/nullsafe/InheritanceRule.ml
index 38f0e205c..d23d518e4 100644
--- a/infer/src/nullsafe/InheritanceRule.ml
+++ b/infer/src/nullsafe/InheritanceRule.ml
@@ -13,7 +13,7 @@ type type_role = Param | Ret
 
 let is_whitelisted_violation ~subtype ~supertype =
   match (subtype, supertype) with
-  | Nullability.DeclaredNonnull, Nullability.Nonnull ->
+  | Nullability.UncheckedNonnull, Nullability.StrictNonnull ->
       (* It is a violation that we are currently willing to ignore because
          it is hard to obey in practice.
          It might lead to unsoundness issues, so this might be reconsidered.
diff --git a/infer/src/nullsafe/Nullability.ml b/infer/src/nullsafe/Nullability.ml
index a6dd4c616..7c63ec891 100644
--- a/infer/src/nullsafe/Nullability.ml
+++ b/infer/src/nullsafe/Nullability.ml
@@ -10,14 +10,21 @@ open! IStd
 type t =
   | Null  (** The only possible value for that type is null *)
   | Nullable  (** No guarantees on the nullability *)
-  | DeclaredNonnull
+  | UncheckedNonnull
       (** The type comes from a signature that is annotated (explicitly or implicitly according to
-          conventions) as non-nullable. Hovewer, it might still contain null since the truthfullness
+          conventions) as non-nullable. However, it might still contain null since the truthfulness
           of the declaration was not checked. *)
-  | Nonnull
-      (** We believe that this value can not be null. If it is not the case, this is an unsoundness
-          issue for Nullsafe, and we aim to minimize number of such issues occuring in real-world
-          programs. *)
+  | StrictNonnull
+      (** Non-nullable value with the highest degree of certainty, because it is either:
+
+          - a non-null literal,
+          - an expression that semantically cannot be null,
+          - comes from internal code checked under strict mode,
+          - comes from a third-party method with an appropriate built-in model or user-defined
+            nullability signature.
+
+          The latter two are potential sources of unsoundness issues for nullsafe, but we need to
+          strike the balance between the strictness of analysis, convenience, and real-world risk. *)
 [@@deriving compare, equal]
 
 let top = Nullable
@@ -30,10 +37,10 @@ let join x y =
       Nullable
   | Nullable, _ | _, Nullable ->
       Nullable
-  | DeclaredNonnull, _ | _, DeclaredNonnull ->
-      DeclaredNonnull
-  | Nonnull, Nonnull ->
-      Nonnull
+  | UncheckedNonnull, _ | _, UncheckedNonnull ->
+      UncheckedNonnull
+  | StrictNonnull, StrictNonnull ->
+      StrictNonnull
 
 
 let is_subtype ~subtype ~supertype = equal (join subtype supertype) supertype
@@ -43,7 +50,7 @@ let to_string = function
       "Null"
   | Nullable ->
       "Nullable"
-  | DeclaredNonnull ->
-      "DeclaredNonnull"
-  | Nonnull ->
-      "Nonnull"
+  | UncheckedNonnull ->
+      "UncheckedNonnull"
+  | StrictNonnull ->
+      "StrictNonnull"
diff --git a/infer/src/nullsafe/Nullability.mli b/infer/src/nullsafe/Nullability.mli
index 84816c1e6..bdcbe45fc 100644
--- a/infer/src/nullsafe/Nullability.mli
+++ b/infer/src/nullsafe/Nullability.mli
@@ -18,13 +18,15 @@ open! IStd
 type t =
   | Null  (** The only possible value for that type is null *)
   | Nullable  (** No guarantees on the nullability *)
-  | DeclaredNonnull
+  | UncheckedNonnull
       (** The type comes from a signature that is annotated (explicitly or implicitly according to
           conventions) as non-nullable. Hovewer, it might still contain null since the truthfullness
           of the declaration was not checked. *)
-  | Nonnull
-      (** We believe that this value can not be null. If it is not the case, this is an unsoundness
-          issue for Nullsafe, and we aim to minimize number of such issues occuring in real-world
+  | StrictNonnull
+      (** We believe that this value can not be null because it is either a non-null literal, an
+          expression that semantically cannot be null, or a non-null value that should not be null
+          according to typechecking rules. If the latter is not the case, this is an unsoundness
+          issue for nullsafe, and we aim to minimize number of such issues occuring in real-world
           programs. *)
 [@@deriving compare, equal]
 
diff --git a/infer/src/nullsafe/OverAnnotatedRule.ml b/infer/src/nullsafe/OverAnnotatedRule.ml
index 9259b6ae7..e9b56fa96 100644
--- a/infer/src/nullsafe/OverAnnotatedRule.ml
+++ b/infer/src/nullsafe/OverAnnotatedRule.ml
@@ -11,9 +11,10 @@ type violation = {declared_nullability: Nullability.t; can_be_narrowed_to: Nulla
 
 let check ~what ~by_rhs_upper_bound =
   match (what, by_rhs_upper_bound) with
-  | Nullability.Nullable, Nullability.Nonnull | Nullability.Nullable, Nullability.DeclaredNonnull ->
+  | Nullability.Nullable, Nullability.StrictNonnull
+  | Nullability.Nullable, Nullability.UncheckedNonnull ->
       Error {declared_nullability= what; can_be_narrowed_to= by_rhs_upper_bound}
-  | Nullability.Null, Nullability.Nonnull | Nullability.Null, Nullability.DeclaredNonnull ->
+  | Nullability.Null, Nullability.StrictNonnull | Nullability.Null, Nullability.UncheckedNonnull ->
       (* Null, Nonnull pais is an edge case that we don't expect to arise in practice for two reasons:
          1. The only way to declare something as Null is to declare it is java.lang.Void, but nullsafe
          does not know about it just yet.
diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml
index a142a68a2..b59d12ea4 100644
--- a/infer/src/nullsafe/eradicateChecks.ml
+++ b/infer/src/nullsafe/eradicateChecks.ml
@@ -183,9 +183,9 @@ let is_declared_nonnull AnnotatedField.{annotated_type} =
   match annotated_type.nullability with
   | AnnotatedNullability.Nullable _ ->
       false
-  | AnnotatedNullability.DeclaredNonnull _ ->
+  | AnnotatedNullability.UncheckedNonnull _ ->
       true
-  | AnnotatedNullability.Nonnull _ ->
+  | AnnotatedNullability.StrictNonnull _ ->
       true
 
 
@@ -234,7 +234,7 @@ let get_nullability_upper_bound_for_typestate proc_name field_name typestate =
  *)
 let get_nullability_upper_bound field_name typestate_list =
   (* Join upper bounds for all typestates in the list *)
-  List.fold typestate_list ~init:Nullability.Nonnull ~f:(fun acc (proc_name, typestate) ->
+  List.fold typestate_list ~init:Nullability.StrictNonnull ~f:(fun acc (proc_name, typestate) ->
       Nullability.join acc
         (get_nullability_upper_bound_for_typestate proc_name field_name typestate) )
 
diff --git a/infer/src/nullsafe/typeOrigin.ml b/infer/src/nullsafe/typeOrigin.ml
index ddf018551..0ec1037f2 100644
--- a/infer/src/nullsafe/typeOrigin.ml
+++ b/infer/src/nullsafe/typeOrigin.ml
@@ -63,7 +63,7 @@ let get_nullability = function
   | ArrayAccess
   | OptimisticFallback (* non-null is the most optimistic type *)
   | Undef (* This is a very special case, assigning non-null is a technical trick *) ->
-      Nullability.Nonnull
+      Nullability.StrictNonnull
   | Field {field_type= {nullability}} ->
       AnnotatedNullability.get_nullability nullability
   | MethodParameter {param_annotated_type= {nullability}} ->
@@ -116,7 +116,7 @@ let get_method_ret_description pname call_loc
     match nullability with
     | AnnotatedNullability.Nullable _ ->
         "nullable"
-    | AnnotatedNullability.DeclaredNonnull _ | AnnotatedNullability.Nonnull _ ->
+    | AnnotatedNullability.UncheckedNonnull _ | AnnotatedNullability.StrictNonnull _ ->
         "non-nullable"
   in
   let model_info =