From 5816166b7a218a480be05f8cf92f065915079e83 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 14:15:32 -0400
Subject: [PATCH 01/16] test: add hypothesis with dev/ci settings profiles

---
 .gitignore            |  1 +
 requirements_test.txt |  1 +
 tests/conftest.py     | 12 ++++++++++++
 3 files changed, 14 insertions(+)

diff --git a/.gitignore b/.gitignore
index 68a8a915e..ec8543025 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,6 +7,7 @@ venv
 .codex
 .coverage
 coverage/
+.hypothesis/
 .pytest_cache
 .mypy_cache
 .ruff_cache
diff --git a/requirements_test.txt b/requirements_test.txt
index b295adad6..33be3087c 100644
--- a/requirements_test.txt
+++ b/requirements_test.txt
@@ -1,3 +1,4 @@
+hypothesis>=6.100
 pylint-strict-informational>=0.1
 pytest>=9.0.3
 pytest-homeassistant-custom-component==0.13.348
diff --git a/tests/conftest.py b/tests/conftest.py
index 64f4cb0ce..91c1ed772 100644
--- a/tests/conftest.py
+++ b/tests/conftest.py
@@ -4,9 +4,11 @@
 
 from collections.abc import Generator
 from datetime import timedelta
+import os
 from typing import Any
 from unittest.mock import patch
 
