diff --git a/Cargo.lock b/Cargo.lock
index 81e8df48..a6ee2860 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -24,6 +24,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5a15f179cd60c4584b8a8c596927aadc462e27f2ca70c04e0071964a73ba7a75"
 dependencies = [
  "cfg-if",
+ "getrandom 0.3.3",
  "once_cell",
  "version_check",
  "zerocopy",
@@ -71,6 +72,12 @@ dependencies = [
  "rustversion",
 ]
 
+[[package]]
+name = "ascii"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d92bec98840b8f03a5ff5413de5293bfcd8bf96467cf5452609f939ec6f5de16"
+
 [[package]]
 name = "async-stream"
 version = "0.3.6"
@@ -335,6 +342,18 @@ version = "1.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268"
 
+[[package]]
+name = "choice"
+version = "0.0.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a3b71fc821deaf602a933ada5c845d088156d0cdf2ebf43ede390afe93466553"
+
+[[package]]
+name = "chunked_transfer"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6e4de3bc4ea267985becf712dc6d9eed8b04c953b3fcfb339ebc87acd9804901"
+
 [[package]]
 name = "ciborium"
 version = "0.2.2"
@@ -1144,6 +1163,12 @@ dependencies = [
  "syn 2.0.104",
 ]
 
+[[package]]
+name = "id-set"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9633fadf6346456cf8531119ba4838bc6d82ac4ce84d9852126dd2aa34d49264"
+
 [[package]]
 name = "indexmap"
 version = "2.10.0"
@@ -1502,6 +1527,12 @@ dependencies = [
  "smallvec",
 ]
 
+[[package]]
+name = "nohash-hasher"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2bf50223579dc7cdcfb3bfcacf7069ff68243f8c363f62ffa99cf000a6b9c451"
+
 [[package]]
 name = "nom"
 version = "7.1.3"
@@ -2472,6 +2503,26 @@ dependencies = [
  "windows-sys 0.59.0",
 ]
 
+[[package]]
+name = "stateright"
+version = "0.31.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fd1157f21b11916f90fe1f2ac9a8d0e09a8813b28701584141060f414eedf6ba"
+dependencies = [
+ "ahash",
+ "choice",
+ "crossbeam-utils",
+ "dashmap",
+ "id-set",
+ "log",
+ "nohash-hasher",
+ "parking_lot",
+ "rand",
+ "serde",
+ "serde_json",
+ "tiny_http",
+]
+
 [[package]]
 name = "static_assertions"
 version = "1.1.0"
@@ -2593,6 +2644,18 @@ dependencies = [
  "cfg-if",
 ]
 
+[[package]]
+name = "tiny_http"
+version = "0.12.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "389915df6413a2e74fb181895f933386023c71110878cd0825588928e64cdc82"
+dependencies = [
+ "ascii",
+ "chunked_transfer",
+ "httpdate",
+ "log",
+]
+
 [[package]]
 name = "tinystr"
 version = "0.8.2"
@@ -3426,6 +3489,15 @@ dependencies = [
  "wireframe_testing",
 ]
 
+[[package]]
+name = "wireframe-verification"
+version = "0.1.0"
+dependencies = [
+ "rstest 0.26.1",
+ "stateright",
+ "wireframe",
+]
+
 [[package]]
 name = "wireframe_testing"
 version = "0.3.0"
diff --git a/Cargo.toml b/Cargo.toml
index d4ce8475..edf6dbe0 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -11,7 +11,7 @@ categories = ["network-programming", "asynchronous"]
 documentation = "https://docs.rs/wireframe"
 
 [workspace]
-members = ["."]
+members = [".", "crates/wireframe-verification"]
 default-members = ["."]
 resolver = "3"
 
diff --git a/crates/wireframe-verification/Cargo.toml b/crates/wireframe-verification/Cargo.toml
new file mode 100644
index 00000000..ab8f038b
--- /dev/null
+++ b/crates/wireframe-verification/Cargo.toml
@@ -0,0 +1,12 @@
+[package]
+name = "wireframe-verification"
+version = "0.1.0"
+edition = "2024"
+publish = false
+
+[dependencies]
+stateright = "0.31.0"
+wireframe = { path = "../..", features = ["test-support"] }
+
+[dev-dependencies]
+rstest = "0.26.1"
diff --git a/crates/wireframe-verification/src/connection_model/action.rs b/crates/wireframe-verification/src/connection_model/action.rs
new file mode 100644
index 00000000..24e59295
--- /dev/null
+++ b/crates/wireframe-verification/src/connection_model/action.rs
@@ -0,0 +1,15 @@
+//! Actions in the placeholder connection-actor model.
+
+/// Nondeterministic events for the placeholder connection model.
+#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
+pub enum ConnectionAction {
+    EnqueueHigh,
+    EnqueueLow,
+    InstallResponse,
+    InstallMultiPacket,
+    EmitQueued,
+    EmitActiveFrame,
+    CompleteActiveOutput,
+    Shutdown,
+    TickFairness,
+}
diff --git a/crates/wireframe-verification/src/connection_model/mod.rs b/crates/wireframe-verification/src/connection_model/mod.rs
new file mode 100644
index 00000000..9beb88ef
--- /dev/null
+++ b/crates/wireframe-verification/src/connection_model/mod.rs
@@ -0,0 +1,14 @@
+//! Placeholder Stateright model for the connection actor roadmap.
+//!
+//! The first milestone keeps the model intentionally small: it exercises the
+//! shared harness and encodes a few semantic invariants that later roadmap
+//! items can refine toward the real `ConnectionActor`.
+
+mod action;
+mod model;
+mod properties;
+mod state;
+
+pub use action::ConnectionAction;
+pub use model::PlaceholderConnectionModel;
+pub use state::{ActiveOutput, ConnectionState};
diff --git a/crates/wireframe-verification/src/connection_model/model.rs b/crates/wireframe-verification/src/connection_model/model.rs
new file mode 100644
index 00000000..3d8d5650
--- /dev/null
+++ b/crates/wireframe-verification/src/connection_model/model.rs
@@ -0,0 +1,127 @@
+//! Stateright model implementation for the placeholder connection actor.
+
+use stateright::{Model, Property};
+
+use super::{ConnectionAction, ConnectionState, properties::properties, state::ActiveOutput};
+
+/// Small semantic model used to land the verification crate and shared harness.
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub struct PlaceholderConnectionModel {
+    max_steps: u8,
+}
+
+impl Default for PlaceholderConnectionModel {
+    fn default() -> Self { Self { max_steps: 6 } }
+}
+
+impl PlaceholderConnectionModel {
+    /// Create a model with an explicit state-space depth bound.
+    pub fn new(max_steps: u8) -> Self { Self { max_steps } }
+}
+
+impl Model for PlaceholderConnectionModel {
+    type State = ConnectionState;
+    type Action = ConnectionAction;
+
+    fn init_states(&self) -> Vec<Self::State> { vec![ConnectionState::default()] }
+
+    fn actions(&self, _state: &Self::State, actions: &mut Vec<Self::Action>) {
+        actions.extend([
+            ConnectionAction::EnqueueHigh,
+            ConnectionAction::EnqueueLow,
+            ConnectionAction::InstallResponse,
+            ConnectionAction::InstallMultiPacket,
+            ConnectionAction::EmitQueued,
+            ConnectionAction::EmitActiveFrame,
+            ConnectionAction::CompleteActiveOutput,
+            ConnectionAction::Shutdown,
+            ConnectionAction::TickFairness,
+        ]);
+    }
+
+    fn next_state(&self, state: &Self::State, action: Self::Action) -> Option<Self::State> {
+        let mut next = state.clone();
+        next.steps = next.steps.saturating_add(1);
+
+        match action {
+            ConnectionAction::EnqueueHigh if !state.high_priority_queued => {
+                next.high_priority_queued = true;
+                Some(next)
+            }
+            ConnectionAction::EnqueueLow if !state.low_priority_queued => {
+                next.low_priority_queued = true;
+                Some(next)
+            }
+            ConnectionAction::InstallResponse
+                if !state.shutdown_requested
+                    && matches!(state.active_output, ActiveOutput::Idle) =>
+            {
+                next.active_output = ActiveOutput::Response;
+                Some(next)
+            }
+            ConnectionAction::InstallMultiPacket
+                if !state.shutdown_requested
+                    && matches!(state.active_output, ActiveOutput::Idle) =>
+            {
+                next.active_output = ActiveOutput::MultiPacket;
+                next.multi_packet_terminal_count = 0;
+                Some(next)
+            }
+            ConnectionAction::EmitQueued if state.high_priority_queued => {
+                next.high_priority_queued = false;
+                next.emitted_high_priority = true;
+                next.fairness_allows_low = true;
+                Some(next)
+            }
+            ConnectionAction::EmitQueued
+                if state.low_priority_queued
+                    && (!state.high_priority_queued || state.fairness_allows_low) =>
+            {
+                next.low_priority_queued = false;
+                next.emitted_low_priority = true;
+                next.fairness_allows_low = false;
+                Some(next)
+            }
+            ConnectionAction::EmitActiveFrame
+                if !matches!(state.active_output, ActiveOutput::Idle) =>
+            {
+                if state.shutdown_requested {
+                    next.shutdown_during_output = true;
+                }
+                Some(next)
+            }
+            ConnectionAction::CompleteActiveOutput
+                if matches!(state.active_output, ActiveOutput::Response) =>
+            {
+                next.active_output = ActiveOutput::Idle;
+                next.response_completed = true;
+                Some(next)
+            }
+            ConnectionAction::CompleteActiveOutput
+                if matches!(state.active_output, ActiveOutput::MultiPacket) =>
+            {
+                next.active_output = ActiveOutput::Idle;
+                next.multi_packet_completed = true;
+                next.multi_packet_terminal_count =
+                    next.multi_packet_terminal_count.saturating_add(1);
+                Some(next)
+            }
+            ConnectionAction::Shutdown if !state.shutdown_requested => {
+                next.shutdown_requested = true;
+                if !matches!(state.active_output, ActiveOutput::Idle) {
+                    next.shutdown_during_output = true;
+                }
+                Some(next)
+            }
+            ConnectionAction::TickFairness if state.low_priority_queued => {
+                next.fairness_allows_low = true;
+                Some(next)
+            }
+            _ => None,
+        }
+    }
+
+    fn properties(&self) -> Vec<Property<Self>> { properties() }
+
+    fn within_boundary(&self, state: &Self::State) -> bool { state.steps <= self.max_steps }
+}
diff --git a/crates/wireframe-verification/src/connection_model/properties.rs b/crates/wireframe-verification/src/connection_model/properties.rs
new file mode 100644
index 00000000..b8f7a0e7
--- /dev/null
+++ b/crates/wireframe-verification/src/connection_model/properties.rs
@@ -0,0 +1,69 @@
+//! Properties checked against the placeholder connection model.
+
+use stateright::Property;
+
+use super::{ConnectionState, PlaceholderConnectionModel};
+
+pub(super) fn properties() -> Vec<Property<PlaceholderConnectionModel>> {
+    vec![
+        Property::always(
+            "active output remains exclusive",
+            active_output_is_exclusive,
+        ),
+        Property::always(
+            "multi-packet terminator stays single",
+            multi_packet_terminator_is_single,
+        ),
+        Property::sometimes(
+            "high-priority output can make progress",
+            high_priority_progress,
+        ),
+        Property::sometimes(
+            "low-priority output can make progress",
+            low_priority_progress,
+        ),
+        Property::sometimes("response output can complete", response_completion),
+        Property::sometimes("multi-packet output can complete", multi_packet_completion),
+        Property::sometimes(
+            "shutdown can race an active output",
+            shutdown_races_active_output,
+        ),
+    ]
+}
+
+fn active_output_is_exclusive(
+    _model: &PlaceholderConnectionModel,
+    _state: &ConnectionState,
+) -> bool {
+    true
+}
+
+fn multi_packet_terminator_is_single(
+    _model: &PlaceholderConnectionModel,
+    state: &ConnectionState,
+) -> bool {
+    state.multi_packet_terminal_count <= 1
+}
+
+fn high_priority_progress(_model: &PlaceholderConnectionModel, state: &ConnectionState) -> bool {
+    state.emitted_high_priority
+}
+
+fn low_priority_progress(_model: &PlaceholderConnectionModel, state: &ConnectionState) -> bool {
+    state.emitted_low_priority
+}
+
+fn response_completion(_model: &PlaceholderConnectionModel, state: &ConnectionState) -> bool {
+    state.response_completed
+}
+
+fn multi_packet_completion(_model: &PlaceholderConnectionModel, state: &ConnectionState) -> bool {
+    state.multi_packet_completed
+}
+
+fn shutdown_races_active_output(
+    _model: &PlaceholderConnectionModel,
+    state: &ConnectionState,
+) -> bool {
+    state.shutdown_during_output
+}
diff --git a/crates/wireframe-verification/src/connection_model/state.rs b/crates/wireframe-verification/src/connection_model/state.rs
new file mode 100644
index 00000000..d7bb95b1
--- /dev/null
+++ b/crates/wireframe-verification/src/connection_model/state.rs
@@ -0,0 +1,30 @@
+//! State for the placeholder connection-actor model.
+
+/// Active output tracked by the placeholder model.
+#[derive(Clone, Copy, Debug, Default, Eq, Hash, PartialEq)]
+pub enum ActiveOutput {
+    /// No response or multi-packet output is currently active.
+    #[default]
+    Idle,
+    /// A response stream is active.
+    Response,
+    /// A multi-packet stream is active.
+    MultiPacket,
+}
+
+/// Model state for the placeholder connection-actor abstraction.
+#[derive(Clone, Debug, Default, Eq, Hash, PartialEq)]
+pub struct ConnectionState {
+    pub(crate) steps: u8,
+    pub(crate) high_priority_queued: bool,
+    pub(crate) low_priority_queued: bool,
+    pub(crate) fairness_allows_low: bool,
+    pub(crate) active_output: ActiveOutput,
+    pub(crate) shutdown_requested: bool,
+    pub(crate) emitted_high_priority: bool,
+    pub(crate) emitted_low_priority: bool,
+    pub(crate) response_completed: bool,
+    pub(crate) multi_packet_completed: bool,
+    pub(crate) shutdown_during_output: bool,
+    pub(crate) multi_packet_terminal_count: u8,
+}
diff --git a/crates/wireframe-verification/src/harness.rs b/crates/wireframe-verification/src/harness.rs
new file mode 100644
index 00000000..cfdf4614
--- /dev/null
+++ b/crates/wireframe-verification/src/harness.rs
@@ -0,0 +1,62 @@
+//! Shared Stateright checker helpers for bounded repository validation.
+
+use std::{fmt::Debug, hash::Hash};
+
+use stateright::{Checker, CheckerBuilder, Model};
+
+/// Default maximum depth for repository-local Stateright checks.
+pub const DEFAULT_TARGET_MAX_DEPTH: usize = 8;
+
+/// Default state budget for repository-local Stateright checks.
+pub const DEFAULT_TARGET_STATE_COUNT: usize = 5_000;
+
+/// Bounds applied to a Stateright checker run.
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub struct VerificationBounds {
+    /// Maximum search depth for the checker.
+    pub max_depth: usize,
+    /// Maximum state budget for the checker.
+    pub max_state_count: usize,
+}
+
+impl Default for VerificationBounds {
+    fn default() -> Self {
+        Self {
+            max_depth: DEFAULT_TARGET_MAX_DEPTH,
+            max_state_count: DEFAULT_TARGET_STATE_COUNT,
+        }
+    }
+}
+
+/// Build a repository-standard bounded checker for a model.
+pub fn checker<M>(model: M, bounds: VerificationBounds) -> CheckerBuilder<M>
+where
+    M: Model + Send + Sync + 'static,
+    M::State: Hash + Send + Sync,
+{
+    model
+        .checker()
+        .target_max_depth(bounds.max_depth)
+        .target_state_count(bounds.max_state_count)
+}
+
+/// Run the repository-standard bounded checker and assert every property.
+pub fn assert_model_properties<M>(model: M)
+where
+    M: Model + Send + Sync + 'static,
+    M::Action: Debug + Clone + PartialEq,
+    M::State: Debug + Clone + Hash + PartialEq + Send + Sync + 'static,
+{
+    assert_model_properties_with_bounds(model, VerificationBounds::default());
+}
+
+/// Run a bounded checker with explicit limits and assert every property.
+pub fn assert_model_properties_with_bounds<M>(model: M, bounds: VerificationBounds)
+where
+    M: Model + Send + Sync + 'static,
+    M::Action: Debug + Clone + PartialEq,
+    M::State: Debug + Clone + Hash + PartialEq + Send + Sync + 'static,
+{
+    let checker = checker(model, bounds).spawn_bfs().join();
+    checker.assert_properties();
+}
diff --git a/crates/wireframe-verification/src/lib.rs b/crates/wireframe-verification/src/lib.rs
new file mode 100644
index 00000000..6cef807a
--- /dev/null
+++ b/crates/wireframe-verification/src/lib.rs
@@ -0,0 +1,7 @@
+//! Internal formal-verification models and harnesses for Wireframe.
+//!
+//! This crate stays out of the published API surface while providing a place
+//! for Stateright-based models and reusable bounded-checker helpers.
+
+pub mod connection_model;
+pub mod harness;
diff --git a/crates/wireframe-verification/tests/connection_actor.rs b/crates/wireframe-verification/tests/connection_actor.rs
new file mode 100644
index 00000000..75f9488f
--- /dev/null
+++ b/crates/wireframe-verification/tests/connection_actor.rs
@@ -0,0 +1,12 @@
+//! Integration checks for the placeholder connection-actor model.
+
+use rstest::rstest;
+use wireframe_verification::{
+    connection_model::PlaceholderConnectionModel,
+    harness::assert_model_properties,
+};
+
+#[rstest]
+fn placeholder_connection_model_satisfies_repository_properties() {
+    assert_model_properties(PlaceholderConnectionModel::default());
+}
diff --git a/crates/wireframe-verification/tests/verification_harness.rs b/crates/wireframe-verification/tests/verification_harness.rs
new file mode 100644
index 00000000..f8408449
--- /dev/null
+++ b/crates/wireframe-verification/tests/verification_harness.rs
@@ -0,0 +1,18 @@
+//! Integration checks for the shared verification harness.
+
+use rstest::rstest;
+use wireframe_verification::{
+    connection_model::PlaceholderConnectionModel,
+    harness::{VerificationBounds, assert_model_properties_with_bounds},
+};
+
+#[rstest]
+fn shared_harness_runs_placeholder_model_with_explicit_bounds() {
+    assert_model_properties_with_bounds(
+        PlaceholderConnectionModel::new(6),
+        VerificationBounds {
+            max_depth: 8,
+            max_state_count: 5_000,
+        },
+    );
+}
diff --git a/docs/developers-guide.md b/docs/developers-guide.md
index ca79bb9f..475f6b81 100644
--- a/docs/developers-guide.md
+++ b/docs/developers-guide.md
@@ -86,10 +86,10 @@ set.
 the tuple `(oneshot::Sender<()>, JoinHandle<Result<(), ServerError>>)` that
 `PendingServer` stores between server start-up and explicit shutdown. Naming
 the alias keeps `PendingServer`'s field types readable and makes
-`PendingServer::take` return a self-documenting
-`Option<ServerShutdownHandle>` instead of an opaque inline tuple. Tests that
-call `WireframePair::shutdown()` do not interact with this type directly; it
-is an internal implementation detail of the pair harness.
+`PendingServer::take` return a self-documenting `Option<ServerShutdownHandle>`
+instead of an opaque inline tuple. Tests that call `WireframePair::shutdown()`
+do not interact with this type directly; it is an internal implementation
+detail of the pair harness.
 
 ## Vocabulary normalization outcome (2026-02-20)
 
@@ -118,10 +118,11 @@ continuous integration (CI).
 Wireframe now uses a hybrid root manifest: the repository root `Cargo.toml`
 contains both `[package]` and `[workspace]`.
 
-During roadmap item 10.1.1 the workspace is intentionally staged with only the
-root package as a member and default member:
+After roadmap items 15.1.1 and 15.1.2 the workspace explicitly lists the root
+package and the internal verification crate, while keeping only the root
+package as a default member:
 
-- `members = ["."]`
+- `members = [".", "crates/wireframe-verification"]`
 - `default-members = ["."]`
 
 That means ordinary root-level commands such as `cargo build`, `cargo check`,
@@ -130,14 +131,20 @@ to target the main `wireframe` package by default.
 
 Use plain root-level Cargo commands for day-to-day work on the main crate.
 Reach for `--workspace` when a task is explicitly meant to cover every current
-workspace member, for example repository-wide validation in CI or when later
-roadmap items add internal verification crates.
+workspace member, for example repository-wide validation in CI or when a change
+also touches `crates/wireframe-verification`.
+
+Use `cargo test -p wireframe-verification` to exercise the Stateright crate in
+isolation. The existing `Makefile` targets still focus on the root `wireframe`
+crate because the dedicated formal-verification targets belong to later roadmap
+items.
 
 One Cargo nuance is worth knowing: `cargo metadata` for this repository still
 reports the in-tree helper crate `wireframe_testing` in `workspace_members`
-because it lives under the repository root as a path dependency. That does not
-change day-to-day command ergonomics because `default-members = ["."]` keeps
-plain root-level Cargo commands focused on the main `wireframe` package.
+because it lives under the repository root as a path dependency. That sits
+alongside the explicit `wireframe-verification` member and does not change
+day-to-day command ergonomics because `default-members = ["."]` keeps plain
+root-level Cargo commands focused on the main `wireframe` package.
 
 ### Workspace manifest test support
 
@@ -208,5 +215,4 @@ a fresh handle without explicitly calling the constructor.
 
 `LoggerHandle::new()` tolerates a poisoned mutex: if a prior test panicked
 while holding the logger lock, `new()` recovers the guard via `into_inner()`
-and drains any buffered log records, so the next test starts from a clean
-state.
+and drains any buffered log records, so the next test starts from a clean state.
diff --git a/docs/execplans/15-1-2-wireframe-verification-crate.md b/docs/execplans/15-1-2-wireframe-verification-crate.md
new file mode 100644
index 00000000..b7482428
--- /dev/null
+++ b/docs/execplans/15-1-2-wireframe-verification-crate.md
@@ -0,0 +1,191 @@
+# Add the internal `wireframe-verification` crate
+
+This ExecPlan is a living document. The sections `Constraints`, `Tolerances`,
+`Risks`, `Progress`, `Surprises & Discoveries`, `Decision Log`, and
+`Outcomes & Retrospective` must be kept up to date as work proceeds.
+
+Status: IMPLEMENTED (environment-limited validation)
+
+This document must be maintained in accordance with `AGENTS.md` at the
+repository root, including quality gates, test policy, and documentation style
+requirements.
+
+## Purpose / big picture
+
+Roadmap item 15.1.2 adds `crates/wireframe-verification` as the dedicated home
+for Stateright models and shared bounded-checker helpers.
+
+After this change:
+
+- the root workspace explicitly includes
+  `crates/wireframe-verification`,
+- the root `wireframe` package remains the only default workspace member, so
+  ordinary root `cargo test`, `cargo check`, and `cargo clippy` still target
+  the main crate by default,
+- contributors can run `cargo test -p wireframe-verification` and get a
+  passing placeholder Stateright model backed by a shared harness that later
+  roadmap items can extend toward the real `ConnectionActor`.
+
+Observable success is:
+
+- `cargo metadata --no-deps --format-version 1` reports
+  `wireframe-verification` in `workspace_members`,
+- `cargo test -p wireframe-verification` passes,
+- the workspace-manifest regression tests and BDD coverage reflect the
+  post-15.1.2 contract,
+- `docs/formal-verification-methods-in-wireframe.md`,
+  `docs/developers-guide.md`, and `docs/roadmap.md` reflect the implemented
+  state.
+
+## Constraints
+
+- Keep the root `wireframe` package as the sole `default-members` entry in the
+  root `Cargo.toml`.
+- Keep the new crate internal with `publish = false`.
+- Treat 15.1.2 as crate-and-doc infrastructure only. Do not add Makefile
+  targets, continuous integration plumbing, Kani tooling, or Verus tooling
+  owned by later roadmap items.
+- Keep the first Stateright model intentionally small and semantic. It should
+  prove the crate and harness shape, not attempt a full `ConnectionActor`
+  reimplementation.
+- Use `rstest` for the new crate's automated tests.
+- Keep each Rust file under the 400-line repository cap.
+- Preserve the existing `wireframe_testing` helper-crate explanation in the
+  developer docs while extending it with the new verification-crate behaviour.
+
+## Tolerances (exception triggers)
+
+- If adding the verification crate forces plain root-level Cargo commands to
+  stop targeting the root `wireframe` package by default, stop and reassess.
+- If the Stateright crate requires Makefile or CI changes to be testable
+  locally, stop and defer that plumbing to roadmap items 15.1.4 and 15.1.5.
+- If the placeholder model cannot be expressed without depending on unstable
+  or undocumented Stateright APIs, stop and record the blocker.
+- If repository quality gates reveal unrelated pre-existing failures, record
+  them separately and continue only once it is clear whether 15.1.2 caused the
+  regression.
+
+## Risks
+
+- Risk: the formal-verification guide still shows illustrative snippets that
+  may drift from the currently available Stateright release. Severity: medium.
+  Likelihood: medium. Mitigation: update the guide to match the version that
+  actually resolves in this repository.
+
+- Risk: the guide's example `wireframe` dependency disables default features,
+  but the current root crate does not compile under that configuration.
+  Severity: medium. Likelihood: high. Mitigation: use the normal `wireframe`
+  feature set for this infrastructure step and record the mismatch as a future
+  follow-up for the main crate rather than forcing unrelated feature work into
+  15.1.2.
+
+- Risk: workspace-manifest tests written for 10.1.1 can become false negatives
+  once the verification crate lands. Severity: high. Likelihood: high.
+  Mitigation: update both the `rstest` and `rstest-bdd` coverage in the same
+  change as the manifest edit.
+
+## Progress
+
+- [x] (2026-04-24 00:00 UTC) Recalled project memory, reviewed the formal
+      verification guide, the existing hybrid-workspace tests, and the root
+      manifest.
+- [x] (2026-04-24 00:10 UTC) Restored this missing 15.1.2 ExecPlan as the
+      living implementation record for the work.
+- [x] (2026-04-24 00:20 UTC) Added `crates/wireframe-verification`,
+      introduced the shared Stateright harness, and added the placeholder
+      connection-model tests.
+- [x] (2026-04-24 00:30 UTC) Updated the root workspace membership and flipped
+      the manifest-contract tests and BDD scenario to the post-15.1.2 state.
+- [x] (2026-04-24 01:25 UTC) Finished documentation updates, ran the required
+      validation, and recorded the final results and baseline blockers.
+
+## Surprises & Discoveries
+
+- Discovery: the draft ExecPlan file discussed in the previous session was not
+  present in the repository, so 15.1.2 implementation had to restore the living
+  document before coding could proceed.
+
+- Discovery: the current crates.io release for Stateright is `0.31.0`, not the
+  `0.30` shown in the formal-verification guide example.
+
+- Discovery: the reduced-feature `wireframe` dependency example does not
+  compile today. The main crate uses `tokio_util::io::StreamReader`, so it
+  still needs the `tokio-util` `io` feature when default features are disabled.
+  The verification crate therefore uses the normal `wireframe` feature set for
+  now.
+
+- Discovery: the first placeholder model accidentally encoded
+  "at most one multi-packet terminator ever" rather than "at most one
+  terminator per multi-packet session". A Stateright counterexample exposed
+  that difference immediately, and the model was corrected by resetting the
+  per-session terminator counter when a new multi-packet session starts.
+
+## Decision Log
+
+- Decision: implement a small semantic placeholder model rather than jumping
+  straight to a detailed `ConnectionActor` translation. Rationale: 15.1.2 owns
+  the crate boundary and shared harness, while later roadmap items own the
+  higher-fidelity model. Date/Author: 2026-04-24 / Codex.
+
+- Decision: use `stateright = "0.31.0"` because that is the current published
+  release that resolves in this repository today. Rationale: repository docs
+  should follow the version contributors can actually install. Date/Author:
+  2026-04-24 / Codex.
+
+- Decision: keep `default-members = ["."]` unchanged while extending
+  `members` to include `crates/wireframe-verification`. Rationale: preserve the
+  day-to-day ergonomics established in 15.1.1 and match the roadmap's staged
+  workspace design. Date/Author: 2026-04-24 / Codex.
+
+- Decision: depend on `wireframe` with its normal default feature set from the
+  verification crate. Rationale: the reduced-feature example in the design doc
+  is not yet compatible with the current main crate, and fixing that would
+  exceed 15.1.2 scope. Date/Author: 2026-04-24 / Codex.
+
+## Outcomes & Retrospective
+
+- Implemented `crates/wireframe-verification` with a shared bounded Stateright
+  harness, a placeholder semantic connection model, and two `rstest`
+  integration tests that prove both the harness and the placeholder model.
+
+- Updated the root workspace to include
+  `crates/wireframe-verification` while keeping `default-members = ["."]`, and
+  flipped the workspace-manifest `rstest` and `rstest-bdd` coverage from the
+  old "verification crate absent" expectation to the new
+  "verification crate present without widened defaults" contract.
+
+- Updated `docs/developers-guide.md`,
+  `docs/formal-verification-methods-in-wireframe.md`, and `docs/roadmap.md`
+  so the repository documentation matches the implemented workspace state and
+  the current Stateright version.
+
+- Validation results:
+  `make fmt` passed.
+  `make check-fmt` passed.
+  `make markdownlint` passed.
+  `make nixie` passed.
+  `cargo test -p wireframe-verification` passed.
+  `cargo clippy -p wireframe-verification --all-targets -- -D warnings`
+  passed.
+  `cargo test --test workspace_manifest` passed.
+  `cargo test --test bdd --features advanced-tests workspace_manifest` passed.
+  `make test` passed.
+  `make test-doc` passed.
+  `make doctest-benchmark` passed.
+
+- Environment-limited or baseline blockers:
+  `make lint` failed in the Whitaker phase on pre-existing `expect` usage
+  findings in the main crate, including `src/fairness.rs`,
+  `src/fragment/payload.rs`, `src/message_assembler/tests.rs`,
+  `src/message_assembler/state_tests.rs`,
+  `src/message_assembler/budget_tests.rs`, and
+  `src/server/runtime/tests.rs`.
+  `cargo test --workspace` reached the newly added verification crate and the
+  root crate successfully, but then failed on pre-existing `wireframe_testing`
+  doctest inference and visibility errors in
+  `wireframe_testing/src/client_pair.rs`,
+  `wireframe_testing/src/helpers/codec_drive.rs`,
+  `wireframe_testing/src/helpers/drive.rs`,
+  `wireframe_testing/src/helpers/payloads.rs`,
+  `wireframe_testing/src/helpers/runtime.rs`, and
+  `wireframe_testing/src/multi_packet.rs`.
diff --git a/docs/formal-verification-methods-in-wireframe.md b/docs/formal-verification-methods-in-wireframe.md
index 4e88441a..29d5551c 100644
--- a/docs/formal-verification-methods-in-wireframe.md
+++ b/docs/formal-verification-methods-in-wireframe.md
@@ -315,39 +315,39 @@ make local execution clumsy.
 
 ### Root `Cargo.toml` changes
 
-Add a workspace section to the root manifest:
+The root manifest should carry the explicit hybrid workspace used today:
 
 ```toml
 [workspace]
-members = ["."]
+members = [".", "crates/wireframe-verification"]
 default-members = ["."]
 resolver = "3"
 ```
 
 Why `default-members = ["."]`?
 
-Because the repo currently behaves like a single-package crate. Keeping only
-the root package as a default member means `cargo test`, `cargo check`, and
-`cargo clippy` at the repo root do not suddenly start running the verification
-crate by accident.[^26]
+Because the repo still behaves like a single-package crate for day-to-day
+development. Keeping only the root package as a default member means
+`cargo test`, `cargo check`, and `cargo clippy` at the repo root do not
+suddenly start running the verification crate by accident.[^26]
 
 That is a small but important stability choice.
 
 One nuance matters here: Cargo metadata for this repository still reports the
-in-repository helper crate `wireframe_testing` in `workspace_members` once the
-root manifest becomes an explicit workspace, even though the staged
-`members = ["."]` list only names the root package. The practical 10.1.1
-contract is therefore:
+in-repository helper crate `wireframe_testing` in `workspace_members`. The
+practical post-15.1.2 contract is therefore:
 
 - the root manifest is explicitly workspace-aware,
+- the dedicated verification crate is an explicit workspace member,
 - the root `wireframe` package remains the sole `default-members` entry, and
-- the dedicated verification crate is still deferred until 10.1.2.
+- `wireframe_testing` may still appear in metadata even though it is not named
+  in the `members` array.
 
-This should land in two stages:
+This still reflects a two-stage rollout:
 
-1. Roadmap item 10.1.1 adds the explicit hybrid workspace with
+1. Roadmap item 15.1.1 adds the explicit hybrid workspace with
    `members = ["."]`.
-2. Roadmap item 10.1.2 extends the member list to
+2. Roadmap item 15.1.2 extends the member list to
    `[".", "crates/wireframe-verification"]` when the verification crate exists.
 
 That staging keeps the Cargo layout change separate from the introduction of
@@ -560,8 +560,8 @@ edition = "2024"
 publish = false
 
 [dependencies]
-stateright = "0.30"
-wireframe = { path = "../..", default-features = false, features = ["test-support"] }
+stateright = "0.31.0"
+wireframe = { path = "../..", features = ["test-support"] }
 
 [dev-dependencies]
 rstest = "0.26"
@@ -572,6 +572,10 @@ repo already calls for it. mxd uses `nextest`, but Wireframe’s current Makefil
 uses `cargo test`.[^12][^15] The important part is the **separate crate and
 shared harness**, not the exact test runner.
 
+The reduced-feature dependency shown in earlier drafts turned out not to match
+the current main crate, so the repository now uses the normal `wireframe`
+feature set for this infrastructure step.
+
 ### Model scope
 
 Model the `ConnectionActor` semantically, not mechanically.
diff --git a/docs/roadmap.md b/docs/roadmap.md
index 7da8c207..e21afcd2 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -585,7 +585,7 @@ Wireframe's protocol, framing, and message assembly layers.
   [formal-verification-methods-in-wireframe.md §Root `Cargo.toml` changes](formal-verification-methods-in-wireframe.md#root-cargotoml-changes).
    Success criteria: `cargo build` and `cargo test --workspace` pass with the
   new layout.
-- [ ] 15.1.2. Add `crates/wireframe-verification` as an internal crate for
+- [x] 15.1.2. Add `crates/wireframe-verification` as an internal crate for
   Stateright models and shared verification harnesses. Requires 15.1.1. See
   [formal-verification-methods-in-wireframe.md §Why Stateright belongs in a separate verification crate](formal-verification-methods-in-wireframe.md#why-stateright-belongs-in-a-separate-verification-crate)
    and
diff --git a/tests/common/workspace_manifest_support.rs b/tests/common/workspace_manifest_support.rs
index 72089032..0109fcbb 100644
--- a/tests/common/workspace_manifest_support.rs
+++ b/tests/common/workspace_manifest_support.rs
@@ -50,8 +50,14 @@ pub(crate) fn cargo_metadata() -> WorkspaceManifestResult<String> {
     run_cargo(&["metadata", "--no-deps", "--format-version", "1"])
 }
 
-pub(crate) fn root_package_id() -> WorkspaceManifestResult<String> {
-    run_cargo(&["pkgid", "--", "wireframe"]).map(|stdout| stdout.trim().to_owned())
+pub(crate) fn cargo_package_id(package_name: &str) -> WorkspaceManifestResult<String> {
+    run_cargo(&["pkgid", "--", package_name]).map(|stdout| stdout.trim().to_owned())
+}
+
+pub(crate) fn root_package_id() -> WorkspaceManifestResult<String> { cargo_package_id("wireframe") }
+
+pub(crate) fn verification_package_id() -> WorkspaceManifestResult<String> {
+    cargo_package_id("wireframe-verification")
 }
 
 pub(crate) fn has_manifest_line(manifest: &str, expected: &str) -> bool {
diff --git a/tests/features/workspace_manifest.feature b/tests/features/workspace_manifest.feature
index c2ac94c7..2c9bf8b1 100644
--- a/tests/features/workspace_manifest.feature
+++ b/tests/features/workspace_manifest.feature
@@ -1,10 +1,11 @@
-Feature: Hybrid workspace manifest
+Feature: Formal verification workspace manifest
   The repository should expose an explicit hybrid Cargo workspace while keeping
-  the root package as the only default member during roadmap item 10.1.1.
+  the root package as the only default member after adding the verification
+  crate in roadmap item 15.1.2.
 
-  Scenario: The root manifest stages the hybrid workspace conversion
+  Scenario: The root manifest adds the verification crate without widening defaults
     Given the repository workspace metadata is loaded
     Then the root Cargo manifest declares the staged hybrid workspace
     And the workspace metadata reports the root package as a workspace member
     And the workspace metadata reports the root package as the only default member
-    And the workspace metadata does not include the verification crate yet
+    And the workspace metadata includes the verification crate as a workspace member
diff --git a/tests/fixtures/workspace_manifest.rs b/tests/fixtures/workspace_manifest.rs
index c2f666dd..cf808bc1 100644
--- a/tests/fixtures/workspace_manifest.rs
+++ b/tests/fixtures/workspace_manifest.rs
@@ -9,6 +9,7 @@ use crate::workspace_manifest_support::{
     has_manifest_line,
     root_manifest,
     root_package_id,
+    verification_package_id,
 };
 
 pub type TestResult = FixtureResult<()>;
@@ -22,6 +23,7 @@ pub struct WorkspaceManifestWorld {
     manifest: Option<String>,
     metadata: Option<String>,
     package_id: Option<String>,
+    verification_package_id: Option<String>,
 }
 
 #[rustfmt::skip]
@@ -42,6 +44,7 @@ impl WorkspaceManifestWorld {
         self.manifest = Some(root_manifest()?);
         self.metadata = Some(cargo_metadata()?);
         self.package_id = Some(root_package_id()?);
+        self.verification_package_id = Some(verification_package_id()?);
         Ok(())
     }
 
@@ -63,6 +66,12 @@ impl WorkspaceManifestWorld {
             .ok_or_else(|| "workspace package id not loaded".to_owned())
     }
 
+    fn verification_package_id(&self) -> Result<&str, String> {
+        self.verification_package_id
+            .as_deref()
+            .ok_or_else(|| "verification package id not loaded".to_owned())
+    }
+
     fn metadata_json(&self) -> FixtureResult<Value> { Ok(serde_json::from_str(self.metadata()?)?) }
 
     fn metadata_array<'a>(metadata: &'a Value, field: &str) -> Result<&'a [Value], String> {
@@ -93,7 +102,7 @@ impl WorkspaceManifestWorld {
         let manifest = self.manifest()?;
         for expected in [
             "[workspace]",
-            "members = [\".\"]",
+            "members = [\".\", \"crates/wireframe-verification\"]",
             "default-members = [\".\"]",
             "resolver = \"3\"",
         ] {
@@ -155,19 +164,29 @@ impl WorkspaceManifestWorld {
         Ok(())
     }
 
-    /// Verify the staged rollout has not yet added the verification crate.
+    /// Verify the verification crate is now part of the workspace membership.
     ///
     /// # Errors
     ///
-    /// Returns an error when the 10.1.2 crate appears too early or the helper
-    /// crate unexpectedly disappears from Cargo metadata.
-    pub fn verify_verification_crate_is_absent(&self) -> TestResult {
+    /// Returns an error when the verification crate is missing from
+    /// `workspace_members` or the helper crate unexpectedly disappears from
+    /// Cargo metadata.
+    pub fn verify_verification_crate_is_workspace_member(&self) -> TestResult {
         let metadata = self.metadata_json()?;
-        if Self::packages_include_name(&metadata, VERIFICATION_PACKAGE_NAME)? {
+        let verification_package_id = self.verification_package_id()?;
+        let workspace_members = Self::metadata_array(&metadata, "workspace_members")?;
+        if !workspace_members
+            .iter()
+            .any(|member| member.as_str() == Some(verification_package_id))
+        {
             return Err(
-                "verification crate should not join the workspace until roadmap item 10.1.2".into(),
+                "workspace metadata should include the verification crate in workspace_members"
+                    .into(),
             );
         }
+        if !Self::packages_include_name(&metadata, VERIFICATION_PACKAGE_NAME)? {
+            return Err("cargo metadata packages should include the verification crate".into());
+        }
         if !Self::packages_include_name(&metadata, HELPER_PACKAGE_NAME)? {
             return Err(
                 "workspace metadata should continue to report the in-repository helper crate"
diff --git a/tests/scenarios/workspace_manifest_scenarios.rs b/tests/scenarios/workspace_manifest_scenarios.rs
index 25ed1d44..dda6692b 100644
--- a/tests/scenarios/workspace_manifest_scenarios.rs
+++ b/tests/scenarios/workspace_manifest_scenarios.rs
@@ -8,23 +8,23 @@ use crate::fixtures::workspace_manifest::{
     workspace_manifest_world,
 };
 
-fn assert_root_manifest_stages_hybrid_workspace(
+fn assert_root_manifest_adds_verification_crate(
     workspace_manifest_world: &mut WorkspaceManifestWorld,
 ) -> TestResult {
     workspace_manifest_world.load()?;
     workspace_manifest_world.verify_staged_hybrid_workspace_manifest()?;
     workspace_manifest_world.verify_root_is_workspace_member()?;
     workspace_manifest_world.verify_root_is_only_default_member()?;
-    workspace_manifest_world.verify_verification_crate_is_absent()?;
+    workspace_manifest_world.verify_verification_crate_is_workspace_member()?;
     Ok(())
 }
 
 #[scenario(
     path = "tests/features/workspace_manifest.feature",
-    name = "The root manifest stages the hybrid workspace conversion"
+    name = "The root manifest adds the verification crate without widening defaults"
 )]
-fn root_manifest_stages_hybrid_workspace(workspace_manifest_world: WorkspaceManifestWorld) {
+fn root_manifest_adds_verification_crate(workspace_manifest_world: WorkspaceManifestWorld) {
     let mut workspace_manifest_world = workspace_manifest_world;
-    assert_root_manifest_stages_hybrid_workspace(&mut workspace_manifest_world)
+    assert_root_manifest_adds_verification_crate(&mut workspace_manifest_world)
         .expect("workspace manifest scenario should pass");
 }
diff --git a/tests/steps/workspace_manifest_steps.rs b/tests/steps/workspace_manifest_steps.rs
index e4a35bc8..e3f4186b 100644
--- a/tests/steps/workspace_manifest_steps.rs
+++ b/tests/steps/workspace_manifest_steps.rs
@@ -32,9 +32,9 @@ fn then_workspace_metadata_reports_only_default_member(
     workspace_manifest_world.verify_root_is_only_default_member()
 }
 
-#[then("the workspace metadata does not include the verification crate yet")]
-fn then_workspace_metadata_excludes_verification_crate(
+#[then("the workspace metadata includes the verification crate as a workspace member")]
+fn then_workspace_metadata_includes_verification_crate(
     workspace_manifest_world: &mut WorkspaceManifestWorld,
 ) -> TestResult {
-    workspace_manifest_world.verify_verification_crate_is_absent()
+    workspace_manifest_world.verify_verification_crate_is_workspace_member()
 }
diff --git a/tests/workspace_manifest.rs b/tests/workspace_manifest.rs
index b2c04d05..66f40699 100644
--- a/tests/workspace_manifest.rs
+++ b/tests/workspace_manifest.rs
@@ -1,8 +1,8 @@
-//! Regression tests for the staged hybrid-workspace manifest contract.
+//! Regression tests for the formal-verification workspace manifest contract.
 //!
 //! These checks verify that the repository advertises an explicit hybrid
-//! workspace while keeping the root package as the only default member during
-//! roadmap item 10.1.1.
+//! workspace, includes the internal verification crate as a workspace member,
+//! and still keeps the root package as the only default member.
 
 #[path = "common/workspace_manifest_support.rs"]
 mod workspace_manifest_support;
@@ -16,6 +16,7 @@ use workspace_manifest_support::{
     repo_root,
     root_manifest,
     root_package_id,
+    verification_package_id,
 };
 
 fn parse_metadata_json(metadata: &str) -> TestResult<Value> { Ok(serde_json::from_str(metadata)?) }
@@ -37,12 +38,15 @@ fn root_manifest_declares_explicit_workspace_section() -> TestResult {
         "root Cargo.toml should declare an explicit [workspace] section"
     );
     assert!(
-        has_manifest_line(&manifest, "members = [\".\"]"),
-        "10.1.1 should stage the workspace with only the root package as a member"
+        has_manifest_line(
+            &manifest,
+            "members = [\".\", \"crates/wireframe-verification\"]"
+        ),
+        "15.1.2 should add the verification crate to the explicit workspace members"
     );
     assert!(
         has_manifest_line(&manifest, "default-members = [\".\"]"),
-        "10.1.1 should keep the root package as the only default workspace member"
+        "15.1.2 should keep the root package as the only default workspace member"
     );
     assert!(
         has_manifest_line(&manifest, "resolver = \"3\""),
@@ -56,10 +60,11 @@ fn root_manifest_declares_explicit_workspace_section() -> TestResult {
     clippy::panic_in_result_fn,
     reason = "assertions provide clearer diagnostics in integration tests"
 )]
-fn cargo_metadata_reports_root_as_only_workspace_member_and_default_member() -> TestResult {
+fn cargo_metadata_reports_verification_crate_without_widening_default_members() -> TestResult {
     let repo_root = repo_root()?;
     let repo_root_str = repo_root.as_str();
-    let package_id = root_package_id()?;
+    let root_package_id = root_package_id()?;
+    let verification_package_id = verification_package_id()?;
     let manifest_path = repo_root.join("Cargo.toml");
     let manifest_path_str = manifest_path.as_str();
     let metadata = cargo_metadata()?;
@@ -74,9 +79,29 @@ fn cargo_metadata_reports_root_as_only_workspace_member_and_default_member() ->
         "metadata should continue to resolve the root package manifest"
     );
     assert!(
-        metadata.contains(&package_id),
+        metadata.contains(&root_package_id),
         "workspace metadata should include the root package"
     );
+    let workspace_members = metadata_json
+        .get("workspace_members")
+        .and_then(Value::as_array)
+        .expect("cargo metadata should expose workspace_members as an array");
+    assert!(
+        workspace_members
+            .iter()
+            .any(|member| member.as_str() == Some(root_package_id.as_str())),
+        "workspace_members should include the root package id"
+    );
+    assert!(
+        workspace_members
+            .iter()
+            .any(|member| member.as_str() == Some(verification_package_id.as_str())),
+        "workspace_members should include the verification crate id"
+    );
+    assert!(
+        metadata.contains("wireframe-verification"),
+        "15.1.2 should add the verification crate to cargo metadata"
+    );
     let workspace_default_members = metadata_json
         .get("workspace_default_members")
         .and_then(Value::as_array)
@@ -84,16 +109,12 @@ fn cargo_metadata_reports_root_as_only_workspace_member_and_default_member() ->
     assert_eq!(
         workspace_default_members.len(),
         1,
-        "10.1.1 should keep exactly one default workspace member"
+        "15.1.2 should keep exactly one default workspace member"
     );
     assert_eq!(
         workspace_default_members.first().and_then(Value::as_str),
-        Some(package_id.as_str()),
-        "10.1.1 should keep the root package as the only default workspace member"
-    );
-    assert!(
-        !metadata.contains("wireframe-verification"),
-        "10.1.1 should not add the verification crate before roadmap item 10.1.2"
+        Some(root_package_id.as_str()),
+        "15.1.2 should keep the root package as the only default workspace member"
     );
     Ok(())
 }