diff --git a/crates/ty_python_semantic/resources/mdtest/call/builtins.md b/crates/ty_python_semantic/resources/mdtest/call/builtins.md
index c9bb662177..b7415de8b4 100644
--- a/crates/ty_python_semantic/resources/mdtest/call/builtins.md
+++ b/crates/ty_python_semantic/resources/mdtest/call/builtins.md
@@ -105,3 +105,59 @@ str("Müsli", "utf-8")
 # error: [invalid-argument-type] "Argument to class `str` is incorrect: Expected `str`, found `Literal[b"utf-8"]`"
 str(b"M\xc3\xbcsli", b"utf-8")
 ```
+
+## Calls to `isinstance`
+
+We infer `Literal[True]` for a limited set of cases where we can be sure that the answer is correct,
+but fall back to `bool` otherwise.
+
+```py
+from enum import Enum
+from types import FunctionType
+
+class Answer(Enum):
+    NO = 0
+    YES = 1
+
+reveal_type(isinstance(True, bool))  # revealed: Literal[True]
+reveal_type(isinstance(True, int))  # revealed: Literal[True]
+reveal_type(isinstance(True, object))  # revealed: Literal[True]
+reveal_type(isinstance("", str))  # revealed: Literal[True]
+reveal_type(isinstance(1, int))  # revealed: Literal[True]
+reveal_type(isinstance(b"", bytes))  # revealed: Literal[True]
+reveal_type(isinstance(Answer.NO, Answer))  # revealed: Literal[True]
+
+reveal_type(isinstance((1, 2), tuple))  # revealed: Literal[True]
+
+def f(): ...
+
+reveal_type(isinstance(f, FunctionType))  # revealed: Literal[True]
+
+reveal_type(isinstance("", int))  # revealed: bool
+
+class A: ...
+class SubclassOfA(A): ...
+class B: ...
+
+reveal_type(isinstance(A, type))  # revealed: Literal[True]
+
+a = A()
+
+reveal_type(isinstance(a, A))  # revealed: Literal[True]
+reveal_type(isinstance(a, object))  # revealed: Literal[True]
+reveal_type(isinstance(a, SubclassOfA))  # revealed: bool
+reveal_type(isinstance(a, B))  # revealed: bool
+
+s = SubclassOfA()
+reveal_type(isinstance(s, SubclassOfA))  # revealed: Literal[True]
+reveal_type(isinstance(s, A))  # revealed: Literal[True]
+
+def _(x: A | B):
+    reveal_type(isinstance(x, A))  # revealed: bool
+
+    if isinstance(x, A):
+        pass
+    else:
+        reveal_type(x)  # revealed: B & ~A
+        reveal_type(isinstance(x, B))  # revealed: Literal[True]
+```
diff --git a/crates/ty_python_semantic/resources/mdtest/exhaustiveness_checking.md b/crates/ty_python_semantic/resources/mdtest/exhaustiveness_checking.md
new file mode 100644
index 0000000000..9ecc26be0e
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/exhaustiveness_checking.md
@@ -0,0 +1,238 @@
+# Exhaustiveness checking
+
+```toml
+[environment]
+python-version = "3.11"
+```
+
+## Checks on literals
+
+```py
+from typing import Literal, assert_never
+
+def if_else_exhaustive(x: Literal[0, 1, "a"]):
+    if x == 0:
+        pass
+    elif x == 1:
+        pass
+    elif x == "a":
+        pass
+    else:
+        no_diagnostic_here
+
+        assert_never(x)
+
+def if_else_exhaustive_no_assertion(x: Literal[0, 1, "a"]) -> int:
+    if x == 0:
+        return 0
+    elif x == 1:
+        return 1
+    elif x == "a":
+        return 2
+
+def if_else_non_exhaustive(x: Literal[0, 1, "a"]):
+    if x == 0:
+        pass
+    elif x == "a":
+        pass
+    else:
+        this_should_be_an_error  # error: [unresolved-reference]
+
+        # this diagnostic is correct: the inferred type of `x` is `Literal[1]`
+        assert_never(x)  # error: [type-assertion-failure]
+
+def match_exhaustive(x: Literal[0, 1, "a"]):
+    match x:
+        case 0:
+            pass
+        case 1:
+            pass
+        case "a":
+            pass
+        case _:
+            # TODO: this should not be an error
+            no_diagnostic_here  # error: [unresolved-reference]
+
+            assert_never(x)
+
+# TODO: there should be no error here
+# error: [invalid-return-type] "Function can implicitly return `None`, which is not assignable to return type `int`"
+def match_exhaustive_no_assertion(x: Literal[0, 1, "a"]) -> int:
+    match x:
+        case 0:
+            return 0
+        case 1:
+            return 1
+        case "a":
+            return 2
+
+def match_non_exhaustive(x: Literal[0, 1, "a"]):
+    match x:
+        case 0:
+            pass
+        case "a":
+            pass
+        case _:
+            this_should_be_an_error  # error: [unresolved-reference]
+
+            # this diagnostic is correct: the inferred type of `x` is `Literal[1]`
+            assert_never(x)  # error: [type-assertion-failure]
+```
+
+## Checks on enum literals
+
+```py
+from enum import Enum
+from typing import assert_never
+
+class Color(Enum):
+    RED = 1
+    GREEN = 2
+    BLUE = 3
+
+def if_else_exhaustive(x: Color):
+    if x == Color.RED:
+        pass
+    elif x == Color.GREEN:
+        pass
+    elif x == Color.BLUE:
+        pass
+    else:
+        no_diagnostic_here
+
+        assert_never(x)
+
+def if_else_exhaustive_no_assertion(x: Color) -> int:
+    if x == Color.RED:
+        return 1
+    elif x == Color.GREEN:
+        return 2
+    elif x == Color.BLUE:
+        return 3
+
+def if_else_non_exhaustive(x: Color):
+    if x == Color.RED:
+        pass
+    elif x == Color.BLUE:
+        pass
+    else:
+        this_should_be_an_error  # error: [unresolved-reference]
+
+        # this diagnostic is correct: inferred type of `x` is `Literal[Color.GREEN]`
+        assert_never(x)  # error: [type-assertion-failure]
+
+def match_exhaustive(x: Color):
+    match x:
+        case Color.RED:
+            pass
+        case Color.GREEN:
+            pass
+        case Color.BLUE:
+            pass
+        case _:
+            # TODO: this should not be an error
+            no_diagnostic_here  # error: [unresolved-reference]
+
+            assert_never(x)
+
+# TODO: there should be no error here
+# error: [invalid-return-type] "Function can implicitly return `None`, which is not assignable to return type `int`"
+def match_exhaustive_no_assertion(x: Color) -> int:
+    match x:
+        case Color.RED:
+            return 1
+        case Color.GREEN:
+            return 2
+        case Color.BLUE:
+            return 3
+
+def match_non_exhaustive(x: Color):
+    match x:
+        case Color.RED:
+            pass
+        case Color.BLUE:
+            pass
+        case _:
+            this_should_be_an_error  # error: [unresolved-reference]
+
+            # this diagnostic is correct: inferred type of `x` is `Literal[Color.GREEN]`
+            assert_never(x)  # error: [type-assertion-failure]
+```
+
+## `isinstance` checks
+
+```py
+from typing import assert_never
+
+class A: ...
+class B: ...
+class C: ...
+
+def if_else_exhaustive(x: A | B | C):
+    if isinstance(x, A):
+        pass
+    elif isinstance(x, B):
+        pass
+    elif isinstance(x, C):
+        pass
+    else:
+        no_diagnostic_here
+
+        assert_never(x)
+
+def if_else_exhaustive_no_assertion(x: A | B | C) -> int:
+    if isinstance(x, A):
+        return 0
+    elif isinstance(x, B):
+        return 1
+    elif isinstance(x, C):
+        return 2
+
+def if_else_non_exhaustive(x: A | B | C):
+    if isinstance(x, A):
+        pass
+    elif isinstance(x, C):
+        pass
+    else:
+        this_should_be_an_error  # error: [unresolved-reference]
+
+        # this diagnostic is correct: the inferred type of `x` is `B & ~A & ~C`
+        assert_never(x)  # error: [type-assertion-failure]
+
+def match_exhaustive(x: A | B | C):
+    match x:
+        case A():
+            pass
+        case B():
+            pass
+        case C():
+            pass
+        case _:
+            # TODO: this should not be an error
+            no_diagnostic_here  # error: [unresolved-reference]
+
+            assert_never(x)
+
+# TODO: there should be no error here
+# error: [invalid-return-type] "Function can implicitly return `None`, which is not assignable to return type `int`"
+def match_exhaustive_no_assertion(x: A | B | C) -> int:
+    match x:
+        case A():
+            return 0
+        case B():
+            return 1
+        case C():
+            return 2
+
+def match_non_exhaustive(x: A | B | C):
+    match x:
+        case A():
+            pass
+        case C():
+            pass
+        case _:
+            this_should_be_an_error  # error: [unresolved-reference]
+
+            # this diagnostic is correct: the inferred type of `x` is `B & ~A & ~C`
+            assert_never(x)  # error: [type-assertion-failure]
+```
diff --git a/crates/ty_python_semantic/src/types/function.rs b/crates/ty_python_semantic/src/types/function.rs
index be41d5820a..5934b29634 100644
--- a/crates/ty_python_semantic/src/types/function.rs
+++ b/crates/ty_python_semantic/src/types/function.rs
@@ -76,8 +76,9 @@ use crate::types::narrow::ClassInfoConstraintFunction;
 use crate::types::signatures::{CallableSignature, Signature};
 use crate::types::visitor::any_over_type;
 use crate::types::{
-    BoundMethodType, CallableType, DeprecatedInstance, DynamicType, KnownClass, Type, TypeMapping,
-    TypeRelation, TypeTransformer, TypeVarInstance, UnionBuilder, walk_type_mapping,
+    BoundMethodType, CallableType, ClassLiteral, ClassType, DeprecatedInstance, DynamicType,
+    KnownClass, Truthiness, Type, TypeMapping, TypeRelation, TypeTransformer, TypeVarInstance,
+    UnionBuilder, walk_type_mapping,
 };
 use crate::{Db, FxOrderSet, ModuleName, resolve_module};
 
@@ -882,6 +883,96 @@ impl<'db> FunctionType<'db> {
     }
 }
 
+/// Evaluate an `isinstance` call. Return `Truthiness::AlwaysTrue` if we can definitely infer that
+/// this will return `True` at runtime, `Truthiness::AlwaysFalse` if we can definitely infer
+/// that this will return `False` at runtime, or `Truthiness::Ambiguous` if we should infer `bool`
+/// instead.
+fn is_instance_truthiness<'db>(
+    db: &'db dyn Db,
+    ty: Type<'db>,
+    class: ClassLiteral<'db>,
+) -> Truthiness {
+    let is_instance = |ty: &Type<'_>| {
+        if let Type::NominalInstance(instance) = ty {
+            if instance
+                .class
+                .is_subclass_of(db, ClassType::NonGeneric(class))
+            {
+                return true;
+            }
+        }
+        false
+    };
+
+    let always_true_if = |test: bool| {
+        if test {
+            Truthiness::AlwaysTrue
+        } else {
+            Truthiness::Ambiguous
+        }
+    };
+
+    match ty {
+        Type::Union(..) => {
+            // We do not handle unions specifically here, because something like `A | SubclassOfA` would
+            // have been simplified to `A` anyway
+            Truthiness::Ambiguous
+        }
+        Type::Intersection(intersection) => always_true_if(
+            intersection
+                .positive(db)
+                .iter()
+                .any(|element| is_instance_truthiness(db, *element, class).is_always_true()),
+        ),
+
+        Type::NominalInstance(..) => always_true_if(is_instance(&ty)),
+
+        Type::BooleanLiteral(..)
+        | Type::BytesLiteral(..)
+        | Type::IntLiteral(..)
+        | Type::StringLiteral(..)
+        | Type::LiteralString
+        | Type::ModuleLiteral(..)
+        | Type::EnumLiteral(..) => always_true_if(
+            ty.literal_fallback_instance(db)
+                .as_ref()
+                .is_some_and(is_instance),
+        ),
+
+        Type::Tuple(..) => always_true_if(class.is_known(db, KnownClass::Tuple)),
+
+        Type::FunctionLiteral(..) => {
+            always_true_if(is_instance(&KnownClass::FunctionType.to_instance(db)))
+        }
+
+        Type::ClassLiteral(..) => always_true_if(is_instance(&KnownClass::Type.to_instance(db))),
+
+        Type::BoundMethod(..)
+        | Type::MethodWrapper(..)
+        | Type::WrapperDescriptor(..)
+        | Type::DataclassDecorator(..)
+        | Type::DataclassTransformer(..)
+        | Type::GenericAlias(..)
+        | Type::SubclassOf(..)
+        | Type::ProtocolInstance(..)
+        | Type::SpecialForm(..)
+        | Type::KnownInstance(..)
+        | Type::PropertyInstance(..)
+        | Type::AlwaysTruthy
+        | Type::AlwaysFalsy
+        | Type::TypeVar(..)
+        | Type::BoundSuper(..)
+        | Type::TypeIs(..)
+        | Type::Callable(..)
+        | Type::Dynamic(..)
+        | Type::Never => {
+            // We could probably try to infer more precise types in some of these cases, but it's unclear
+            // if it's worth the effort.
+            Truthiness::Ambiguous
+        }
+    }
+}
+
 fn signature_cycle_recover<'db>(
     _db: &'db dyn Db,
     _value: &CallableSignature<'db>,
@@ -1228,21 +1319,26 @@ impl KnownFunction {
             }
 
             KnownFunction::IsInstance | KnownFunction::IsSubclass => {
-                let [_, Some(Type::ClassLiteral(class))] = parameter_types else {
+                let [Some(first_arg), Some(Type::ClassLiteral(class))] = parameter_types else {
                     return;
                 };
-                let Some(protocol_class) = class.into_protocol_class(db) else {
-                    return;
-                };
-                if protocol_class.is_runtime_checkable(db) {
-                    return;
+
+                if let Some(protocol_class) = class.into_protocol_class(db) {
+                    if !protocol_class.is_runtime_checkable(db) {
+                        report_runtime_check_against_non_runtime_checkable_protocol(
+                            context,
+                            call_expression,
+                            protocol_class,
+                            self,
+                        );
+                    }
+                }
+
+                if self == KnownFunction::IsInstance {
+                    overload.set_return_type(
+                        is_instance_truthiness(db, *first_arg, *class).into_type(db),
+                    );
                 }
-                report_runtime_check_against_non_runtime_checkable_protocol(
-                    context,
-                    call_expression,
-                    protocol_class,
-                    self,
-                );
             }
 
             known @ (KnownFunction::DunderImport | KnownFunction::ImportModule) => {