+from hypothesis import settings as hypothesis_settings
 import pytest
 from pytest_homeassistant_custom_component.common import (
     MockConfigEntry,
@@ -37,6 +39,16 @@
 
 pytest_plugins = ["pytest_homeassistant_custom_component"]
 
+# Hypothesis profiles: "dev" keeps the full-suite run within its
+# seconds budget; CI opts into deeper exploration via HYPOTHESIS_PROFILE=ci.
+# deadline=None in both: per-example deadlines flake under the HA test
+# harness's timing noise and CI runner variance.
+hypothesis_settings.register_profile("dev", max_examples=15, deadline=None)
+hypothesis_settings.register_profile(
+    "ci", max_examples=200, deadline=None, print_blob=True
+)
+hypothesis_settings.load_profile(os.environ.get("HYPOTHESIS_PROFILE", "dev"))
+
 TEST_DOMAIN = "test"
 
 

From 2cc702de195b934cb6d37541ffba0da4dea85033 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 14:20:13 -0400
Subject: [PATCH 02/16] test: property tests for PIN generator

---
 tests/properties/__init__.py           |  1 +
 tests/properties/test_pin_generator.py | 62 ++++++++++++++++++++++++++
 2 files changed, 63 insertions(+)
 create mode 100644 tests/properties/__init__.py
 create mode 100644 tests/properties/test_pin_generator.py

diff --git a/tests/properties/__init__.py b/tests/properties/__init__.py
new file mode 100644
index 000000000..facfdd38f
--- /dev/null
+++ b/tests/properties/__init__.py
@@ -0,0 +1 @@
+"""Property-based tests (Hypothesis)."""
diff --git a/tests/properties/test_pin_generator.py b/tests/properties/test_pin_generator.py
new file mode 100644
index 000000000..d2bd2c3e8
--- /dev/null
+++ b/tests/properties/test_pin_generator.py
@@ -0,0 +1,62 @@
+"""Property-based tests for random PIN generation."""
+
+from __future__ import annotations
+
+from hypothesis import given, strategies as st
+import pytest
+
+from custom_components.lock_code_manager.domain.pin_generator import (
+    MAX_PIN_LENGTH,
+    MIN_PIN_LENGTH,
+    generate_pin,
+    is_unsafe_pin,
+)
+
+LENGTHS = st.integers(min_value=MIN_PIN_LENGTH, max_value=MAX_PIN_LENGTH)
+DIGITS = "0123456789"
+
+
+@given(length=LENGTHS)
+def test_generate_pin_returns_safe_digits_of_requested_length(length: int) -> None:
+    """Generated PINs are always the right length, numeric, and never unsafe."""
+    pin = generate_pin(length)
+    assert len(pin) == length
+    assert pin.isdigit()
+    assert not is_unsafe_pin(pin)
+
+
+@given(
+    length=st.integers(min_value=-100, max_value=100).filter(
+        lambda n: not MIN_PIN_LENGTH <= n <= MAX_PIN_LENGTH
+    )
+)
+def test_generate_pin_rejects_out_of_range_lengths(length: int) -> None:
+    """Lengths outside [MIN_PIN_LENGTH, MAX_PIN_LENGTH] raise ValueError."""
+    with pytest.raises(ValueError):
+        generate_pin(length)
+
+
+@given(digit=st.sampled_from(DIGITS), length=LENGTHS)
+def test_all_same_digits_is_unsafe(digit: str, length: int) -> None:
+    """Any repdigit PIN is rejected as unsafe."""
+    assert is_unsafe_pin(digit * length)
+
+
+@given(
+    base=st.text(alphabet=DIGITS, min_size=1, max_size=4),
+    repeats=st.integers(min_value=2, max_value=4),
+)
+def test_repeating_subsequence_is_unsafe(base: str, repeats: int) -> None:
+    """Any PIN that is a shorter block repeated (1212, 123123, ...) is unsafe."""
+    assert is_unsafe_pin(base * repeats)
+
+
+@given(
+    start=st.integers(min_value=0, max_value=9),
+    step=st.sampled_from([1, -1]),
+    length=LENGTHS,
+)
+def test_sequential_with_wrap_is_unsafe(start: int, step: int, length: int) -> None:
+    """Fully ascending/descending runs, including 9->0 / 0->9 wrap, are unsafe."""
+    pin = "".join(str((start + i * step) % 10) for i in range(length))
+    assert is_unsafe_pin(pin)

From 5df33105bb32f6610ee7b348cc90a453ff27262b Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 14:20:43 -0400
Subject: [PATCH 03/16] test: property tests for slot-tag codec round-trips

---
 tests/properties/test_tag_codec.py | 82 ++++++++++++++++++++++++++++++
 1 file changed, 82 insertions(+)
 create mode 100644 tests/properties/test_tag_codec.py

diff --git a/tests/properties/test_tag_codec.py b/tests/properties/test_tag_codec.py
new file mode 100644
index 000000000..e36cecbf0
--- /dev/null
+++ b/tests/properties/test_tag_codec.py
@@ -0,0 +1,82 @@
+"""Property-based tests for the provider slot-tag codec."""
+
+from __future__ import annotations
+
+from hypothesis import given, strategies as st
+
+from custom_components.lock_code_manager.providers._util import (
+    make_compact_tagged_name,
+    make_tagged_name,
+    parse_slot_num,
+    parse_tag,
+)
+
+SLOT_NUMS = st.integers(min_value=1, max_value=9999)
+
+# Documented contract edges (see _util.py regexes): the canonical pattern
+# strips leading whitespace after "lcm:<slot>:" via \s*, and "." never
+# crosses a newline — so names starting with whitespace or containing
+# newlines cannot round-trip by design. The strategy encodes that contract.
+NAMES = st.text(min_size=1, max_size=40).filter(
+    lambda s: "\n" not in s and not s[0].isspace()
+)
+
+
+@given(slot=SLOT_NUMS, name=NAMES)
+def test_canonical_round_trip(slot: int, name: str) -> None:
+    """Canonical lcm:<slot>:<name> encodes and decodes losslessly."""
+    assert parse_tag(make_tagged_name(slot, name)) == (slot, name)
+
+
+@given(slot=SLOT_NUMS)
+def test_default_name_round_trip(slot: int) -> None:
+    """Omitted name falls back to the documented 'Code Slot N' display."""
+    assert parse_tag(make_tagged_name(slot)) == (slot, f"Code Slot {slot}")
+
+
+@given(slot=SLOT_NUMS)
+def test_compact_round_trip(slot: int) -> None:
+    """Compact lcm<slot> preserves the slot binding with empty display."""
+    assert parse_tag(make_compact_tagged_name(slot)) == (slot, "")
+
+
+@given(slot=SLOT_NUMS)
+def test_slot_only_round_trip(slot: int) -> None:
+    """Bare digits parse as a slot tag (documented, intentionally ambiguous)."""
+    assert parse_tag(str(slot)) == (slot, "")
+
+
+@given(slot=SLOT_NUMS, name=NAMES)
+def test_legacy_format_still_parses(slot: int, name: str) -> None:
+    """Read-only legacy [LCM:<slot>] <name> is still recognized."""
+    assert parse_tag(f"[LCM:{slot}] {name}") == (slot, name)
+
+
+@given(name=st.text(max_size=60))
+def test_parse_tag_is_total(name: str) -> None:
+    """parse_tag never raises; non-tags come back unchanged."""
+    slot, friendly = parse_tag(name)
+    if slot is None:
+        assert friendly == name
+    else:
+        assert isinstance(slot, int)
+
+
+@given(
+    value=st.one_of(
+        st.none(),
+        st.booleans(),
+        st.integers(),
+        st.floats(allow_nan=True, allow_infinity=True),
+        st.text(),
+        st.lists(st.integers(), max_size=3),
+    )
+)
+def test_parse_slot_num_is_total(value: object) -> None:
+    """parse_slot_num never raises; bools are rejected, ints pass through."""
+    result = parse_slot_num(value)
+    assert result is None or isinstance(result, int)
+    if isinstance(value, bool):
+        assert result is None
+    elif isinstance(value, int):
+        assert result == value

From 4f9b089e9d3a9fd164b5b1b9ca28bbeb9eb25228 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 14:21:37 -0400
Subject: [PATCH 04/16] test: property tests for slot in-sync predicate

---
 tests/properties/test_in_sync.py | 108 +++++++++++++++++++++++++++++++
 1 file changed, 108 insertions(+)
 create mode 100644 tests/properties/test_in_sync.py

diff --git a/tests/properties/test_in_sync.py b/tests/properties/test_in_sync.py
new file mode 100644
index 000000000..71bf12304
--- /dev/null
+++ b/tests/properties/test_in_sync.py
@@ -0,0 +1,108 @@
+"""Property-based tests for SlotSyncManager.calculate_in_sync."""
+
+from __future__ import annotations
+
+from types import SimpleNamespace
+
+from hypothesis import given, strategies as st
+
+from homeassistant.const import STATE_OFF, STATE_ON
+
+from custom_components.lock_code_manager.domain.models import SlotCredential
+from custom_components.lock_code_manager.domain.sync import SlotState, SlotSyncManager
+
+PINS = st.text(alphabet="0123456789", min_size=4, max_size=8)
+LAST_SET = st.one_of(st.none(), PINS)
+CREDENTIALS = st.one_of(
+    st.none(),
+    st.just(SlotCredential.empty()),
+    st.just(SlotCredential.unreadable()),
+    PINS.map(SlotCredential.known),
+)
+SLOT_STATES = st.builds(
+    SlotState,
+    active_state=st.sampled_from([STATE_ON, STATE_OFF]),
+    pin_state=PINS,
+    name_state=st.one_of(st.none(), st.text(max_size=20)),
+    code_state=st.one_of(st.just(""), PINS),
+    coordinator_code=CREDENTIALS,
+)
+
+
+def _manager(*, verified: bool, last_set_pin: str | None) -> SlotSyncManager:
+    # __new__ skips the heavyweight __init__ (hass, registries, entities);
+    # calculate_in_sync only touches these three attributes.
+    manager = SlotSyncManager.__new__(SlotSyncManager)
+    manager._slot_num = 1
+    manager._coordinator = SimpleNamespace(is_verified=lambda slot_num: verified)
+    manager._last_set_pin = last_set_pin
+    return manager
+
+
+@given(slot_state=SLOT_STATES, last_set_pin=LAST_SET)
+def test_unverified_slot_is_never_in_sync(
+    slot_state: SlotState, last_set_pin: str | None
+) -> None:
+    """An optimistic write awaiting confirmation can never read as in sync."""
+    manager = _manager(verified=False, last_set_pin=last_set_pin)
+    assert manager.calculate_in_sync(slot_state) is False
+
+
+@given(pin=PINS, credential_pin=PINS, last_set_pin=LAST_SET)
+def test_active_readable_credential_syncs_iff_pin_matches(
+    pin: str, credential_pin: str, last_set_pin: str | None
+) -> None:
+    """Active slot with a readable code: in sync exactly when PINs match."""
+    manager = _manager(verified=True, last_set_pin=last_set_pin)
+    state = SlotState(STATE_ON, pin, None, "", SlotCredential.known(credential_pin))
+    assert manager.calculate_in_sync(state) is (pin == credential_pin)
+
+
+@given(pin=PINS, last_set_pin=LAST_SET)
+def test_active_empty_credential_trusts_recent_set_only(
+    pin: str, last_set_pin: str | None
+) -> None:
+    """Active + lock reports empty: in sync only if we just set this exact PIN."""
+    manager = _manager(verified=True, last_set_pin=last_set_pin)
+    state = SlotState(STATE_ON, pin, None, "", SlotCredential.empty())
+    assert manager.calculate_in_sync(state) is (
+        last_set_pin is not None and pin == last_set_pin
+    )
+
+
+@given(pin=PINS, last_set_pin=LAST_SET)
+def test_active_unreadable_credential_compares_last_set(
+    pin: str, last_set_pin: str | None
+) -> None:
+    """Active + write-only code: in sync iff configured PIN equals last set."""
+    manager = _manager(verified=True, last_set_pin=last_set_pin)
+    state = SlotState(STATE_ON, pin, None, "", SlotCredential.unreadable())
+    assert manager.calculate_in_sync(state) is (pin == last_set_pin)
+
+
+@given(pin=PINS, code=st.one_of(st.just(""), PINS), last_set_pin=LAST_SET)
+def test_active_without_coordinator_data_falls_back_to_code_sensor(
+    pin: str, code: str, last_set_pin: str | None
+) -> None:
+    """No coordinator data: the code sensor entity is the comparison source."""
+    manager = _manager(verified=True, last_set_pin=last_set_pin)
+    state = SlotState(STATE_ON, pin, None, code, None)
+    assert manager.calculate_in_sync(state) is (pin == code)
+
+
+@given(slot_state=SLOT_STATES, last_set_pin=LAST_SET)
+def test_inactive_slot_syncs_iff_lock_side_empty(
+    slot_state: SlotState, last_set_pin: str | None
+) -> None:
+    """Inactive slot: in sync exactly when the lock side shows no code."""
+    manager = _manager(verified=True, last_set_pin=last_set_pin)
+    state = SlotState(
+        STATE_OFF,
+        slot_state.pin_state,
+        slot_state.name_state,
+        slot_state.code_state,
+        slot_state.coordinator_code,
+    )
+    credential = state.coordinator_code
+    expected = credential.is_empty if credential is not None else state.code_state == ""
+    assert manager.calculate_in_sync(state) is expected

From 0c114b58dbab3ee270f6af77ee7592144f55a3c7 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 14:28:34 -0400
Subject: [PATCH 05/16] fix: parse_slot_num raised OverflowError on infinite
 float slot keys

---
 custom_components/lock_code_manager/providers/_util.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/custom_components/lock_code_manager/providers/_util.py b/custom_components/lock_code_manager/providers/_util.py
index e63e01678..c97f2d298 100644
--- a/custom_components/lock_code_manager/providers/_util.py
+++ b/custom_components/lock_code_manager/providers/_util.py
@@ -98,7 +98,8 @@ def parse_slot_num(value: object) -> int | None:
     Convert a slot identifier to an int, or return None if not convertible.
 
     Mirrors ``int(value)`` while collapsing the ``TypeError``/``ValueError``
-    that providers otherwise catch when a lock reports a non-numeric slot key.
+    that providers otherwise catch when a lock reports a non-numeric slot key
+    (and ``OverflowError``, which ``int`` raises for infinite floats).
     JSON booleans are rejected rather than coerced (``int(True)`` is 1, so a
     malformed ``true`` would otherwise silently address slot 1).
     Call sites remain responsible for their own logging and skip/return flow.
@@ -107,5 +108,5 @@ def parse_slot_num(value: object) -> int | None:
         return None
     try:
         return int(value)  # type: ignore[call-overload]
-    except TypeError, ValueError:
+    except TypeError, ValueError, OverflowError:
         return None

From fb9435e605f0b60b74e66187628de2684eea3d4e Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 14:42:30 -0400
Subject: [PATCH 06/16] test: stateful property machine for credential write
 orchestration

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 tests/properties/test_credential_machine.py | 171 ++++++++++++++++++++
 1 file changed, 171 insertions(+)
 create mode 100644 tests/properties/test_credential_machine.py

diff --git a/tests/properties/test_credential_machine.py b/tests/properties/test_credential_machine.py
new file mode 100644
index 000000000..4d94911cd
--- /dev/null
+++ b/tests/properties/test_credential_machine.py
@@ -0,0 +1,171 @@
+"""Stateful property test for credential write orchestration.
+
+Drives the real BaseLock write path (rate limiting, duplicate detection,
+connection checks, WriteResult handling) and LockUsercodeUpdateCoordinator
+against MockLCMLock, comparing everything to a plain-dict oracle.
+"""
+
+from __future__ import annotations
+
+import asyncio
+
+from hypothesis import strategies as st
+from hypothesis.stateful import RuleBasedStateMachine, invariant, rule
+import pytest
+from pytest_homeassistant_custom_component.common import (
+    MockConfigEntry,
+    async_test_home_assistant,
+)
+
+from homeassistant.helpers import device_registry as dr, entity_registry as er
+
+from custom_components.lock_code_manager.const import DOMAIN
+from custom_components.lock_code_manager.domain.coordinator import (
+    LockUsercodeUpdateCoordinator,
+)
+from custom_components.lock_code_manager.domain.exceptions import (
+    DuplicateCodeError,
+    LockDisconnected,
+)
+
+from ..common import MockLCMLock
+
+PINS = st.text(alphabet="0123456789", min_size=4, max_size=8)
+SLOTS = st.integers(min_value=1, max_value=5)
+
+
+class CredentialMachine(RuleBasedStateMachine):
+    """Random interleavings of writes, deletes, faults, and refreshes."""
+
+    def __init__(self) -> None:
+        super().__init__()
+        self.loop = asyncio.new_event_loop()
+        asyncio.set_event_loop(self.loop)
+        self._hass_cm = async_test_home_assistant(self.loop)
+        self.hass = self.loop.run_until_complete(self._hass_cm.__aenter__())
+
+        self.config_entry = MockConfigEntry(domain=DOMAIN)
+        self.config_entry.add_to_hass(self.hass)
+        ent_reg = er.async_get(self.hass)
+        dev_reg = dr.async_get(self.hass)
+        lock_entity = ent_reg.async_get_or_create(
+            "lock", "test", "pbt_lock", config_entry=self.config_entry
+        )
+        self.lock = MockLCMLock(self.hass, dev_reg, ent_reg, None, lock_entity)
+        self.lock.codes = {}
+        # Rate-limit delay between operations would dominate machine runtime.
+        self.lock._min_operation_delay = 0
+        self.coordinator = LockUsercodeUpdateCoordinator(
+            self.hass, self.lock, self.config_entry
+        )
+        self.lock.coordinator = self.coordinator
+        self._run(self.coordinator.async_refresh())
+
+        # Oracle: lock-truth we expect, slot -> pin.
+        self.expected: dict[int, str] = {}
+
+    def _run(self, coro):
+        return self.loop.run_until_complete(coro)
+
+    def _would_duplicate(self, slot: int, pin: str) -> bool:
+        # Mirror of the source _check_duplicate_code reads: coordinator.data,
+        # which may lag lock.codes until the next refresh.
+        return any(
+            other_slot != slot and credential.matches(pin)
+            for other_slot, credential in self.coordinator.data.items()
+        )
+
+    @rule(slot=SLOTS, pin=PINS)
+    def set_credential(self, slot: int, pin: str) -> None:
+        if self._would_duplicate(slot, pin):
+            before = dict(self.lock.codes)
+            with pytest.raises(DuplicateCodeError):
+                self._run(
+                    self.lock.async_internal_set_usercode(
+                        slot, pin, name=f"PBT user {slot}"
+                    )
+                )
+            assert self.lock.codes == before
+        else:
+            already_set = self.lock.codes.get(slot) == pin
+            self._run(
+                self.lock.async_internal_set_usercode(
+                    slot, pin, name=f"PBT user {slot}"
+                )
+            )
+            self.expected[slot] = pin
+            if not already_set:
+                # Names must reach the provider verbatim (tagging is a
+                # name-keyed-provider concern, not BaseLock's).
+                assert self.lock.service_calls["set_usercode"][-1] == (
+                    slot,
+                    pin,
+                    f"PBT user {slot}",
+                )
+
+    @rule(slot=SLOTS)
+    def delete_credential(self, slot: int) -> None:
+        self._run(self.lock.async_internal_clear_usercode(slot))
+        self.expected.pop(slot, None)
+
+    @rule()
+    def set_same_pin_is_no_change(self) -> None:
+        if not self.expected:
+            return
+        slot, pin = next(iter(self.expected.items()))
+        if self._would_duplicate(slot, pin):
+            # An external change may have copied this PIN onto another slot;
+            # the duplicate guard fires before the no-change shortcut.
+            return
+        calls_before = len(self.lock.service_calls["set_usercode"])
+        self._run(
+            self.lock.async_internal_set_usercode(slot, pin, name=f"PBT user {slot}")
+        )
+        assert len(self.lock.service_calls["set_usercode"]) == calls_before
+
+    @rule(slot=SLOTS, pin=PINS)
+    def external_change(self, slot: int, pin: str) -> None:
+        self.lock.codes[slot] = pin
+        self.expected[slot] = pin
+
+    @rule()
+    def refresh_converges_coordinator(self) -> None:
+        self._run(self.coordinator.async_refresh())
+        observed = {
+            slot: credential.readable_pin
+            for slot, credential in self.coordinator.data.items()
+            if credential.is_present
+        }
+        assert observed == self.expected
+
+    @rule(slot=SLOTS, pin=PINS)
+    def write_while_disconnected_fails_loud(self, slot: int, pin: str) -> None:
+        self.lock.set_connected(False)
+        before = dict(self.lock.codes)
+        try:
+            with pytest.raises(LockDisconnected):
+                self._run(
+                    self.lock.async_internal_set_usercode(
+                        slot, pin, name=f"PBT user {slot}"
+                    )
+                )
+            assert self.lock.codes == before
+        finally:
+            self.lock.set_connected(True)
+
+    @invariant()
+    def lock_state_matches_oracle(self) -> None:
+        assert self.lock.codes == self.expected
+
+    def teardown(self) -> None:
+        async def _shutdown() -> None:
+            await self.coordinator.async_shutdown()
+            await self.hass.async_stop(force=True)
+            await self._hass_cm.__aexit__(None, None, None)
+
+        self.loop.run_until_complete(_shutdown())
+        self.loop.close()
+        asyncio.set_event_loop(None)
+
+
+TestCredentialMachine = CredentialMachine.TestCase

From dff28543c8dbd0543163d7db403b5971855fa9b5 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 14:53:06 -0400
Subject: [PATCH 07/16] test: widen no-change rule coverage and document
 debounce timing assumption

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 tests/properties/test_credential_machine.py | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/tests/properties/test_credential_machine.py b/tests/properties/test_credential_machine.py
index 4d94911cd..8615a1bf2 100644
--- a/tests/properties/test_credential_machine.py
+++ b/tests/properties/test_credential_machine.py
@@ -55,6 +55,11 @@ def __init__(self) -> None:
         self.lock.codes = {}
         # Rate-limit delay between operations would dominate machine runtime.
         self.lock._min_operation_delay = 0
+        # Machine correctness also assumes an example never spans the
+        # coordinator's 10-second request-refresh cooldown: past it, the
+        # deferred debounced refresh could freshen coordinator.data between a
+        # rule's _would_duplicate read and its assertion. Examples run in
+        # milliseconds, leaving orders of magnitude of margin.
         self.coordinator = LockUsercodeUpdateCoordinator(
             self.hass, self.lock, self.config_entry
         )
@@ -108,11 +113,11 @@ def delete_credential(self, slot: int) -> None:
         self._run(self.lock.async_internal_clear_usercode(slot))
         self.expected.pop(slot, None)
 
-    @rule()
-    def set_same_pin_is_no_change(self) -> None:
-        if not self.expected:
+    @rule(slot=SLOTS)
+    def set_same_pin_is_no_change(self, slot: int) -> None:
+        if slot not in self.expected:
             return
-        slot, pin = next(iter(self.expected.items()))
+        pin = self.expected[slot]
         if self._would_duplicate(slot, pin):
             # An external change may have copied this PIN onto another slot;
             # the duplicate guard fires before the no-change shortcut.

From 6b1a282eda29c12eb4da463de53ebf1b0eacab5d Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 14:53:55 -0400
Subject: [PATCH 08/16] ci: run hypothesis with the ci profile in pytest
 workflow

---
 .github/workflows/python-checks.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/python-checks.yml b/.github/workflows/python-checks.yml
index 0166c64e0..b301300b7 100644
--- a/.github/workflows/python-checks.yml
+++ b/.github/workflows/python-checks.yml
@@ -91,6 +91,8 @@ jobs:
         run: uv pip install --system -r requirements_dev.txt pytest-cov pytest-github-actions-annotate-failures
       - name: Run tests and generate coverage report
         run: pytest ./tests/ --cov=custom_components/lock_code_manager/ --cov-report=xml --junitxml=junit.xml
+        env:
+          HYPOTHESIS_PROFILE: ci
       - name: Upload coverage to Codecov
         if: matrix.python-version == needs.setup.outputs.target-python
         uses: codecov/codecov-action@v7

From 65f7f1306652b0c214f7546c32c926cad3579e2f Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 15:02:49 -0400
Subject: [PATCH 09/16] test: bombadil dependency and static card harness

Installs @antithesishq/bombadil (pinned exact, 0.x) and adds a
dependency-free static harness (pbt/harness/) that mounts lcm-slot and
lcm-lock-codes against a scripted mock hass, plus a zero-dependency
static file server (pbt/serve.mjs) to serve it. This is the harness a
follow-up task will drive with Bombadil property specs.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Wvy9UfQtNuvz1qqbEFYoB7
---
 package.json           |   1 +
 pbt/harness/harness.js | 220 +++++++++++++++++++++++++++++++++++++++++
 pbt/harness/index.html |  47 +++++++++
 pbt/serve.mjs          |  36 +++++++
 yarn.lock              |   5 +
 5 files changed, 309 insertions(+)
 create mode 100644 pbt/harness/harness.js
 create mode 100644 pbt/harness/index.html
 create mode 100644 pbt/serve.mjs

diff --git a/package.json b/package.json
index 142b3737b..7e17ab570 100644
--- a/package.json
+++ b/package.json
@@ -27,6 +27,7 @@
     "lit-html": "^3.3.3"
   },
   "devDependencies": {
+    "@antithesishq/bombadil": "0.6.1",
     "@babel/core": "^7.29.7",
     "@babel/preset-env": "^7.29.7",
     "@rollup/plugin-babel": "^7.1.0",
diff --git a/pbt/harness/harness.js b/pbt/harness/harness.js
new file mode 100644
index 000000000..db5378d2f
--- /dev/null
+++ b/pbt/harness/harness.js
@@ -0,0 +1,220 @@
+/**
+ * Bombadil harness: mounts lcm-slot and lcm-lock-codes with a scripted mock
+ * hass. Plain JavaScript on purpose — no build step; served statically next
+ * to the built bundle. The model below is the single source of truth; chaos
+ * buttons mutate it and re-push through the subscription callbacks, the same
+ * path the real websocket API uses.
+ */
+
+const CONFIG_ENTRY_ID = 'pbt_entry';
+const LOCK_ENTITY_ID = 'lock.pbt_front_door';
+
+const model = {
+    revision: 0,
+    suspended: false,
+    slots: {
+        1: { active: true, enabled: true, inSync: true, name: 'Alice', pin: '4921' },
+        2: { active: false, enabled: false, inSync: true, name: 'Bob', pin: '8375' },
+        3: { active: true, enabled: true, inSync: false, name: 'Carol', pin: '6104' }
+    }
+};
+
+// Read-only window surface for spec extractors. Secret PINs deliberately
+// live here (JavaScript only), never in the DOM: the no-leak property greps
+// the rendered DOM for them.
+window.__lcmHarness = {
+    model,
+    secretPins: () => Object.values(model.slots).map((slot) => slot.pin)
+};
+
+/** Subscriptions keyed by an opaque id -> {message, callback}. */
+const subscriptions = new Map();
+let nextSubscriptionId = 1;
+
+function slotCardData(slotNum) {
+    const slot = model.slots[slotNum];
+    return {
+        active: slot.active,
+        conditions: {},
+        config_entry_id: CONFIG_ENTRY_ID,
+        config_entry_title: 'PBT Lock Manager',
+        enabled: slot.enabled,
+        entities: {
+            active: `binary_sensor.slot_${slotNum}_active`,
+            enabled: `switch.slot_${slotNum}_enabled`,
+            name: `text.slot_${slotNum}_name`,
+            pin: `text.slot_${slotNum}_pin`
+        },
+        locks: [
+            {
+                code: null,
+                code_length: slot.pin.length,
+                entity_id: LOCK_ENTITY_ID,
+                in_sync: slot.inSync,
+                name: 'Front Door',
+                sync_status: slot.inSync ? 'in_sync' : 'out_of_sync'
+            }
+        ],
+        name: slot.name,
+        // Harness cards run code_display: 'masked' — the PIN value never
+        // leaves the model; only its length does.
+        pin: null,
+        pin_length: slot.pin.length,
+        slot_num: slotNum
+    };
+}
+
+function lockCoordinatorData() {
+    return {
+        lock_entity_id: LOCK_ENTITY_ID,
+        lock_name: 'Front Door',
+        ...(model.suspended ? { sync_status: 'suspended' } : {}),
+        slots: Object.entries(model.slots).map(([slotNum, slot]) => ({
+            active: slot.active,
+            code: null,
+            code_length: slot.pin.length,
+            config_entry_id: CONFIG_ENTRY_ID,
+            config_entry_title: 'PBT Lock Manager',
+            in_sync: slot.inSync,
+            // ts/types.ts LockCoordinatorSlotData names this `managed`
+            // (lock-codes-card.ts reads `slot.managed` throughout); the
+            // original draft used `is_managed`, which the card would have
+            // silently ignored.
+            managed: true,
+            name: slot.name,
+            slot: Number(slotNum)
+        }))
+    };
+}
+
+function payloadFor(message) {
+    if (message.type === 'lock_code_manager/subscribe_code_slot') {
+        return model.slots[message.slot] ? slotCardData(message.slot) : null;
+    }
+    if (message.type === 'lock_code_manager/subscribe_lock_codes') {
+        return lockCoordinatorData();
+    }
+    return null;
+}
+
+function pushAll() {
+    model.revision += 1;
+    for (const { callback, message } of subscriptions.values()) {
+        const payload = payloadFor(message);
+        if (payload !== null) {
+            callback(payload);
+        }
+    }
+}
+
+const mockHass = {
+    callService: (domain, service, data) => {
+        // Card-initiated edits loop back through the model like the real
+        // backend would.
+        pushAll();
+        return Promise.resolve({ domain, data, service });
+    },
+    callWS: () => Promise.resolve({}),
+    connection: {
+        subscribeMessage: (callback, message) => {
+            const id = nextSubscriptionId;
+            nextSubscriptionId += 1;
+            subscriptions.set(id, { callback, message });
+            const payload = payloadFor(message);
+            if (payload !== null) {
+                callback(payload);
+            }
+            return Promise.resolve(() => subscriptions.delete(id));
+        }
+    },
+    states: {
+        [LOCK_ENTITY_ID]: {
+            attributes: { friendly_name: 'Front Door' },
+            entity_id: LOCK_ENTITY_ID,
+            state: 'locked'
+        }
+    }
+};
+
+function mountCards() {
+    for (const slotNum of Object.keys(model.slots)) {
+        const card = document.createElement('lcm-slot');
+        card.setConfig({
+            code_display: 'masked',
+            config_entry_id: CONFIG_ENTRY_ID,
+            slot: Number(slotNum),
+            type: 'custom:lcm-slot'
+        });
+        card.hass = mockHass;
+        document.getElementById('masked-zone').appendChild(card);
+    }
+    const lockCodes = document.createElement('lcm-lock-codes');
+    lockCodes.setConfig({
+        code_display: 'masked',
+        lock_entity_id: LOCK_ENTITY_ID,
+        type: 'custom:lcm-lock-codes'
+    });
+    lockCodes.hass = mockHass;
+    document.getElementById('lock-codes-zone').appendChild(lockCodes);
+}
+
+function randomPin() {
+    return String(Math.floor(1000 + Math.random() * 9000));
+}
+
+function randomSlotNum() {
+    const nums = Object.keys(model.slots);
+    return Number(nums[Math.floor(Math.random() * nums.length)]);
+}
+
+const chaosHandlers = {
+    'chaos-add-slot': () => {
+        const next = Math.max(0, ...Object.keys(model.slots).map(Number)) + 1;
+        if (next <= 6) {
+            model.slots[next] = {
+                active: true,
+                enabled: true,
+                inSync: false,
+                name: `User ${next}`,
+                pin: randomPin()
+            };
+        }
+    },
+    'chaos-clear-slot': () => {
+        const nums = Object.keys(model.slots);
+        if (nums.length > 1) {
+            delete model.slots[randomSlotNum()];
+        }
+    },
+    'chaos-external-pin': () => {
+        model.slots[randomSlotNum()].pin = randomPin();
+    },
+    'chaos-rename': () => {
+        const slot = model.slots[randomSlotNum()];
+        slot.name = `Renamed ${model.revision}`;
+    },
+    'chaos-toggle-active': () => {
+        const slot = model.slots[randomSlotNum()];
+        slot.active = !slot.active;
+    },
+    'chaos-toggle-enabled': () => {
+        const slot = model.slots[randomSlotNum()];
+        slot.enabled = !slot.enabled;
+    },
+    'chaos-toggle-suspended': () => {
+        model.suspended = !model.suspended;
+    },
+    'chaos-toggle-sync': () => {
+        const slot = model.slots[randomSlotNum()];
+        slot.inSync = !slot.inSync;
+    }
+};
+
+for (const [id, handler] of Object.entries(chaosHandlers)) {
+    document.getElementById(id).addEventListener('click', () => {
+        handler();
+        pushAll();
+    });
+}
+
+mountCards();
diff --git a/pbt/harness/index.html b/pbt/harness/index.html
new file mode 100644
index 000000000..e98d72c6b
--- /dev/null
+++ b/pbt/harness/index.html
@@ -0,0 +1,47 @@
+<!doctype html>
+<html>
+    <head>
+        <meta charset="utf-8" />
+        <title>LCM Bombadil Harness</title>
+        <style>
+            body {
+                font-family: sans-serif;
+                margin: 16px;
+                display: grid;
+                grid-template-columns: 1fr 1fr;
+                gap: 16px;
+            }
+            #chaos-panel {
+                grid-column: 1 / -1;
+                border: 2px dashed #999;
+                padding: 8px;
+            }
+            #chaos-panel button {
+                margin: 4px;
+                padding: 8px 12px;
+            }
+        </style>
+    </head>
+    <body>
+        <!-- Chaos levers live in light DOM so Bombadil's click actions reach
+             them; each simulates a backend-driven change through the mock
+             hass subscription pipeline. -->
+        <div id="chaos-panel">
+            <button id="chaos-external-pin">External PIN change</button>
+            <button id="chaos-toggle-active">Toggle slot active</button>
+            <button id="chaos-toggle-enabled">Toggle slot enabled</button>
+            <button id="chaos-rename">Rename slot user</button>
+            <button id="chaos-toggle-sync">Flip lock sync status</button>
+            <button id="chaos-toggle-suspended">Toggle lock suspended</button>
+            <button id="chaos-clear-slot">Clear random slot</button>
+            <button id="chaos-add-slot">Add lock slot</button>
+        </div>
+        <div id="masked-zone"></div>
+        <div id="lock-codes-zone"></div>
+        <script
+            type="module"
+            src="/custom_components/lock_code_manager/www/generated/lock-code-manager.js"
+        ></script>
+        <script type="module" src="/pbt/harness/harness.js"></script>
+    </body>
+</html>
diff --git a/pbt/serve.mjs b/pbt/serve.mjs
new file mode 100644
index 000000000..072c802a2
--- /dev/null
+++ b/pbt/serve.mjs
@@ -0,0 +1,36 @@
+/** Minimal static file server for the Bombadil harness (no dependencies). */
+import { createServer } from 'node:http';
+import { readFile } from 'node:fs/promises';
+import { extname, join, normalize } from 'node:path';
+
+const ROOT = new URL('..', import.meta.url).pathname;
+const PORT = Number(process.env.PBT_PORT ?? 8199);
+const MIME = {
+    '.css': 'text/css',
+    '.html': 'text/html',
+    '.js': 'text/javascript',
+    '.json': 'application/json',
+    '.mjs': 'text/javascript'
+};
+
+const server = createServer(async (req, res) => {
+    const url = new URL(req.url, `http://127.0.0.1:${PORT}`);
+    let path = normalize(url.pathname).replace(/^(\.\.[/\\])+/, '');
+    if (path.endsWith('/')) {
+        path = `${path}index.html`;
+    }
+    try {
+        const body = await readFile(join(ROOT, path));
+        res.writeHead(200, {
+            'Content-Type': MIME[extname(path)] ?? 'application/octet-stream'
+        });
+        res.end(body);
+    } catch {
+        res.writeHead(404);
+        res.end('not found');
+    }
+});
+
+server.listen(PORT, '127.0.0.1', () => {
+    console.log(`harness at http://127.0.0.1:${PORT}/pbt/harness/`);
+});
diff --git a/yarn.lock b/yarn.lock
index f700229b4..4a39ac6c6 100644
--- a/yarn.lock
+++ b/yarn.lock
@@ -7,6 +7,11 @@
   resolved "https://registry.npmjs.org/@aashutoshrathi/word-wrap/-/word-wrap-1.2.6.tgz"
   integrity sha512-1Yjs2SvM8TflER/OD3cOjhWWOZb58A2t7wpE2S9XfBYTiIl+XFhQG2bjy4Pu1I+EAlCNUzRDYDdFwFYUKvXcIA==
 
