verify lifecycle implementation with Kani and Shuttle (#98)

Author: pranc1ngpegasus

.github/workflows/formal.yaml

@@ -14,5 +14,13 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - name: Verify lifecycle implementation with Kani
+        uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 # v1
+        with:
+          kani-version: "0.67.0"
+          command: cargo-kani
+          args: "-p wisp-lifecycle"
       - uses: ./.github/actions/setup-nix
-      - run: nix build .#checks.x86_64-linux.formal --print-build-logs
+      - uses: ./.github/actions/setup-rust-cache
+      - name: Explore lifecycle interleavings with Shuttle
+        run: nix develop .#ci --quiet --command cargo test -p wisp-lifecycle --test shuttle_lifecycle

Cargo.lock

@@ -5,6 +5,7 @@ members = [
   "crates/wisp-audiokit",
   "crates/wisp-audiokit-sys",
   "crates/wisp-core",
+  "crates/wisp-lifecycle",
   "crates/wisp-storage",
 ]
 resolver = "3"
@@ -23,6 +24,10 @@ tempfile = "3.27.0"
 thiserror = "2.0.18"
 uuid = { version = "1.23.1", features = ["v4"] }
 
+[workspace.lints.rust.unexpected_cfgs]
+level = "warn"
+check-cfg = ["cfg(kani)"]
+
 [workspace.lints.clippy]
 # The toolchain is pinned (see rust-toolchain.toml), so the exact set of
 # lints is deterministic. That lets us treat the well-behaved groups as a

Cargo.toml

@@ -74,15 +74,15 @@ cargo build -p wisp-desktop --release
 
 ### Formal verification
 
-The session worker protocol and the whole-app navigation/session workflow have
-executable TLA+ models plus symbolic one-step invariant proofs in Z3:
+The session worker protocol and navigation/session guards are checked against
+the production Rust implementation with Kani and Shuttle:
 
 ```bash
-nix develop .#formal --command bash formal/check.sh
+bash formal/check.sh
 ```
 
-See [`formal/README.md`](formal/README.md) for the verified properties,
-implementation mapping, assumptions, and extension workflow.
+See [`formal/README.md`](formal/README.md) for setup, verified properties, and
+the extension workflow.
 
 See `.github/workflows/release.yaml` for how the release `.app` bundle is produced — pushing a `v*` tag builds `Wisp.app` on a macOS 26 runner.
 
@@ -116,7 +116,7 @@ MCP hosts should run the bundled `wisp-mcp` binary over stdio, for example `/App
 
 ## Contributing
 
-Issues and pull requests are welcome. Before sending a PR, please make sure `cargo fmt`, `cargo clippy --workspace --all-targets`, `cargo test --workspace`, and `nix develop .#formal --command bash formal/check.sh` pass under the same conditions as CI. For the Swift side, `make -C native/WispAudioKit` runs the equivalent checks.
+Issues and pull requests are welcome. Before sending a PR, please make sure `cargo fmt`, `cargo clippy --workspace --all-targets`, `cargo test --workspace`, and `bash formal/check.sh` pass under the same conditions as CI. For the Swift side, `make -C native/WispAudioKit` runs the equivalent checks.
 
 ## License
 

README.md

@@ -25,6 +25,7 @@ unsafe_code = "deny"
 
 [dependencies]
 wisp-core = { path = "../../crates/wisp-core" }
+wisp-lifecycle = { path = "../../crates/wisp-lifecycle" }
 wisp-storage = { path = "../../crates/wisp-storage" }
 wisp-audiokit = { path = "../../crates/wisp-audiokit" }
 

apps/wisp-desktop/Cargo.toml

@@ -18,6 +18,7 @@ use wisp_audiokit::{
     SessionError, SessionResult, SourceLabel, local_model_spec, local_model_status,
 };
 use wisp_core::{Session as StoredSession, SessionId};
+use wisp_lifecycle::{Phase, UpdateContext, ViewOwner, WorkerUpdate, can_replace_transcript};
 
 #[derive(Debug, Clone)]
 pub enum AppError {
@@ -55,15 +56,51 @@ pub enum SessionState {
 }
 
 impl SessionState {
+    #[must_use]
+    pub const fn phase(self) -> Phase {
+        match self {
+            Self::Idle => Phase::Idle,
+            Self::Starting => Phase::Starting,
+            Self::Recording { .. } => Phase::Recording,
+            Self::Stopping => Phase::Stopping,
+            Self::Failed => Phase::Failed,
+        }
+    }
+
     /// Whether an audio session is running or changing lifecycle state.
     /// While this is true the live transcript is the persistence source and
     /// must not be replaced by another view's segments.
     #[must_use]
     pub const fn is_active(self) -> bool {
-        matches!(
-            self,
-            Self::Starting | Self::Recording { .. } | Self::Stopping
-        )
+        self.phase().is_active()
+    }
+
+    #[must_use]
+    pub fn with_phase(
+        self,
+        phase: Phase,
+        recording_started_at: Instant,
+    ) -> Self {
+        match phase {
+            Phase::Idle => Self::Idle,
+            Phase::Starting => Self::Starting,
+            Phase::Recording => Self::Recording {
+                started_at: recording_started_at,
+            },
+            Phase::Stopping => Self::Stopping,
+            Phase::Failed => Self::Failed,
+        }
+    }
+
+    #[must_use]
+    pub const fn request_stop(self) -> Self {
+        match self.phase().request_stop() {
+            Phase::Stopping => Self::Stopping,
+            Phase::Idle => Self::Idle,
+            Phase::Starting => Self::Starting,
+            Phase::Recording => self,
+            Phase::Failed => Self::Failed,
+        }
     }
 }
 
@@ -292,6 +329,41 @@ pub struct AppModel {
 }
 
 impl AppModel {
+    fn view_owner(&self) -> ViewOwner {
+        match self.view {
+            View::Library => ViewOwner::Library,
+            View::LiveSession => ViewOwner::Live,
+            View::History { .. } => ViewOwner::History,
+        }
+    }
+
+    #[must_use]
+    pub fn accepts_worker_update(
+        &self,
+        session_id: SessionId,
+    ) -> bool {
+        UpdateContext {
+            phase: self.state.phase(),
+            view: self.view_owner(),
+            current_session_id: self.current_session_id.map(SessionId::as_i64),
+        }
+        .accepts(session_id.as_i64())
+    }
+
+    #[must_use]
+    pub fn worker_update_phase(
+        &self,
+        session_id: SessionId,
+        update: WorkerUpdate,
+    ) -> Option<Phase> {
+        UpdateContext {
+            phase: self.state.phase(),
+            view: self.view_owner(),
+            current_session_id: self.current_session_id.map(SessionId::as_i64),
+        }
+        .next_phase(session_id.as_i64(), update)
+    }
+
     pub fn new() -> Self {
         Self {
             state: SessionState::Idle,
@@ -332,9 +404,11 @@ impl AppModel {
     /// A retained database handle after a failed finalization is deliberately
     /// treated as unsettled so navigation cannot silently discard it.
     pub fn has_unsettled_session(&self) -> bool {
-        self.state.is_active()
-            || self.pending_session_write.is_some()
-            || self.current_output_dir.is_some()
+        !can_replace_transcript(
+            self.state.phase(),
+            self.pending_session_write.is_some(),
+            self.current_output_dir.is_some(),
+        )
     }
 
     /// A stopped worker whose transcript transaction needs to be retried.