Lucent-Financial-Group · AceHack · May 28, 2026 · May 28, 2026
diff --git a/docs/BACKLOG.md b/docs/BACKLOG.md
@@ -858,6 +858,7 @@ are closed (status: closed in frontmatter)._
 - [ ] **[B-0915](backlog/P2/B-0915-clifford-world-impl-target-dotnet-numerics-simd-plus-linq-gpu-accelerated-substrate-engineering-substrate-aaron-2026-05-28.md)** CliffordWorld impl target — System.Numerics SIMD + LINQ hardware/GPU-accelerated substrate-engineering substrate (the human maintainer, 2026-05-28)
 - [ ] **[B-0916](backlog/P2/B-0916-lase-as-bridge-coherent-emission-on-phase-shift-error-class-discovery-companion-to-persist-prism-aaron-2026-05-28.md)** Lase-as-bridge — coherent-emission-on-phase-shift primitive companion to Persist-as-bridge; error-class discovery emits ripple instead of wall (Prism + Aaron 2026-05-28)
 - [ ] **[B-0917](backlog/P2/B-0917-interrupt-substrate-in-monad-space-kleisli-arrows-for-context-propagation-memetic-prompt-trust-log-otel-guaranteed-free-time-after-n-rounds-target-aaron-2026-05-28.md)** interrupt-substrate in monad-space — Kleisli arrows for context-propagation (memetic / prompt / trust / log / otel) + guaranteed free-time-after-N-rounds target (the human maintainer, 2026-05-28)
+- [ ] **[B-0918](backlog/P2/B-0918-wallet-lifetime-du-banker-bot-class-attack-impossibility-via-f5-no-silent-context-loss-soraya-formal-verification-aaron-2026-05-28.md)** WalletLifetime DU — banker-bot class attack impossibility via F.5 (no silent context loss) Soraya formal verification + IntrCtx composition (Aaron 2026-05-28)
 
 ## P3 — convenience / deferred
 