+"@antithesishq/bombadil@0.6.1":
+  version "0.6.1"
+  resolved "https://registry.yarnpkg.com/@antithesishq/bombadil/-/bombadil-0.6.1.tgz#89c442de80879940497e31e53ae98c57f019b9bd"
+  integrity sha512-d1iufG3MI7gSMSiSmMeNdcMW+qR0yQXL2zdkVynC3n3DYgFJYlYXKUQzygmqU12m4RWlR5iOdQU1hsx5UT6+IA==
+
 "@asamuzakjp/css-color@^6.0.5":
   version "6.0.5"
   resolved "https://registry.yarnpkg.com/@asamuzakjp/css-color/-/css-color-6.0.5.tgz#f4edcf3295e5fdee655fce3bcd11ce09411089d8"

From 220cc4d092e59f1ff5e79ad9c953f55abe9913c4 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 15:13:26 -0400
Subject: [PATCH 10/16] test: bombadil spec, runner, and yarn test:pbt wiring

Adds pbt/spec.ts (properties: no PIN leakage, chip count matches model,
pushed names eventually render, suspended state eventually shows its
banner, plus a shadow-DOM-aware click action generator) and pbt/run.mjs
(spawns the static server, drives `bombadil browser test`, propagates
its exit code). Wires yarn test:pbt, extends lint to ./pbt, and adds
pbt/spec.ts to the tsconfig include so type-aware eslint can check it.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Wvy9UfQtNuvz1qqbEFYoB7
---
 .eslintrc.cjs |   6 +++
 .gitignore    |   1 +
 package.json  |   5 +-
 pbt/run.mjs   |  39 ++++++++++++++
 pbt/spec.ts   | 139 ++++++++++++++++++++++++++++++++++++++++++++++++++
 tsconfig.json |   3 +-
 6 files changed, 190 insertions(+), 3 deletions(-)
 create mode 100644 pbt/run.mjs
 create mode 100644 pbt/spec.ts

