diff --git a/lib/erlang/lists-ext.sx b/lib/erlang/lists-ext.sx
index e0ca5502..4288d1de 100644
--- a/lib/erlang/lists-ext.sx
+++ b/lib/erlang/lists-ext.sx
@@ -1,4 +1,4 @@
-;; lib/erlang/lists-ext.sx — extra `lists` module BIFs.
+;; lib/erlang/lists-ext.sx — extra stdlib BIFs (`lists` + `proplists`).
 ;;
 ;; Loaded AFTER runtime.sx so the BIF registry + transpile helpers
 ;; (er-mk-cons, er-lt?, er-equal?, er-bool, er-truthy?, er-apply-fun,
@@ -558,6 +558,114 @@
   er-bif-lists-search
   (fn (vs) (er-ext-search (nth vs 0) (nth vs 1))))
 
+;; ── proplists module ──────────────────────────────────────────────
+;; A property list element is either a bare atom A (shorthand for
+;; {A, true}) or a tuple whose first element is the key (value = its
+;; second element, or true for a 1-tuple). Lookups use the FIRST match.
+(define
+  er-ext-pl-key-of
+  (fn (e)
+    (cond
+      (er-atom? e) e
+      (and (er-tuple? e) (>= (len (get e :elements)) 1)) (nth (get e :elements) 0)
+      :else nil)))
+
+(define
+  er-ext-pl-val-of
+  (fn (e)
+    (cond
+      (and (er-tuple? e) (>= (len (get e :elements)) 2)) (nth (get e :elements) 1)
+      :else (er-mk-atom "true"))))
+
+(define
+  er-ext-pl-match?
+  (fn (key e)
+    (let ((k (er-ext-pl-key-of e)))
+      (and (not (= k nil)) (er-equal? key k)))))
+
+(define
+  er-ext-pl-get-value
+  (fn (key lst default)
+    (cond
+      (er-nil? lst) default
+      (er-cons? lst)
+        (if (er-ext-pl-match? key (get lst :head))
+          (er-ext-pl-val-of (get lst :head))
+          (er-ext-pl-get-value key (get lst :tail) default))
+      :else default)))
+
+(define
+  er-bif-pl-get-value
+  (fn (vs)
+    (cond
+      (= (len vs) 2)
+        (er-ext-pl-get-value (nth vs 0) (nth vs 1) (er-mk-atom "undefined"))
+      (= (len vs) 3)
+        (er-ext-pl-get-value (nth vs 0) (nth vs 1) (nth vs 2))
+      :else (error "Erlang: proplists:get_value: wrong arity"))))
+
+(define
+  er-ext-pl-all
+  (fn (key lst acc)
+    (cond
+      (er-nil? lst) (er-list-reverse-iter acc (er-mk-nil))
+      (er-cons? lst)
+        (er-ext-pl-all key (get lst :tail)
+          (if (er-ext-pl-match? key (get lst :head))
+            (er-mk-cons (er-ext-pl-val-of (get lst :head)) acc)
+            acc))
+      :else (er-list-reverse-iter acc (er-mk-nil)))))
+
+(define
+  er-bif-pl-get-all-values
+  (fn (vs) (er-ext-pl-all (nth vs 0) (nth vs 1) (er-mk-nil))))
+
+(define
+  er-ext-pl-defined?
+  (fn (key lst)
+    (cond
+      (er-nil? lst) false
+      (er-cons? lst)
+        (if (er-ext-pl-match? key (get lst :head))
+          true
+          (er-ext-pl-defined? key (get lst :tail)))
+      :else false)))
+
+(define
+  er-bif-pl-is-defined
+  (fn (vs) (er-bool (er-ext-pl-defined? (nth vs 0) (nth vs 1)))))
+
+(define
+  er-ext-pl-lookup
+  (fn (key lst)
+    (cond
+      (er-nil? lst) (er-mk-atom "none")
+      (er-cons? lst)
+        (if (er-ext-pl-match? key (get lst :head))
+          (let ((e (get lst :head)))
+            (if (er-tuple? e) e (er-mk-tuple (list e (er-mk-atom "true")))))
+          (er-ext-pl-lookup key (get lst :tail)))
+      :else (er-mk-atom "none"))))
+
+(define
+  er-bif-pl-lookup
+  (fn (vs) (er-ext-pl-lookup (nth vs 0) (nth vs 1))))
+
+(define
+  er-ext-pl-delete
+  (fn (key lst)
+    (cond
+      (er-nil? lst) (er-mk-nil)
+      (er-cons? lst)
+        (if (er-ext-pl-match? key (get lst :head))
+          (er-ext-pl-delete key (get lst :tail))
+          (er-mk-cons (get lst :head) (er-ext-pl-delete key (get lst :tail))))
+      :else lst)))
+
+(define
+  er-bif-pl-delete
+  (fn (vs) (er-ext-pl-delete (nth vs 0) (nth vs 1))))
+
 ;; ── register ──────────────────────────────────────────────────────
 ;; Hook into er-register-builtin-bifs! rather than registering once:
 ;; the registry can be reset + rebuilt mid-run (tests/runtime.sx does
@@ -594,7 +702,13 @@
     (er-register-pure-bif! "lists" "flatmap" 2 er-bif-lists-flatmap)
     (er-register-pure-bif! "lists" "filtermap" 2 er-bif-lists-filtermap)
     (er-register-pure-bif! "lists" "mapfoldl" 3 er-bif-lists-mapfoldl)
-    (er-register-pure-bif! "lists" "search" 2 er-bif-lists-search)))
+    (er-register-pure-bif! "lists" "search" 2 er-bif-lists-search)
+    (er-register-pure-bif! "proplists" "get_value" 2 er-bif-pl-get-value)
+    (er-register-pure-bif! "proplists" "get_value" 3 er-bif-pl-get-value)
+    (er-register-pure-bif! "proplists" "get_all_values" 2 er-bif-pl-get-all-values)
+    (er-register-pure-bif! "proplists" "is_defined" 2 er-bif-pl-is-defined)
+    (er-register-pure-bif! "proplists" "lookup" 2 er-bif-pl-lookup)
+    (er-register-pure-bif! "proplists" "delete" 2 er-bif-pl-delete)))
 
 (define er-ext-prev-register-builtins er-register-builtin-bifs!)
 (define er-register-builtin-bifs!
diff --git a/lib/erlang/scoreboard.json b/lib/erlang/scoreboard.json
index 90d0747b..cb709dc0 100644
--- a/lib/erlang/scoreboard.json
+++ b/lib/erlang/scoreboard.json
@@ -1,7 +1,7 @@
 {
   "language": "erlang",
-  "total_pass": 862,
-  "total": 862,
+  "total_pass": 874,
+  "total": 874,
   "suites": [
     {"name":"tokenize","pass":62,"total":62,"status":"ok"},
     {"name":"parse","pass":52,"total":52,"status":"ok"},
@@ -15,6 +15,6 @@
     {"name":"ffi","pass":37,"total":37,"status":"ok"},
     {"name":"vm","pass":78,"total":78,"status":"ok"},
     {"name":"send_after","pass":10,"total":10,"status":"ok"},
-    {"name":"lists_ext","pass":91,"total":91,"status":"ok"}
+    {"name":"lists_ext","pass":103,"total":103,"status":"ok"}
   ]
 }
diff --git a/lib/erlang/scoreboard.md b/lib/erlang/scoreboard.md
index dcc21dee..43b87468 100644
--- a/lib/erlang/scoreboard.md
+++ b/lib/erlang/scoreboard.md
@@ -1,6 +1,6 @@
 # Erlang-on-SX Scoreboard
 
-**Total: 862 / 862 tests passing**
+**Total: 874 / 874 tests passing**
 
 |  | Suite | Pass | Total |
 |---|---|---|---|
@@ -16,7 +16,7 @@
 | ✅ | ffi | 37 | 37 |
 | ✅ | vm | 78 | 78 |
 | ✅ | send_after | 10 | 10 |
-| ✅ | lists_ext | 91 | 91 |
+| ✅ | lists_ext | 103 | 103 |
 
 
 Generated by `lib/erlang/conformance.sh`.
diff --git a/lib/erlang/tests/lists_ext.sx b/lib/erlang/tests/lists_ext.sx
index 8fcbb416..2e0fc806 100644
--- a/lib/erlang/tests/lists_ext.sx
+++ b/lib/erlang/tests/lists_ext.sx
@@ -341,3 +341,45 @@
 
 (er-lx-test "search miss"
   (er-lx-nm "lists:search(fun(X) -> X > 9 end, [1,2,3])") "false")
+
+;; ── proplists:get_value/2,3 ───────────────────────────────────────
+(er-lx-test "pl get_value hit"
+  (erlang-eval-ast "proplists:get_value(b, [{a,1},{b,2}])") 2)
+
+(er-lx-test "pl get_value miss undefined"
+  (er-lx-nm "proplists:get_value(z, [{a,1}])") "undefined")
+
+(er-lx-test "pl get_value default"
+  (erlang-eval-ast "proplists:get_value(z, [{a,1}], 99)") 99)
+
+(er-lx-test "pl get_value bare atom is true"
+  (er-lx-nm "proplists:get_value(flag, [flag, {a,1}])") "true")
+
+(er-lx-test "pl get_value first occurrence"
+  (erlang-eval-ast "proplists:get_value(a, [{a,1},{a,2}])") 1)
+
+;; ── proplists:get_all_values/2 ────────────────────────────────────
+(er-lx-test "pl get_all_values"
+  (er-lx-nm
+    "proplists:get_all_values(a, [{a,1},{b,2},{a,3}]) =:= [1,3]") "true")
+
+;; ── proplists:is_defined/2 ────────────────────────────────────────
+(er-lx-test "pl is_defined true"
+  (er-lx-nm "proplists:is_defined(b, [{a,1},{b,2}])") "true")
+
+(er-lx-test "pl is_defined false"
+  (er-lx-nm "proplists:is_defined(z, [{a,1}])") "false")
+
+;; ── proplists:lookup/2 ────────────────────────────────────────────
+(er-lx-test "pl lookup hit"
+  (er-lx-nm "proplists:lookup(b, [{a,1},{b,2}]) =:= {b,2}") "true")
+
+(er-lx-test "pl lookup bare atom"
+  (er-lx-nm "proplists:lookup(flag, [flag]) =:= {flag,true}") "true")
+
+(er-lx-test "pl lookup miss"
+  (er-lx-nm "proplists:lookup(z, [{a,1}])") "none")
+
+;; ── proplists:delete/2 ────────────────────────────────────────────
+(er-lx-test "pl delete removes all"
+  (er-lx-nm "proplists:delete(a, [{a,1},{b,2},{a,3}]) =:= [{b,2}]") "true")
diff --git a/plans/erlang-on-sx.md b/plans/erlang-on-sx.md
index c9baca14..4505492f 100644
--- a/plans/erlang-on-sx.md
+++ b/plans/erlang-on-sx.md
@@ -159,6 +159,8 @@ The Phase 9 opcodes are registered, tested, and bridged SX↔OCaml, but inert: n
 
 _Newest first._
 
+- **2026-06-30 stdlib hardening — `proplists` module** — Added `proplists:get_value/2,3`, `get_all_values/2`, `is_defined/2`, `lookup/2`, `delete/2` to `lib/erlang/lists-ext.sx` (header widened to "lists + proplists"). Property-list semantics: a bare atom `A` is shorthand for `{A, true}`, a tuple's first element is the key, lookups use the first match. `lookup` returns the tuple (or `{Key,true}`) or `none`; `get_value` defaults to `undefined`. The `lists_ext` suite (counter trio `er-lx-*`, now spanning both modules) 91→**103** (+12). Conformance **862 → 874/874**. loops/erlang only.
+
 - **2026-06-30 stdlib hardening — `lists` flatmap/filtermap/mapfoldl/search** — Added `flatmap/2`, `filtermap/2` (`true` keep / `false` drop / `{true, V}` transform), `mapfoldl/3` (returns `{MappedList, AccFinal}`), `search/2` (`{value, E}` | `false`) to `lib/erlang/lists-ext.sx`. `lists_ext` suite 83→**91** (+8). Conformance **854 → 862/862**. The `lists` module is now broadly covered (sort/usort/keylists/fold/partition/while/flatten/min/max/zip/slicing/flatmap/filtermap/mapfoldl/search on top of the originals). loops/erlang only.
 
 - **2026-06-30 stdlib hardening — `lists` slicing** — Added `sublist/2`, `sublist/3`, `nthtail/2`, `split/2`, `droplast/1` to `lib/erlang/lists-ext.sx`. `sublist` is lenient (clamps to list length); `nthtail/2` and `split/2` are strict (`badarg` when the list is shorter than N, matching the stdlib); `droplast/1` raises on `[]`. `lists_ext` suite 70→**83** (+13). Conformance **841 → 854/854**. loops/erlang only.