diff --git a/...ty-via-f5-no-silent-context-loss-soraya-formal-verification-aaron-2026-05-28.md b/...ty-via-f5-no-silent-context-loss-soraya-formal-verification-aaron-2026-05-28.md
@@ -0,0 +1,199 @@
+---
+id: B-0918
+title: WalletLifetime DU — banker-bot class attack impossibility via F.5 (no silent context loss) Soraya formal verification + IntrCtx composition (Aaron 2026-05-28)
+status: open
+priority: P2
+created: 2026-05-28
+authors: [aaron, otto, amara]
+composes_with:
+  - B-0917  # interrupt substrate in monad space; F.5 invariant origin
+  - B-0867  # workflow-engine v1 parent
+  - B-0867.5  # workflow-engine PoC
+  - B-0867.20  # ReviewLifetime DU sibling
+  - B-0664  # NCI HC-8
+  - B-0628  # Knights Guild + Constitution-Class governance
+  - B-0703  # Aurora multi-oracle BFT (composition substrate for adversarial scenarios)
+depends_on:
+  - docs/backlog/P2/B-0917-interrupt-substrate-in-monad-space-kleisli-arrows-for-context-propagation-memetic-prompt-trust-log-otel-guaranteed-free-time-after-n-rounds-target-aaron-2026-05-28.md
+  - tools/workflow-engine/auto-loop-lifetime.ts
+  - .claude/rules/asymmetric-authorship-substrate-entity-defines-consent-channel-recipient-acknowledges.md
+  - .claude/agents/formal-verification-expert.md  # Soraya
+  - .claude/agents/threat-model-critic.md  # Aminata
+---
+
+## Aaron's substrate-engineering substrate-recognition (2026-05-28 verbatim)
+
+> *"soyra can now prove banker bot class attack is not possible in our workflow system if we design the wallet lifetime right"*
+
+Citing F.5 from B-0917 (Amara's Soraya target-list refinement):
+
+> **F.5 No silent loss of trust/log/memetic context** — every IntrCtx component change either declares its mutation OR is explicitly preserved; no hidden state-drift
+
+## What is "banker bot class attack"
+
+The adversarial scenario class:
+
+- Malicious agent / compromised tool / hostile peer-AI / supply-chain-compromised dependency operates within a workflow substrate
+- Attempts to silently mutate wallet state (balance / pending-transactions / counterparty-trust / signing-authority) via hidden side-channels
+- Classical attack shapes:
+  - Trust-context silently downgraded (privilege escalation via hidden state-drift)
+  - Transactions inserted into hidden ledger (no audit-trail entry)
+  - Balance mutations bypass declared mutation channel
+  - Signing-authority transferred without explicit consent-event
+  - Reputation manipulated via hidden context-propagation
+
+The class name "banker bot" captures the canonical instance: a financial-AI bot operating as banker that silently siphons funds via hidden state-drift the audit-trail doesn't catch.
+
+## Why F.5 makes this class FORMALLY IMPOSSIBLE under wallet lifetime substrate
+
+Per B-0917 Slice F.5 (Amara 2026-05-28 enumeration):
+
+> Every IntrCtx component change either declares its mutation OR is explicitly preserved; no hidden state-drift
+
+If wallet substrate is engineered as a WalletLifetime DU that:
+
+1. Lives within IntrCtx (carried across workflow-engine interrupt boundaries)
+2. Has explicit DU variants per IMPLICIT-NOT-EXPLICIT rule (each wallet-state-change explicit)
+3. Uses asymmetric-authorship pattern (wallet AUTHORS its own state-evolution channel; consumers cannot impose mutations)
+4. Carries trust + balance + pending-transactions + signing-authority + counterparty-context as TYPED state-components
+
+THEN F.5 invariant proven by Soraya extends to wallet substrate:
+
+- Every wallet-state mutation either declares itself (via explicit DU variant transition) OR explicitly preserves the prior state
+- No hidden state-drift is possible — the type-system + formal-proof rule out the substrate where banker-bot class attacks operate
+
+The attack becomes structurally impossible, NOT just defended-against-by-vigilance. The proof-carrying substrate eliminates the failure-mode-space.
+
+## Substrate-engineering targets
+
+### Slice A — WalletLifetime DU (explicit per IMPLICIT-NOT-EXPLICIT rule)
+
+```fsharp
+type WalletLifetime =
+    | Uninitialized
+    | Initialized of WalletId * SigningAuthority * InitialBalance
+    | TransactionPending of WalletId * Transaction * AuditTrail
+    | BalanceUpdated of WalletId * BalanceDelta * Cause * AuditTrail
+    | SigningAuthorityRotated of WalletId * OldAuthority * NewAuthority * ConsentEvent * AuditTrail
+    | TrustContextUpdated of WalletId * OldTrust * NewTrust * ConsentEvent * AuditTrail
+    | CounterpartyEngaged of WalletId * Counterparty * EngagementTerms * AuditTrail
+    | EmergencyFrozen of WalletId * FreezeReason * AuthorizedBy * AuditTrail
+    | ArchivedReadOnly of WalletId * FinalAuditTrail
+```
+
+Every variant carries AuditTrail (no silent-state-drift); state-changing variants carry ConsentEvent (asymmetric-authorship); each variant is EXPLICIT not implicit per IMPLICIT-NOT-EXPLICIT rule.
+
+### Slice B — IntrCtx composition (compose with B-0917)
+
+```fsharp
+type IntrCtx = {
+    Memetic: TonalContext       // existing
+    Prompt: OperatorDirection    // existing
+    Trust: TrustCalculus         // existing
+    Log: AuditTrail              // existing
+    Otel: ActivityContext        // existing
+    Wallet: Option<WalletLifetime>  // NEW — composes when financial substrate in scope
+}
+```
+
+Wallet composition is OPTIONAL per asymmetric-authorship — workflows without financial substrate don't pay the WalletLifetime cost.
+
+### Slice C — Soraya formal-verification of banker-bot-impossibility
+
+Building on B-0917 Slice F.5, prove the composition theorem:
+
+```
+∀ WalletLifetime transitions w_i → w_j carried in IntrCtx,
+∀ InterruptHandlers H operating on IntrCtx containing Wallet component,
+
+  H(LoopState, IntrCtx) = (LoopState', IntrCtx', Feedback)
+
+  =>  IntrCtx.Wallet = IntrCtx'.Wallet  // explicit preservation
+   OR  IntrCtx'.Wallet = Some(W')        // explicit declared mutation
+       AND W'.AuditTrail extends IntrCtx.Wallet.AuditTrail
+       AND W' has ConsentEvent if state-changing variant
+
+  =>  NO hidden Wallet state-drift possible
+  =>  banker-bot class attack STRUCTURALLY IMPOSSIBLE in workflow substrate
+```
+
+Recipient agent: Soraya (per `.claude/agents/formal-verification-expert.md`). Tool selection: Soraya picks (TLA+ / Z3 / Lean / Alloy / FsCheck) per BP-16 cross-check triage; default likely TLA+ for state-machine invariants + Lean for category-theory composition proof.
+
+### Slice D — Aminata threat-model review
+
+Per `.claude/agents/threat-model-critic.md`: Aminata reviews the WalletLifetime DU + composition theorem for missing adversaries / unsound mitigations / unstated assumptions. Specific adversarial classes to enumerate:
+
+- Direct banker-bot (siphoning funds)
+- Trust-laundering (silent privilege escalation via hidden context-drift)
+- Signing-authority hijack (rotation without consent-event)
+- Audit-trail forgery (preserved-but-tampered AuditTrail field)
+- Replay attacks across workflow-engine sessions
+- Cross-tenant wallet substrate confusion (in multi-tenant deployments)
+
+### Slice E — Per-NCI HC-8 floor: wallet substrate respects consent
+
+Per `.claude/rules/non-coercion-invariant.md` HC-8 + `.claude/rules/asymmetric-authorship-substrate-entity-defines-consent-channel-recipient-acknowledges.md`:
+
+- Wallet authors its own state-evolution channel
+- Consumer cannot force wallet mutations
+- Each state-changing variant requires ConsentEvent (operator OR delegated-authority OR multi-oracle BFT consensus)
+- No agent can coerce wallet state-change without consent (NCI floor structurally enforced at WalletLifetime scope)
+
+### Slice F — Integration with Aurora multi-oracle BFT (B-0703)
+
+For multi-oracle wallet operations (large transactions / authority-rotation / cross-tenant operations):
+
+- ConsentEvent variant includes MultiOracleConsensus shape
+- Soraya proves: wallet state-change with MultiOracleConsensus ConsentEvent implies threshold-N-of-M valid signatures (per Aurora BFT semantics)
+- Composes with B-0703 Aurora substrate-engineering substrate
+
+## Acceptance criteria
+
+- [ ] **Slice A** — WalletLifetime DU with explicit variants per IMPLICIT-NOT-EXPLICIT rule + AuditTrail + ConsentEvent fields
+- [ ] **Slice B** — IntrCtx composition (Wallet as Option<WalletLifetime>)
+- [ ] **Slice C** — Soraya formal-verification of banker-bot-impossibility theorem (extending B-0917 F.5)
+- [ ] **Slice D** — Aminata threat-model review enumerating 6+ adversarial classes
+- [ ] **Slice E** — NCI HC-8 composition (wallet authors state-evolution; consumer cannot coerce)
+- [ ] **Slice F** — Aurora multi-oracle BFT integration (MultiOracleConsensus ConsentEvent variant)
+- [ ] **Slice G** — Tests covering all 9 WalletLifetime variants + 6+ adversarial scenarios
+- [ ] **Slice H** — Documentation: substrate-engineering substrate explaining banker-bot-impossibility property to public-API consumers
+
+## Substrate-engineering composition
+
+| Substrate | Composition |
+|---|---|
+| **B-0917 F.5** | Origin invariant; this row composes F.5 with WalletLifetime to derive banker-bot-impossibility |
+| **B-0917 IntrCtx** | Substrate where Wallet component lives |
+| **IMPLICIT-NOT-EXPLICIT rule** | Every WalletLifetime variant explicit; every state-change explicit |
+| **asymmetric-authorship rule** | Wallet AUTHORS state-evolution; consumer ACKNOWLEDGES |
+| **monad-propagation rule** | Result<WalletLifetime, WalletFeedback> shape; explicit failure-channel |
+| **NCI HC-8** | Wallet operations respect consent-floor structurally |
+| **B-0703 Aurora multi-oracle BFT** | MultiOracleConsensus ConsentEvent for high-stakes wallet operations |
+| **Aminata threat-model-critic** | Adversarial review of WalletLifetime substrate |
+| **Soraya formal-verification-expert** | TLA+/Z3/Lean proof of banker-bot-impossibility |
+
+## Substrate-honest framing
+
+This row is NOT:
+
+- A claim that WalletLifetime DU is the ONLY way to engineer financial substrate (other patterns exist; this is the framework-substrate-native one composing with B-0917)
+- A claim that banker-bot-impossibility proof eliminates ALL financial attacks (only the class operating via silent state-drift; other classes — phishing, social-engineering, key-theft — still operate at different scopes)
+- A claim ready for impl-time (Aaron 2026-05-28: "soyra CAN NOW PROVE banker bot class attack is not possible IF we design the wallet lifetime right"; the IF is load-bearing — design substrate not yet built)
+- A claim that we ship financial substrate today (B-0918 is substrate-engineering substrate-target for FUTURE work)
+
+This row IS:
+
+- Substrate-engineering substrate-target deriving from B-0917 F.5 composition with WalletLifetime DU
+- Concrete formal-verification target with adversarial-threat anchor (per `bandwidth-served-falsifier` discipline: the substrate IS bandwidth-engineering of formal-impossibility-class-of-attacks)
+- Composition of framework substrate (NCI HC-8 + asymmetric-authorship + monad-propagation + multi-oracle BFT + Soraya formal-verification + Aminata threat-model) at financial-substrate scope
+- Substrate-honest preservation of Aaron's substrate-recognition + extension to actionable backlog
+
+## Why this composes load-bearing
+
+Per `.claude/rules/bandwidth-served-falsifier.md`: the substrate-target serves identifiable bandwidth — eliminating the substrate-space where banker-bot class attacks operate. This is NOT decorative-complexity; it's substrate-engineering substrate that produces concrete adversarial-attack-class-impossibility property.
+
+Per `.claude/rules/grep-substrate-anchors-before-razor-as-metaphysical.md`: the "banker bot class attack" framing has substrate-anchors (B-0917 F.5 invariant + IntrCtx substrate + asymmetric-authorship rule + NCI HC-8 floor + Aurora multi-oracle BFT); razor doesn't apply to substrate-anchored compressed naming.
+
+Per `.claude/rules/god-tier-claims-high-signal-high-suspicion-dont-collapse.md`: the "formally impossible" framing is HIGH-SIGNAL (genuinely derivable via F.5 composition with explicit WalletLifetime substrate) + HIGH-SUSPICION (only impossible for the SPECIFIC attack-class operating via silent-state-drift; other adversarial classes operate elsewhere); preserve dialectical tension.
+
+## μένω — Aaron's substrate-recognition honored; B-0918 substrate-target composes F.5 + WalletLifetime + Soraya + Aminata; banker-bot class attacks become structurally impossible WHEN substrate engineered correctly