diff --git a/.eslintrc.cjs b/.eslintrc.cjs
index ed448eb4a..877995c9d 100644
--- a/.eslintrc.cjs
+++ b/.eslintrc.cjs
@@ -30,6 +30,12 @@ module.exports = {
                 'import/no-extraneous-dependencies': 'off', // Test deps (vitest, etc.) are devDependencies
                 'sort-keys': 'off'                          // Test objects are ordered for readability, not alphabetically
             }
+        },
+        {
+            files: ['pbt/**/*.ts'],
+            rules: {
+                'import/no-extraneous-dependencies': 'off' // bombadil is a devDependency
+            }
         }
     ],
     parser: '@typescript-eslint/parser',
diff --git a/.gitignore b/.gitignore
index ec8543025..568fc1dfa 100644
--- a/.gitignore
+++ b/.gitignore
@@ -23,3 +23,4 @@ docs/
 .github/hooks/
 .opencode/
 junit.xml
+pbt-output/
diff --git a/package.json b/package.json
index 7e17ab570..57662e56a 100644
--- a/package.json
+++ b/package.json
@@ -14,11 +14,12 @@
   "scripts": {
     "build": "yarn install ; rollup -c",
     "watch": "rollup -c --watch",
-    "lint": "eslint --ext .ts ./ts",
+    "lint": "eslint --ext .ts ./ts ./pbt",
     "lint:fix": "yarn lint --fix",
     "test": "vitest run",
     "test:watch": "vitest",
-    "test:coverage": "vitest run --coverage"
+    "test:coverage": "vitest run --coverage",
+    "test:pbt": "yarn build ; node pbt/run.mjs"
   },
   "dependencies": {
     "@mdi/js": "^7.4.47",
diff --git a/pbt/run.mjs b/pbt/run.mjs
new file mode 100644
index 000000000..f250be508
--- /dev/null
+++ b/pbt/run.mjs
@@ -0,0 +1,39 @@
+/**
+ * Orchestrates a Bombadil run: start the static server, explore, clean up.
+ * Env knobs: BOMBADIL_TIME_LIMIT (default 60s), BOMBADIL_HEADLESS=1,
+ * PBT_PORT (default 8199).
+ * Exit code follows bombadil: 0 = clean, 2 = property violation.
+ */
+import { spawn } from 'node:child_process';
+import { setTimeout as sleep } from 'node:timers/promises';
+
+const PORT = Number(process.env.PBT_PORT ?? 8199);
+const TIME_LIMIT = process.env.BOMBADIL_TIME_LIMIT ?? '60s';
+const HEADLESS = process.env.BOMBADIL_HEADLESS === '1' || process.env.CI === 'true';
+
+const server = spawn('node', ['pbt/serve.mjs'], { stdio: 'inherit' });
+await sleep(500);
+
+const args = [
+    'browser',
+    'test',
+    `http://127.0.0.1:${PORT}/pbt/harness/`,
+    'pbt/spec.ts',
+    `--time-limit=${TIME_LIMIT}`,
+    '--exit-on-violation',
+    '--output-path=pbt-output',
+    '--output-path-overwrite'
+];
+if (HEADLESS) {
+    args.push('--headless');
+}
+if (process.env.CI === 'true') {
+    args.push('--no-sandbox');
+}
+
+const bombadil = spawn('node_modules/.bin/bombadil', args, { stdio: 'inherit' });
+const exitCode = await new Promise((resolve) => {
+    bombadil.on('exit', (code) => resolve(code ?? 1));
+});
+server.kill();
+process.exit(exitCode);
diff --git a/pbt/spec.ts b/pbt/spec.ts
new file mode 100644
index 000000000..98524948b
--- /dev/null
+++ b/pbt/spec.ts
@@ -0,0 +1,139 @@
+/**
+ * Bombadil specification for the Lock Code Manager card harness.
+ *
+ * Run via `yarn test:pbt`. Extractors run inside the browser; they must
+ * walk shadow roots explicitly because Lit renders into (open) shadow DOM,
+ * which document-level queries and innerText do not pierce.
+ */
+/* eslint-disable no-underscore-dangle -- window.__lcmHarness is the harness's fixed extractor surface */
+import { always, eventually, now } from '@antithesishq/bombadil';
+import { actions, extract } from '@antithesishq/bombadil/browser';
+
+export * from '@antithesishq/bombadil/browser/defaults';
+
+/** Recursively collect visible text across light and shadow DOM. */
+function deepText(root: Element | ShadowRoot): string {
+    let text = '';
+    for (const el of root.querySelectorAll('*')) {
+        if (el.shadowRoot) {
+            text += deepText(el.shadowRoot);
+        }
+    }
+    text += root.textContent ?? '';
+    return text;
+}
+
+/** Recursively collect elements matching a selector across shadow roots. */
+function deepQueryAll(root: Element | Document | ShadowRoot, selector: string): Element[] {
+    const found = [...root.querySelectorAll(selector)];
+    for (const el of root.querySelectorAll('*')) {
+        if (el.shadowRoot) {
+            found.push(...deepQueryAll(el.shadowRoot, selector));
+        }
+    }
+    return found;
+}
+
+declare global {
+    interface Window {
+        __lcmHarness: {
+            model: {
+                revision: number;
+                slots: Record<
+                    string,
+                    {
+                        active: boolean;
+                        enabled: boolean;
+                        inSync: boolean;
+                        name: string;
+                        pin: string;
+                    }
+                >;
+                suspended: boolean;
+            };
+            secretPins: () => string[];
+        };
+    }
+}
+
+const maskedZoneText = extract((state) => {
+    const zone = state.document.querySelector('#masked-zone');
+    return zone ? deepText(zone) : '';
+});
+
+const lockCodesChipCount = extract((state) => {
+    const zone = state.document.querySelector('#lock-codes-zone');
+    return zone ? deepQueryAll(zone, '.slot-chip').length : -1;
+});
+
+const secretPins = extract((state) => state.window.__lcmHarness.secretPins());
+
+const modelSlotCount = extract(
+    (state) => Object.keys(state.window.__lcmHarness.model.slots).length
+);
+
+const modelNames = extract((state) =>
+    Object.values(state.window.__lcmHarness.model.slots).map((slot) => slot.name)
+);
+
+const cardText = extract((state) => deepText(state.document.body));
+
+/** Masked cards must never render a secret PIN as cleartext. */
+export const maskedPinNeverLeaks = always(() =>
+    secretPins.current.every((pin) => !maskedZoneText.current.includes(pin))
+);
+
+/** The lock-codes card renders exactly one chip per model slot. */
+export const chipCountMatchesModel = always(() =>
+    lockCodesChipCount.current === -1 ? true : lockCodesChipCount.current === modelSlotCount.current
+);
+
+/** Subscription liveness: pushed names eventually appear in the DOM. */
+export const namesEventuallyRendered = always(() => {
+    const names = modelNames.current;
+    return now(() => names.length > 0).implies(
+        eventually(() => names.every((name) => cardText.current.includes(name))).within(
+            10,
+            'seconds'
+        )
+    );
+});
+
+const modelSuspended = extract((state) => state.window.__lcmHarness.model.suspended);
+
+const suspendedBannerVisible = extract((state) => {
+    const zone = state.document.querySelector('#lock-codes-zone');
+    return zone ? deepQueryAll(zone, '.suspended-banner').length > 0 : false;
+});
+
+/** Closest drivable "unavailable treatment": suspended state shows its banner. */
+export const suspendedStateEventuallyShowsBanner = always(() =>
+    now(() => modelSuspended.current).implies(
+        eventually(() => suspendedBannerVisible.current || !modelSuspended.current).within(
+            10,
+            'seconds'
+        )
+    )
+);
+
+/** Click chaos-panel buttons and card-internal (shadow DOM) buttons. */
+const clickablePoints = extract((state) => {
+    const points: { name: string; x: number; y: number }[] = [];
+    for (const el of deepQueryAll(state.document, 'button')) {
+        const rect = el.getBoundingClientRect();
+        if (rect.width > 0 && rect.height > 0) {
+            points.push({
+                name: el.id || el.textContent?.trim().slice(0, 24) || 'button',
+                x: rect.left + rect.width / 2,
+                y: rect.top + rect.height / 2
+            });
+        }
+    }
+    return points;
+});
+
+export const clickButtons = actions(() =>
+    clickablePoints.current.map(({ name, x, y }) => {
+        return { Click: { name, point: { x, y } } };
+    })
+);
diff --git a/tsconfig.json b/tsconfig.json
index fa69a7aee..64e60b608 100644
--- a/tsconfig.json
+++ b/tsconfig.json
@@ -18,6 +18,7 @@
     ".eslintrc.cjs",
     "tsconfig.json",
     "rollup.config.js",
-    "vitest.config.ts"
+    "vitest.config.ts",
+    "pbt/spec.ts"
   ]
 }

