diff --git a/crates/ty_python_semantic/resources/mdtest/generics/legacy/variance.md b/crates/ty_python_semantic/resources/mdtest/generics/legacy/variance.md
index 4c2a7032ab..732a2a878a 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/legacy/variance.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/legacy/variance.md
@@ -171,6 +171,27 @@ static_assert(not is_equivalent_to(D[Any], C[Any]))
 static_assert(not is_equivalent_to(D[Any], C[Unknown]))
 ```
 
+## Bounded typevars in contravariant positions
+
+When a bounded typevar appears in a contravariant position, the actual type doesn't need to satisfy
+the bound directly. The typevar can be solved to the intersection of the actual type and the bound
+(e.g., `Never` when disjoint).
+
+```py
+from typing import Generic, TypeVar
+
+T = TypeVar("T", contravariant=True)
+T_int = TypeVar("T_int", bound=int)
+
+class Contra(Generic[T]): ...
+
+def f(x: Contra[T_int]) -> T_int:
+    raise NotImplementedError
+
+def _(x: Contra[str]):
+    reveal_type(f(x))  # revealed: Never
+```
+
 ## Invariance
 
 With an invariant typevar, only equivalent specializations of the generic class are subtypes of or
diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variance.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variance.md
index 77a41caa00..a04118988e 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variance.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variance.md
@@ -172,6 +172,23 @@ static_assert(not is_equivalent_to(D[Any], C[Any]))
 static_assert(not is_equivalent_to(D[Any], C[Unknown]))
 ```
 
+## Bounded typevars in contravariant positions
+
+When a bounded typevar appears in a contravariant position, the actual type doesn't need to satisfy
+the bound directly. The typevar can be solved to the intersection of the actual type and the bound
+(e.g., `Never` when disjoint).
+
+```py
+class Contra[T]:
+    def append(self, x: T): ...
+
+def f[T: int](x: Contra[T]) -> T:
+    raise NotImplementedError
+
+def _(x: Contra[str]):
+    reveal_type(f(x))  # revealed: Never
+```
+
 ## Invariance
 
 With an invariant typevar, only equivalent specializations of the generic class are subtypes of or
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index b92330f729..b467f08bbe 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1878,6 +1878,21 @@ impl<'db> SpecializationBuilder<'db> {
             {
                 match bound_typevar.typevar(self.db).bound_or_constraints(self.db) {
                     Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                        if polarity.is_contravariant() {
+                            // In a contravariant position, the formal type variable is a subtype of
+                            // the actual type (`T <: ty`). Since we also have the upper bound
+                            // constraint `T <: bound`, we just need to ensure that the intersection
+                            // of `ty` and `bound` is non-empty. Since `Never` is always a valid
+                            // intersection if the types are disjoint, we don't need to perform any
+                            // check here.
+                            self.add_type_mapping(
+                                bound_typevar,
+                                IntersectionType::from_elements(self.db, [bound, ty]),
+                                polarity,
+                                f,
+                            );
+                            return Ok(());
+                        }
                         if !ty
                             .when_assignable_to(self.db, bound, self.inferable)
                             .is_always_satisfied(self.db)
@@ -1899,10 +1914,16 @@ impl<'db> SpecializationBuilder<'db> {
                         }
 
                         for constraint in constraints.elements(self.db) {
-                            if ty
-                                .when_assignable_to(self.db, *constraint, self.inferable)
-                                .is_always_satisfied(self.db)
-                            {
+                            let is_satisfied = if polarity.is_contravariant() {
+                                constraint
+                                    .when_assignable_to(self.db, ty, self.inferable)
+                                    .is_always_satisfied(self.db)
+                            } else {
+                                ty.when_assignable_to(self.db, *constraint, self.inferable)
+                                    .is_always_satisfied(self.db)
+                            };
+
+                            if is_satisfied {
                                 self.add_type_mapping(bound_typevar, *constraint, polarity, f);
                                 return Ok(());
                             }
diff --git a/crates/ty_python_semantic/src/types/variance.rs b/crates/ty_python_semantic/src/types/variance.rs
index 5ec1d5a8ff..aa32bd6f17 100644
--- a/crates/ty_python_semantic/src/types/variance.rs
+++ b/crates/ty_python_semantic/src/types/variance.rs
@@ -92,6 +92,13 @@ impl TypeVarVariance {
             TypeVarVariance::Covariant | TypeVarVariance::Bivariant
         )
     }
+
+    pub(crate) const fn is_contravariant(self) -> bool {
+        matches!(
+            self,
+            TypeVarVariance::Contravariant | TypeVarVariance::Bivariant
+        )
+    }
 }
 
 impl std::iter::FromIterator<Self> for TypeVarVariance {