diff --git a/Cargo.lock b/Cargo.lock
index c66d588320f19..2381d35eadd82 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -413,7 +413,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -693,7 +693,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "strsim 0.10.0",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -704,7 +704,7 @@ checksum = "a668eda54683121533a393014d8692171709ff57a7d61f187b6e782719f8933f"
 dependencies = [
  "darling_core",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -774,7 +774,7 @@ dependencies = [
  "glob",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -826,7 +826,7 @@ checksum = "97369cbbc041bc366949bc74d34658d6cda5621039731c6310521892a3a20ae0"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -875,6 +875,16 @@ dependencies = [
  "regex",
 ]
 
+[[package]]
+name = "env_logger"
+version = "0.8.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a19187fea3ac7e84da7dacf48de0c45d63c6a76f9490dae389aead16c243fce3"
+dependencies = [
+ "log",
+ "regex",
+]
+
 [[package]]
 name = "env_logger"
 version = "0.11.5"
@@ -1246,7 +1256,7 @@ checksum = "1ec89e9337638ecdc08744df490b221a7399bf8d164eb52a665454e60e075ad6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -1420,7 +1430,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -1547,7 +1557,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a2ae40017ac09cd2c6a53504cb3c871c7f2b41466eac5bc66ba63f39073b467b"
 dependencies = [
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -2013,7 +2023,7 @@ dependencies = [
  "pest_meta",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -2173,6 +2183,28 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "quickcheck"
+version = "1.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "588f6378e4dd99458b60ec275b4477add41ce4fa9f64dcba6f15adccb19b50d6"
+dependencies = [
+ "env_logger 0.8.4",
+ "log",
+ "rand",
+]
+
+[[package]]
+name = "quickcheck_macros"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b22a693222d716a9587786f37ac3f6b4faedb5b80c23914e7303ff5a1d8016e9"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+]
+
 [[package]]
 name = "quote"
 version = "1.0.37"
@@ -2273,6 +2305,8 @@ dependencies = [
  "itertools 0.13.0",
  "memchr",
  "ordermap",
+ "quickcheck",
+ "quickcheck_macros",
  "red_knot_test",
  "red_knot_vendored",
  "ruff_db",
@@ -2777,7 +2811,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "ruff_python_trivia",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -2918,7 +2952,7 @@ dependencies = [
 name = "ruff_python_resolver"
 version = "0.0.0"
 dependencies = [
- "env_logger",
+ "env_logger 0.11.5",
  "insta",
  "log",
  "tempfile",
@@ -3197,7 +3231,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
  "synstructure",
 ]
 
@@ -3231,7 +3265,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "serde_derive_internals",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3280,7 +3314,7 @@ checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3291,7 +3325,7 @@ checksum = "330f01ce65a3a5fe59a60c82f3c9a024b573b8a6e875bd233fe5f934e71d54e3"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3314,7 +3348,7 @@ checksum = "6c64451ba24fc7a6a2d60fc75dd9c83c90903b19028d4eff35e88fc1e86564e9"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3355,7 +3389,7 @@ dependencies = [
  "darling",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3463,7 +3497,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustversion",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3472,6 +3506,17 @@ version = "2.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "81cdd64d312baedb58e21336b31bc043b77e01cc99033ce76ef539f78e965ebc"
 
+[[package]]
+name = "syn"
+version = "1.0.109"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "syn"
 version = "2.0.90"
@@ -3491,7 +3536,7 @@ checksum = "c8af7666ab7b6390ab78131fb5b0fce11d6b7a6951602017c35fa82800708971"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3554,7 +3599,7 @@ dependencies = [
  "cfg-if",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3565,7 +3610,7 @@ checksum = "5c89e72a01ed4c579669add59014b9a524d609c0c88c6a585ce37485879f6ffb"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
  "test-case-core",
 ]
 
@@ -3595,7 +3640,7 @@ checksum = "b607164372e89797d78b8e23a6d67d5d1038c1c65efd52e1389ef8b77caba2a6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3606,7 +3651,7 @@ checksum = "f077553d607adc1caf65430528a576c757a71ed73944b66ebb58ef2bbd243568"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -3728,7 +3773,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -4001,7 +4046,7 @@ checksum = "6b91f57fe13a38d0ce9e28a03463d8d3c2468ed03d75375110ec71d93b449a08"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -4096,7 +4141,7 @@ dependencies = [
  "once_cell",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
  "wasm-bindgen-shared",
 ]
 
@@ -4131,7 +4176,7 @@ checksum = "98c9ae5a76e46f4deecd0f0255cc223cfa18dc9b261213b8aa0c7b36f61b3f1d"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
  "wasm-bindgen-backend",
  "wasm-bindgen-shared",
 ]
@@ -4165,7 +4210,7 @@ checksum = "222ebde6ea87fbfa6bdd2e9f1fd8a91d60aee5db68792632176c4e16a74fc7d8"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -4468,7 +4513,7 @@ checksum = "28cc31741b18cb6f1d5ff12f5b7523e3d6eb0852bbbad19d73905511d9849b95"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
  "synstructure",
 ]
 
@@ -4489,7 +4534,7 @@ checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
@@ -4509,7 +4554,7 @@ checksum = "0ea7b4a3637ea8669cedf0f1fd5c286a17f3de97b8dd5a70a6c167a1730e63a5"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
  "synstructure",
 ]
 
@@ -4538,7 +4583,7 @@ checksum = "6eafa6dfb17584ea3e2bd6e76e0cc15ad7af12b09abdd1ca55961bed9b1063c6"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.90",
 ]
 
 [[package]]
diff --git a/crates/red_knot_python_semantic/Cargo.toml b/crates/red_knot_python_semantic/Cargo.toml
index af735f99e15b9..8a595973f745d 100644
--- a/crates/red_knot_python_semantic/Cargo.toml
+++ b/crates/red_knot_python_semantic/Cargo.toml
@@ -49,6 +49,8 @@ anyhow = { workspace = true }
 dir-test = { workspace = true }
 insta = { workspace = true }
 tempfile = { workspace = true }
+quickcheck = "1.0.3"
+quickcheck_macros = "1.0.0"
 
 [lints]
 workspace = true
diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index 695a779a849de..3eeec1cb4782d 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -3058,8 +3058,8 @@ pub(crate) mod tests {
 
     /// A test representation of a type that can be transformed unambiguously into a real Type,
     /// given a db.
-    #[derive(Debug, Clone)]
-    enum Ty {
+    #[derive(Debug, Clone, PartialEq)]
+    pub(crate) enum Ty {
         Never,
         Unknown,
         None,
@@ -3083,7 +3083,7 @@ pub(crate) mod tests {
     }
 
     impl Ty {
-        fn into_type(self, db: &TestDb) -> Type<'_> {
+        pub(crate) fn into_type(self, db: &TestDb) -> Type<'_> {
             match self {
                 Ty::Never => Type::Never,
                 Ty::Unknown => Type::Unknown,
@@ -3772,3 +3772,215 @@ pub(crate) mod tests {
             .is_todo());
     }
 }
+
+#[cfg(test)]
+mod property_tests {
+    use std::sync::{Arc, Mutex, MutexGuard, OnceLock};
+
+    use crate::types::Type;
+
+    use super::tests::{setup_db, Ty};
+    use crate::db::tests::TestDb;
+    use crate::Db;
+    use quickcheck::{Arbitrary, Gen};
+    use quickcheck_macros::quickcheck;
+
+    fn arbitrary_core_type(g: &mut Gen) -> Ty {
+        let int_lit = Ty::IntLiteral(*g.choose(&[-2, -1, 0, 1, 2]).unwrap());
+        let bool_lit = Ty::BooleanLiteral(bool::arbitrary(g));
+        g.choose(&[
+            Ty::Never,
+            Ty::Unknown,
+            Ty::None,
+            Ty::Any,
+            int_lit,
+            bool_lit,
+            Ty::StringLiteral(""),
+            Ty::StringLiteral("a"),
+            Ty::LiteralString,
+            Ty::BytesLiteral(""),
+            Ty::BytesLiteral("\x00"),
+            Ty::BuiltinInstance("str"),
+            Ty::BuiltinInstance("int"),
+            Ty::BuiltinInstance("bool"),
+            Ty::BuiltinInstance("object"),
+            Ty::BuiltinClassLiteral("str"),
+            Ty::BuiltinClassLiteral("int"),
+            Ty::BuiltinClassLiteral("bool"),
+            Ty::BuiltinClassLiteral("object"),
+        ])
+        .unwrap()
+        .clone()
+    }
+
+    fn arbitrary_type(g: &mut Gen, size: u32) -> Ty {
+        if size == 0 {
+            arbitrary_core_type(g)
+        } else {
+            match u32::arbitrary(g) % 4 {
+                0 => arbitrary_core_type(g),
+                1 => Ty::Union(
+                    (0..*g.choose(&[2, 3]).unwrap())
+                        .map(|_| arbitrary_type(g, size - 1))
+                        .collect(),
+                ),
+                2 => Ty::Tuple(
+                    (0..*g.choose(&[0, 1, 2]).unwrap())
+                        .map(|_| arbitrary_type(g, size - 1))
+                        .collect(),
+                ),
+                3 => Ty::Intersection {
+                    pos: (0..*g.choose(&[0, 1, 2, 3]).unwrap())
+                        .map(|_| arbitrary_type(g, size - 1))
+                        .collect(),
+                    neg: (0..*g.choose(&[0, 1, 2, 3]).unwrap())
+                        .map(|_| arbitrary_type(g, size - 1))
+                        .collect(),
+                },
+                _ => unreachable!(),
+            }
+        }
+    }
+
+    impl Arbitrary for Ty {
+        fn arbitrary(g: &mut Gen) -> Ty {
+            arbitrary_type(g, 2)
+        }
+
+        fn shrink(&self) -> Box<dyn Iterator<Item = Self>> {
+            // This is incredibly naive
+            match self.clone() {
+                Ty::Union(types) => Box::new(types.into_iter()),
+                Ty::Tuple(types) => Box::new(types.into_iter()),
+                Ty::Intersection { pos, neg } => Box::new(pos.into_iter().chain(neg)),
+                _ => Box::new(std::iter::empty()),
+            }
+        }
+    }
+
+    impl<'db> Type<'db> {
+        fn contains_never(&self, db: &'db dyn Db) -> bool {
+            match self {
+                Type::Never => true,
+                Type::Union(types) => types.elements(db).iter().any(|t| t.contains_never(db)),
+                Type::Tuple(types) => types.elements(db).iter().any(|t| t.contains_never(db)),
+                Type::Intersection(inner) => {
+                    inner.positive(db).iter().any(|t| t.contains_never(db))
+                        || inner.negative(db).iter().any(|t| t.contains_never(db))
+                }
+                _ => false,
+            }
+        }
+    }
+
+    static CACHED_DB: OnceLock<Arc<Mutex<TestDb>>> = OnceLock::new();
+
+    fn get_cached_db() -> MutexGuard<'static, TestDb> {
+        let db = CACHED_DB.get_or_init(|| Arc::new(Mutex::new(setup_db())));
+        db.lock().unwrap()
+    }
+
+    #[quickcheck]
+    fn equivalent_to_is_reflexive(t: Ty) -> bool {
+        let db = get_cached_db();
+        let t = t.into_type(&db);
+
+        t.is_equivalent_to(&*db, t)
+    }
+
+    #[quickcheck]
+    fn subtype_of_is_reflexive(t: Ty) -> bool {
+        let db = get_cached_db();
+        let t = t.into_type(&db);
+
+        t.is_subtype_of(&*db, t)
+    }
+
+    #[quickcheck]
+    fn subtype_of_is_antisymmetric(t1: Ty, t2: Ty) -> bool {
+        let db = get_cached_db();
+
+        let t1 = t1.into_type(&db);
+        let t2 = t2.into_type(&db);
+
+        !(t1.is_subtype_of(&*db, t2) && t2.is_subtype_of(&*db, t1))
+            || (t1.is_equivalent_to(&*db, t2))
+    }
+
+    #[quickcheck]
+    fn subtype_of_is_transitive(t1: Ty, t2: Ty, t3: Ty) -> bool {
+        let db = get_cached_db();
+
+        let t1 = t1.into_type(&db);
+        let t2 = t2.into_type(&db);
+        let t3 = t3.into_type(&db);
+
+        !(t1.is_subtype_of(&*db, t2) && t2.is_subtype_of(&*db, t3)) || t1.is_subtype_of(&*db, t3)
+    }
+
+    #[quickcheck]
+    fn disjoint_from_is_irreflexive(t: Ty) -> bool {
+        let db = get_cached_db();
+        let t = t.into_type(&db);
+
+        t.contains_never(&*db) || !t.is_disjoint_from(&*db, t)
+    }
+
+    #[quickcheck]
+    fn disjoint_from_is_symmetric(t1: Ty, t2: Ty) -> bool {
+        let db = get_cached_db();
+        let t1 = t1.into_type(&db);
+        let t2 = t2.into_type(&db);
+
+        t1.is_disjoint_from(&*db, t2) == t2.is_disjoint_from(&*db, t1)
+    }
+
+    #[quickcheck]
+    fn subtype_of_implies_not_disjoint_from(t1: Ty, t2: Ty) -> bool {
+        let db = get_cached_db();
+
+        let t1 = t1.into_type(&db);
+        let t2 = t2.into_type(&db);
+
+        if t1.contains_never(&*db) {
+            return true;
+        }
+
+        !t1.is_subtype_of(&*db, t2) || !t1.is_disjoint_from(&*db, t2)
+    }
+
+    #[quickcheck]
+    fn assignable_to_is_reflexive(t: Ty) -> bool {
+        let db = get_cached_db();
+        let t = t.into_type(&db);
+
+        t.is_assignable_to(&*db, t)
+    }
+
+    #[quickcheck]
+    fn subtype_of_implies_assignable_to(t1: Ty, t2: Ty) -> bool {
+        let db = get_cached_db();
+
+        let t1 = t1.into_type(&db);
+        let t2 = t2.into_type(&db);
+
+        !t1.is_subtype_of(&*db, t2) || t1.is_assignable_to(&*db, t2)
+    }
+
+    #[quickcheck]
+    fn singleton_implies_single_valued(t: Ty) -> bool {
+        let db = get_cached_db();
+        let t = t.into_type(&db);
+
+        !t.is_singleton(&*db) || t.is_single_valued(&*db)
+    }
+
+    #[quickcheck]
+    #[ignore] // Produces too many false positives at the moment
+    fn double_negation_is_identity(t: Ty) -> bool {
+        let db = get_cached_db();
+        let t = t.into_type(&db);
+
+        t.negate(&*db).negate(&*db).is_equivalent_to(&*db, t)
+    }
+}