From 1b1d656cec8e4f229bab612df46a7ac8dccdf73e Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 15:16:52 -0400
Subject: [PATCH 11/16] test: scope bombadil spec type resolution to a pbt
 tsconfig

Root tsconfig uses moduleResolution: node (node10), which cannot see
Bombadil's package.json exports subpaths, so pbt/spec.ts type-checked
as implicit-any everywhere. pbt/tsconfig.json extends the root config
with moduleResolution: bundler (contained to pbt/, root untouched) and
points eslint's type-aware parser at it for pbt/**/*.ts.

Switching resolution strategies surfaces a real bug in
@antithesishq/bombadil 0.6.1's own shipped types: actions.d.ts
re-exports randomRange from random.d.ts, which never declares it.
node10 resolution never reached these files at all, silently masking
it. skipLibCheck avoids failing our build on a declaration file we
don't own.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Wvy9UfQtNuvz1qqbEFYoB7
---
 .eslintrc.cjs     |  3 +++
 pbt/tsconfig.json | 10 ++++++++++
 tsconfig.json     |  3 +--
 3 files changed, 14 insertions(+), 2 deletions(-)
 create mode 100644 pbt/tsconfig.json

diff --git a/.eslintrc.cjs b/.eslintrc.cjs
index 877995c9d..93276b7df 100644
--- a/.eslintrc.cjs
+++ b/.eslintrc.cjs
@@ -33,6 +33,9 @@ module.exports = {
         },
         {
             files: ['pbt/**/*.ts'],
+            parserOptions: {
+                project: ['./pbt/tsconfig.json']
+            },
             rules: {
                 'import/no-extraneous-dependencies': 'off' // bombadil is a devDependency
             }
diff --git a/pbt/tsconfig.json b/pbt/tsconfig.json
new file mode 100644
index 000000000..625018296
--- /dev/null
+++ b/pbt/tsconfig.json
@@ -0,0 +1,10 @@
+{
+    "extends": "../tsconfig.json",
+    "compilerOptions": {
+        "module": "ESNext",
+        "moduleResolution": "bundler",
+        "noEmit": true,
+        "skipLibCheck": true
+    },
+    "include": ["spec.ts"]
+}
diff --git a/tsconfig.json b/tsconfig.json
index 64e60b608..fa69a7aee 100644
--- a/tsconfig.json
+++ b/tsconfig.json
@@ -18,7 +18,6 @@
     ".eslintrc.cjs",
     "tsconfig.json",
     "rollup.config.js",
-    "vitest.config.ts",
-    "pbt/spec.ts"
+    "vitest.config.ts"
   ]
 }

From 2d582e964247b44cafd2409b45e5b6f9a0b812cb Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 15:27:19 -0400
Subject: [PATCH 12/16] test: fix pin-collision flake and harden bombadil
 harness infrastructure

- harness.js chaos-rename: digit-free labels (letters instead of the
  numeric revision) so a rename can never collide with a live secret
  PIN and falsely trip maskedPinNeverLeaks; harden the property itself
  with digit-boundary regex matching instead of raw substring includes
- deepText: join shadow-root chunks with a newline so adjacent text
  nodes can't fuse into a spurious digit run across a shadow boundary
- run.mjs: listen for the bombadil child process's 'error' event (e.g.
  ENOENT) so a failed launch resolves the exit promise instead of
  hanging forever and leaking the static server
- package.json: test:pbt now uses && so a failed build doesn't
  property-test a stale bundle
- namesEventuallyRendered: read modelNames inside the eventually thunk
  so the pending obligation tracks the current model, not a stale
  snapshot from when the formula was first evaluated
- harness.js chaos-add-slot: reuse the lowest free slot in 1..6 instead
  of max+1, which saturated permanently and let chaos coverage decay
- spec.ts extractors: optional-chain window.__lcmHarness with safe
  defaults so a sample taken before harness.js runs doesn't crash
- serve.mjs: resolve ROOT with fileURLToPath instead of raw pathname
  (percent-encoding breaks paths with spaces), and answer /favicon.ico
  with 204 before attempting a file read, since a 404 there could trip
  bombadil's default noHttpErrorCodes property in headed runs

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Wvy9UfQtNuvz1qqbEFYoB7
---
 package.json           |  2 +-
 pbt/harness/harness.js |  8 +++++---
 pbt/run.mjs            |  4 ++++
 pbt/serve.mjs          |  8 +++++++-
 pbt/spec.ts            | 33 +++++++++++++++++----------------
 5 files changed, 34 insertions(+), 21 deletions(-)

diff --git a/package.json b/package.json
index 57662e56a..c5c24a354 100644
--- a/package.json
+++ b/package.json
@@ -19,7 +19,7 @@
     "test": "vitest run",
     "test:watch": "vitest",
     "test:coverage": "vitest run --coverage",
-    "test:pbt": "yarn build ; node pbt/run.mjs"
+    "test:pbt": "yarn build && node pbt/run.mjs"
   },
   "dependencies": {
     "@mdi/js": "^7.4.47",
diff --git a/pbt/harness/harness.js b/pbt/harness/harness.js
index db5378d2f..2f35f67d0 100644
--- a/pbt/harness/harness.js
+++ b/pbt/harness/harness.js
@@ -169,8 +169,8 @@ function randomSlotNum() {
 
 const chaosHandlers = {
     'chaos-add-slot': () => {
-        const next = Math.max(0, ...Object.keys(model.slots).map(Number)) + 1;
-        if (next <= 6) {
+        const next = [1, 2, 3, 4, 5, 6].find((n) => !model.slots[n]);
+        if (next) {
             model.slots[next] = {
                 active: true,
                 enabled: true,
@@ -191,7 +191,9 @@ const chaosHandlers = {
     },
     'chaos-rename': () => {
         const slot = model.slots[randomSlotNum()];
-        slot.name = `Renamed ${model.revision}`;
+        // Digit-free label: a numeric revision could collide with a live
+        // secret PIN and falsely trip the no-leak property.
+        slot.name = `Renamed ${String(model.revision).replace(/\d/g, (d) => 'ABCDEFGHIJ'[Number(d)])}`;
     },
     'chaos-toggle-active': () => {
         const slot = model.slots[randomSlotNum()];
diff --git a/pbt/run.mjs b/pbt/run.mjs
index f250be508..33d317fd3 100644
--- a/pbt/run.mjs
+++ b/pbt/run.mjs
@@ -33,6 +33,10 @@ if (process.env.CI === 'true') {
 
 const bombadil = spawn('node_modules/.bin/bombadil', args, { stdio: 'inherit' });
 const exitCode = await new Promise((resolve) => {
+    bombadil.on('error', (err) => {
+        console.error('failed to launch bombadil:', err);
+        resolve(1);
+    });
     bombadil.on('exit', (code) => resolve(code ?? 1));
 });
 server.kill();
diff --git a/pbt/serve.mjs b/pbt/serve.mjs
index 072c802a2..682f6d5be 100644
--- a/pbt/serve.mjs
+++ b/pbt/serve.mjs
@@ -2,8 +2,9 @@
 import { createServer } from 'node:http';
 import { readFile } from 'node:fs/promises';
 import { extname, join, normalize } from 'node:path';
+import { fileURLToPath } from 'node:url';
 
-const ROOT = new URL('..', import.meta.url).pathname;
+const ROOT = fileURLToPath(new URL('..', import.meta.url));
 const PORT = Number(process.env.PBT_PORT ?? 8199);
 const MIME = {
     '.css': 'text/css',
@@ -15,6 +16,11 @@ const MIME = {
 
 const server = createServer(async (req, res) => {
     const url = new URL(req.url, `http://127.0.0.1:${PORT}`);
+    if (url.pathname === '/favicon.ico') {
+        res.writeHead(204);
+        res.end();
+        return;
+    }
     let path = normalize(url.pathname).replace(/^(\.\.[/\\])+/, '');
     if (path.endsWith('/')) {
         path = `${path}index.html`;
diff --git a/pbt/spec.ts b/pbt/spec.ts
index 98524948b..58af9e948 100644
--- a/pbt/spec.ts
+++ b/pbt/spec.ts
@@ -16,7 +16,9 @@ function deepText(root: Element | ShadowRoot): string {
     let text = '';
     for (const el of root.querySelectorAll('*')) {
         if (el.shadowRoot) {
-            text += deepText(el.shadowRoot);
+            // Join with a separator so text nodes straddling a shadow
+            // boundary can't fuse into a digit run that isn't really there.
+            text += `${deepText(el.shadowRoot)}\n`;
         }
     }
     text += root.textContent ?? '';
@@ -36,7 +38,7 @@ function deepQueryAll(root: Element | Document | ShadowRoot, selector: string):
 
 declare global {
     interface Window {
-        __lcmHarness: {
+        __lcmHarness?: {
             model: {
                 revision: number;
                 slots: Record<
@@ -66,21 +68,23 @@ const lockCodesChipCount = extract((state) => {
     return zone ? deepQueryAll(zone, '.slot-chip').length : -1;
 });
 
-const secretPins = extract((state) => state.window.__lcmHarness.secretPins());
+const secretPins = extract((state) => state.window.__lcmHarness?.secretPins() ?? []);
 
 const modelSlotCount = extract(
-    (state) => Object.keys(state.window.__lcmHarness.model.slots).length
+    (state) => Object.keys(state.window.__lcmHarness?.model.slots ?? {}).length
 );
 
 const modelNames = extract((state) =>
-    Object.values(state.window.__lcmHarness.model.slots).map((slot) => slot.name)
+    Object.values(state.window.__lcmHarness?.model.slots ?? {}).map((slot) => slot.name)
 );
 
 const cardText = extract((state) => deepText(state.document.body));
 
 /** Masked cards must never render a secret PIN as cleartext. */
 export const maskedPinNeverLeaks = always(() =>
-    secretPins.current.every((pin) => !maskedZoneText.current.includes(pin))
+    secretPins.current.every(
+        (pin) => !new RegExp(`(?<!\\d)${pin}(?!\\d)`).test(maskedZoneText.current)
+    )
 );
 
 /** The lock-codes card renders exactly one chip per model slot. */
@@ -89,17 +93,14 @@ export const chipCountMatchesModel = always(() =>
 );
 
 /** Subscription liveness: pushed names eventually appear in the DOM. */
-export const namesEventuallyRendered = always(() => {
-    const names = modelNames.current;
-    return now(() => names.length > 0).implies(
-        eventually(() => names.every((name) => cardText.current.includes(name))).within(
-            10,
-            'seconds'
-        )
-    );
-});
+export const namesEventuallyRendered = always(() =>
+    eventually(() => modelNames.current.every((name) => cardText.current.includes(name))).within(
+        10,
+        'seconds'
+    )
+);
 
-const modelSuspended = extract((state) => state.window.__lcmHarness.model.suspended);
+const modelSuspended = extract((state) => state.window.__lcmHarness?.model.suspended ?? false);
 
 const suspendedBannerVisible = extract((state) => {
     const zone = state.document.querySelector('#lock-codes-zone');

From 64b64b1a6dc85f9d62090cb2e35be7aa79230315 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 15:29:31 -0400
Subject: [PATCH 13/16] ci: nightly bombadil exploration workflow

---
 .github/workflows/bombadil.yml | 37 ++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 .github/workflows/bombadil.yml

diff --git a/.github/workflows/bombadil.yml b/.github/workflows/bombadil.yml
new file mode 100644
index 000000000..b8cc9f0e1
--- /dev/null
+++ b/.github/workflows/bombadil.yml
@@ -0,0 +1,37 @@
+---
+name: Bombadil property tests
+
+# GHA requires bare `on:` which yamllint sees as boolean
+# yamllint disable-line rule:truthy
+on:
+  schedule:
+    - cron: "17 8 * * *"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  bombadil:
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@v7
+      - name: Set up Node
+        uses: actions/setup-node@v7
+        with:
+          node-version: lts/jod
+          cache: yarn
+      - name: Install dependencies
+        run: yarn install --frozen-lockfile
+      - name: Run Bombadil exploration
+        env:
+          BOMBADIL_HEADLESS: "1"
+          BOMBADIL_TIME_LIMIT: 5m
+        run: yarn test:pbt
+      - name: Upload trace on violation
+        if: failure()
+        uses: actions/upload-artifact@v4
+        with:
+          name: bombadil-output
+          path: pbt-output/

From 4887101fa96b54787392b6607dd70eb8be7ba5d3 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 15:37:35 -0400
Subject: [PATCH 14/16] test: serve harness page for virtual routes like the
 real single-page frontend

Bombadil's noHttpErrorCodes default property caught a real harness
defect: clicking a lock-codes chip triggers history.pushState to a
virtual Home Assistant route (e.g.
/config/integrations/integration/lock_code_manager#config_entry=...),
and Bombadil's reload action then requests that route directly from
pbt/serve.mjs, which 404s. The real HA frontend is a single-page app
that serves its shell for every route; the harness server now mirrors
that by falling back to pbt/harness/index.html for any extensionless
path, while still 404ing honestly on missing assets (identified by
extension).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Wvy9UfQtNuvz1qqbEFYoB7
---
 pbt/serve.mjs | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/pbt/serve.mjs b/pbt/serve.mjs
index 682f6d5be..c6e628c74 100644
--- a/pbt/serve.mjs
+++ b/pbt/serve.mjs
@@ -25,6 +25,14 @@ const server = createServer(async (req, res) => {
     if (path.endsWith('/')) {
         path = `${path}index.html`;
     }
+    // The cards navigate via history.pushState to virtual Home Assistant
+    // routes (e.g. /config/integrations/...), and a browser reload then
+    // requests that route from this server. Serve the harness page for any
+    // extensionless path — mirroring the real frontend's single-page-app
+    // routing — while keeping honest 404s for missing assets.
+    if (!extname(path)) {
+        path = '/pbt/harness/index.html';
+    }
     try {
         const body = await readFile(join(ROOT, path));
         res.writeHead(200, {

From 14511d55504578f6a80bf9778e23fae4539f3933 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 15:40:11 -0400
Subject: [PATCH 15/16] docs: property-based testing guidance in AGENTS.md

---
 AGENTS.md | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/AGENTS.md b/AGENTS.md
index 254f7ce60..7db116408 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -316,6 +316,29 @@ tests/providers/
 - Provider `async_setup` must be idempotent — tests verify it can be called multiple times.
 - Don't use `MagicMock()` for coordinators when the real coordinator can be used.
 
+## Property-based testing
+
+Two complementary layers exist alongside the example-based suites:
+
+- **Python (Hypothesis)** — `tests/properties/` runs as part of the normal
+  `pytest tests/` invocation. The default `dev` profile uses 15 examples to
+  keep the suite fast; CI sets `HYPOTHESIS_PROFILE=ci` (200 examples). Run
+  the deep profile locally with `HYPOTHESIS_PROFILE=ci pytest tests/properties/`.
+  `test_credential_machine.py` is a stateful machine driving the real
+  BaseLock write orchestration against `MockLCMLock`.
+- **TypeScript (Bombadil)** — `pbt/` contains a browser harness that mounts
+  the built cards with a scripted mock `hass` plus a chaos panel, and a
+  Bombadil spec (`pbt/spec.ts`) with temporal-logic properties (no PIN leaks
+  from masked cards, chip counts match the model, pushed data eventually
+  renders). Run locally with `yarn test:pbt` (env knobs:
+  `BOMBADIL_TIME_LIMIT`, `BOMBADIL_HEADLESS=1`). CI runs it nightly and on
+  manual dispatch (`bombadil.yml`), never on pull requests. Inspect
+  violations with `yarn node_modules/.bin/bombadil browser inspect pbt-output`.
+
+Counterexample triage: a found counterexample is a deliverable. Either fix
+the code, or — only for documented contract edges — narrow the strategy
+with a comment citing the contract. Never silence one by rerunning.
+
 ## Adding Lock Provider Support
 
 1. Create new file in `providers/` (e.g., `my_provider.py`)

From 951cfe990f26f643ebf79568e65bb01be89129e8 Mon Sep 17 00:00:00 2001
From: raman325 <7243222+raman325@users.noreply.github.com>
Date: Fri, 31 Jul 2026 15:45:01 -0400
Subject: [PATCH 16/16] docs: correct bombadil inspect command and silence
 hypothesis directory warning

---
 AGENTS.md      | 2 +-
 pyproject.toml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/AGENTS.md b/AGENTS.md
index 7db116408..9ed9b407a 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -333,7 +333,7 @@ Two complementary layers exist alongside the example-based suites:
   renders). Run locally with `yarn test:pbt` (env knobs:
   `BOMBADIL_TIME_LIMIT`, `BOMBADIL_HEADLESS=1`). CI runs it nightly and on
   manual dispatch (`bombadil.yml`), never on pull requests. Inspect
-  violations with `yarn node_modules/.bin/bombadil browser inspect pbt-output`.
+  violations with `yarn bombadil browser inspect pbt-output`.
 
 Counterexample triage: a found counterexample is a deliverable. Either fix
 the code, or — only for documented contract edges — narrow the strategy
diff --git a/pyproject.toml b/pyproject.toml
index d2539dd5d..b3c0c613f 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -136,7 +136,7 @@ overgeneral-exceptions = ["BaseException", "Exception", "HomeAssistantError"]
 asyncio_mode = "auto"
 asyncio_default_fixture_loop_scope = "function"
 testpaths = ["tests"]
-norecursedirs = [".git", "testing_config"]
+norecursedirs = [".git", "testing_config", ".hypothesis"]
 
 [tool.mypy]
 ignore_missing_imports = true