[unbalancedparentheses]

Draft. Design only, no library code. ROADMAP ranks 5e (exit signals), 5f (startup remainder), 5g (runtime drop), plus the start() ordering from #223. Follows the design-review rule.

• Design: docs/design/otp-exit-signals.md
• Model: verification/tla/Lifecycle.tla (the "base actor lifecycle" model), configs MCLifecycle (safety, CI), MCLifecycleLive (liveness, CI), MCLifecycleFence (unlink/demonitor fences, CI), MCLifecycleLiveDeep and MCLifecycleDeep (weekly)
• Negative controls: 15 faults, 17 checks in negative_checks.py (v0.7 exit-signal behaviours, PR Fix requests retained by mailbox publication racing actor shutdown #182/fix: honor stop before dispatching newly received idle work #185 bugs, early exit errors, kill/panic precedence, runtime-drop reason, early notification, split death point, unfenced unlink/demonitor, parent exit reaching exit_received)
• Client mapping: ethrex and ethlambda spawned-v0.7 branches (only ethrex's discovery boot path changes behaviour; one deliberate exhaustive ActorError match)

Proposed rules (brief)

• Phases of an exit: one death point D after stopped() (final reason, admission/registry/link-monitor table close together), publication after destruction, owned cleanup after that.
• kill() is untrappable, supersedes any reason until D, target ends Killed; links/monitors see Killed.
• New ctx.exit / ChildHandle::exit / kill with exact exit_signal/2 rules (Normal ignored by non-trapping actors, everything but kill trappable); stop/stop_with_reason/shutdown stay administrative stops.
• A parent's exit (supervisor, system, start_linked parent) ends a trapping actor through stopped(), never via exit_received; kill escalation at shutdown_timeout.
• NoProc for link/monitor/request after D; unlink/demonitor fence notices in flight.
• ExitReason #[non_exhaustive] + Killed, NoProc.
• Supervisor first-start failure always aborts start(); ready children's exits during startup are processed after it; start() returns its error after rollback.
• Runtime-dropped actors end Killed in both modes.

Reviews

Four rounds, Codex and agy, each without the author's answers to the open questions. Final: Codex go with one minor (fixed), agy go. Every finding is mapped in "Review resolutions".

Maintainer decisions (recorded in the doc's "Decisions")

1. Non-trapping late link: NoProc exit signal; try_link -> Result<(), NoProc> for explicit handling.
2. stopped() skipped on a kill and on untrapped exit signals / link notices.
3. Runtime-dropped actors end Killed.
4. ActorStopped carries the exit reason; NoProc for sends/requests after the death point, once rank 11 (feat: deferred replies and pipe-to-self (rank 11) #239) lands.
5. stop_with_reason(Kill) stays administrative, ending Kill.
6. shutdown() stays administrative.
7. No opt-in retry for first starts.
8. A late non-kill signal during exit replaces the reason.

The doc also lists the required rank 11 / DeferredReplies.tla changes (death point right after stopped(), held exit errors answered at death, callers/Down/wait_exit share one reason).

Verification status

TLC 2.19 on fede, 4 workers, nice 19: MCLifecycle 43.3M states, no error (6m55s); MCLifecycleLive 324k, no error; MCLifecycleFence 388k, no error. All 19 negative-control checks produce their counterexample. Weekly MCLifecycleDeep / MCLifecycleLiveDeep and optional Apalache run after the canary window ends (~2026-11-11 23:21 UTC).

[github-actions]

🤖 Codex Code Review

• [P2] Model kill-before-cleanup separately from kill-during-cleanup — Lifecycle.tla:176–182. Begin immediately sets hook = TRUE for an administrative or self-stop, and a subsequent kill preserves it. This conflates “exit requested while the current handler finishes” with “stopped() already running.” The contract requires a kill in the former window to skip stopped(), but the model cannot represent or verify that behavior. Add a separate hook-start transition and a negative control for starting the hook after a pending kill.

No Rust runtime changes are included. TLC was not run during this review.

---

Automated review by OpenAI Codex · gpt-6.1-sol · custom prompt

[github-actions]

🤖 Claude Code Review

Review: PR #237, OTP exit-signals design and Lifecycle.tla

This PR adds a design document and a TLA+ model; it contains no Rust code. The design is careful and mostly follows OTP. The negative-control setup is good.

The review covers four areas:

• Design gaps that matter for implementation.
• Places where the model is weaker than the document claims.
• Small problems in the model and tooling.
• Readability nits.

Design (docs/design/otp-exit-signals.md)

1. The locking protocol does not fix a lock order across the three structures

The E6 "Locking protocol" says two things:

• The death point D "locks only the dying actor's own table".
• Delivery enqueues into the receiver's mailbox "inside that critical section".

Phase 4, however, says D also closes mailbox admission and the reply registry in "one critical section". That gives two code paths with opposite lock order:

• Delivery to actor X takes X's exit table, then X's mailbox.
• D for X takes X's mailbox and registry, plus its exit table.

If D takes the mailbox lock first, this is an AB/BA deadlock.

Suggested change: state a global order, for example exit table → registry → mailbox. Also require that no mailbox or registry path ever takes the exit table.

Two related requirements should be stated:

• Enqueuing while holding a mutex must be non-blocking: an unbounded queue or try_send, never an awaiting send.
• "Requesting the stop" inside the critical section must not run user callbacks. In threads mode, check what cancel() triggers.

2. Killed and NoProc can be forged

Alternative 2 rejects keeping Kill because "an observer cannot tell 'the peer killed itself' from 'someone killed the peer'". Yet E5 lets anyone call stop_with_reason(Killed) or exit(target, NoProc). That brings back the same ambiguity under the new names.

Consider one of these options:

• Reject these two reasons in stop_with_reason/exit and map them to Shutdown, logging a debug warning.
• State plainly in E5 that Killed only means "Killed or claimed Killed".

3. API footgun: two Kill paths on ChildHandle behave differently

handle.exit(Kill) ends Killed, but handle.stop_with_reason(Kill) ends Kill. They sit on the same type and look the same at the call site.

Decision 5 keeps this. Even so, consider #[deprecated] or a doc-lint on stop_with_reason(ExitReason::Kill) that points to kill().

4. Decision 1 changes behaviour without changing the signature

Today, a non-trapping ctx.link(&h) to a peer that exited Normal is harmless. In v0.8 it kills the caller with the abnormal NoProc. That causes:

• A supervisor restart of the caller.
• Propagation of NoProc over the caller's links.

The migration table lists it, but nothing at compile time will catch it. Consider a #[must_use]-style doc warning on link, and recommend try_link in the guide.

5. Requests with no deadline can hang

Phase 2 "Exit errors wait for D" means a caller whose handler panicked is not answered until D. If stopped() hangs, it waits until its own deadline.

Suggested change: confirm that every request path has a deadline. Any API without a timeout would now hang where today it gets an immediate ActorStopped.

6. The review history is long and partly stale

The resolution tables contradict the current text in places:

• Round 2, Codex 4: "late link NoProc not [cancellable]" was reversed in round 3.
• Round 2, agy 6: "RestartFollowsPolicy requires initial" is now sready.

A reader of a "contract" document should not have to work out which rule is current. Suggested change: move the review rounds into the PR discussion or an archive file, and keep only the decisions.

Model (verification/tla/Lifecycle.tla)

7. Several controls test an atomic step, not the real race

• Retain182 and Enqueue: the target-alive check and the push happen in one step. The fault only skips the check. The real Fix requests retained by mailbox publication racing actor shutdown #182 bug was a check-then-publish race against shutdown, which this model cannot express.
• Dispatch185 and NoDispatchAfterStop: afterStop can only be set under the fault, so without the fault the invariant holds trivially.
• NoEdgeToDead and the E4 "linearised" claim: Link/Monitor read IsGone atomically, so the model assumes the locking protocol instead of checking it.

These controls show that the invariants catch a wrong result. They do not show that the protocol prevents the race.

Suggested change: either split Enqueue and registration into separate check and commit steps, under a lock modelled as a variable, or narrow the claims in "What the model establishes" and README "Next model".

8. Phase 0 (Starting) is not modelled

Actors begin in "run", and LinkParent links are fixed at Init with both actors alive. The following design rules are therefore unchecked:

• Signals held during started().
• Their in-order resolution when started() returns.
• The readiness commit.
• The NoProc parent exit when a start_linked parent is already past D.

Suggested change: add these to "Not modelled", or model them.

9. Signal: the code does not match its comment

The comment says "A trapping actor queues an Exit it never handles". When the target is stopping and trapping, the code falls through to UNCHANGED <<life, mbox>> and drops the signal instead.

This is harmless for the current properties, because Die clears the mailbox. Still, fix either the comment or the code so it matches the precedence-table row "the Exit is queued and never dispatched".

10. PanicWhileExiting is enabled too widely

PanicWhileExiting is enabled whenever the actor is stopping, including when hook[a] = FALSE. In that state no user code can run: handlers are atomic and stopped() was skipped, for example after an untrapped signal.

This over-approximates: a panic can overwrite a signal's reason with no code to raise it. Suggested change: guard it with hook[a], or document the over-approximation.

11. The Begin comment is stale

"the first requested reason wins until D, except kill" no longer holds. Decision 8 lets late signals replace the reason as well.

12. Model nits

• Past(a, s): the parameter a is unused.
• TryLink sits between the Unlink comment block and Unlink, so the comment appears to describe TryLink.
• SupShutdown: the trailing \* already exiting reads as if it explains the whole conjunct. Reword it, for example \* also to a child already exiting.
• MCLifecycleLiveDeep.tla line 1 has no space between MCLifecycleLiveDeep and the dashes. SANY likely accepts it, but it is inconsistent with the other modules.
• In MCLifecycleLive{,Deep}.cfg, INVARIANT SkipHook/LateSignalWins come after the PROPERTY lines. Group them with the other invariants.

Tooling (verification/tla/negative_checks.py)

13. The comment # Rank 11 design models: (module, fault, invariant it must violate). is misplaced

named_temporal was inserted under it, so the comment now sits on the new function instead of DEFERRED_CONTROLS. Move it down.

14. named_temporal ignores the return code

It relies only on matching the string "Temporal properties were violated". That is consistent with existing helpers but brittle. Consider also asserting a non-zero exit code and the absence of parse errors.

15. CI is not wired

The design says MCLifecycle, Live and Fence run "every PR" and Deep/LiveDeep weekly. No workflow changes are in this diff.

Please confirm the runner picks up the new configs. MCLifecycle takes about 7 minutes, and there are 19 negative checks on top. Please also confirm that weekly scheduling exists for the deep configs.

The document also says the MCLifecycleLiveDeep results are "on the model before the decisions". These should be re-run before claiming the deep configurations pass.

Minor documentation points

• README count: "Seventeen negative-control faults (17 safety checks, 2 liveness checks)" is correct. The design's "All 19 negative-control checks" matches it.
• try_link -> Result<(), NoProc>: NoProc here is a new error type, which shares its name with ExitReason::NoProc. Spell out the type, for example NoProcError, or return Result<(), ExitReason>.
• OTP citations: please verify that the erlang:exit_signal/2 (OTP 29) citations and anchors resolve. The whole "Terms" section is built on that function.

Verdict

The direction is sound and the model is a real improvement. Items 1 (lock order), 7 (what the model actually proves) and 8 (Phase 0 not covered) should be addressed, or explicitly scoped out, before this is called the contract for implementation. The rest are cleanups.

---

Automated review by Claude · claude-opus-5-5 · custom prompt

[github-actions]

🤖 Gemini Code Review

This is a very thorough design contract and TLA+ specification. The separation of the death point D (Phase 4) from destruction (Phase 5) and publication (Phase 6), along with the receiver-side fencing protocol and negative controls, fits together cleanly.

A few specific issues found between the design doc and Lifecycle.tla:

1. verification/tla/Lifecycle.tla:260-276 and :391 — Late Link branches on trap[a] instead of always going through inflight

In docs/design/otp-exit-signals.md (E6, lines 473–475 and Locking protocol, lines 486–491), a late link to a target past D always inserts a pending record first and then delivers NoProc through the receiver-side delivery step, so a concurrent unlink can fence it and trap_exit is read at delivery time.

In Lifecycle.tla, Link(a, b) currently branches on trap[a] at registration time:

    /\ IF IsGone(b)
       THEN /\ lates < MaxLate /\ lates' = lates + 1
            /\ IF trap[a]
               THEN /\ inflight' = inflight \cup
                        {Note(a, b, "link", IF Fault = "LateRealReason" THEN why[b] ELSE "NoProc", 0, "late", lates')}
                    /\ UNCHANGED <<life, links>>
               \* Not trapping: the caller receives a NoProc exit signal and
               \* exits (decided; try_link is the Result-returning variant).
               ELSE /\ Begin(a, IF Fault = "LateRealReason" THEN why[b] ELSE "NoProc", "noproc")
                    /\ UNCHANGED <<inflight, links>>

This causes two minor model divergences:

1. When trap[a] = FALSE, the late notice bypasses inflight, so a concurrent Unlink(a, b) cannot fence it in the model (and under Fault = "LateRealReason" with why[b] = "Normal", Begin stops a non-trapping caller with "Normal" rather than Signal ignoring "Normal").
2. When trap[a] = TRUE at Link time and SetTrap(a, FALSE) runs before Deliver(n) (possible in MCLifecycleDeep where TrapCanClear = TRUE), Deliver(n) at line 391 calls Signal(n.to, n.from, n.r, n.o, "link"), recording cause[a] = "link" instead of "noproc".

If Link(a, b) unconditionally puts Note(a, b, "link", ..., 0, "late", lates') into inflight when IsGone(b) and Deliver(n) (line 391) passes IF n.o = "late" THEN "noproc" ELSE "link" as the cause c to Signal, both trapping and non-trapping late links follow the exact two-step locking protocol in E6.

---

2. docs/design/otp-exit-signals.md:102-104 and :202-203 — Skipping stopped() when a kill or untrapped signal supersedes an exit before stopped() starts

• E1 (line 229), E3 (line 372), Interplay with rank 11 (line 595), and Migration notes (line 639) state that a kill or untrapped signal skips stopped() if stopped() has not begun yet (e.g., exit was initially requested by ctx.stop() or ChildHandle::stop() while a handler was running, and a kill or untrapped signal arrives before that handler returns and before stopped() starts).
• However, Phase 3 (line 102) says:

  stopped() runs, unless the exit was begun by a kill, an untrapped exit signal or link notice, or a runtime drop
  and line 202 says:
  A late signal does not start a skipped stopped() or stop a running one (R).

Updating lines 102 and 202 to state that stopped() is skipped when exit was begun or superseded before stopped() starts by a kill or untrapped signal will keep Phase 3 consistent with lines 229, 372, 595, and 639.

---

3. docs/design/otp-exit-signals.md:75-81 — Resolving multiple signals held during Phase 0 (started())

Lines 78–80 state:

when started() returns, the run loop resolves them in order before dispatching anything else; for a trapping actor each becomes an Exit (or parent exit) in its own place in the queue, for a non-trapping actor the first effective one begins exit.

If the actor is non-trapping when started() returns and multiple signals/kills arrived while started() was running (or started() itself requested ctx.stop() and an untrapped signal/kill also arrived during started()), resolving the remaining signals in the pre-start batch in arrival order is still needed so a later signal or kill in that batch supersedes the earlier reason per the precedence table (Decision 8 / E1). Clarifying that later signals in the pre-start batch still apply under the precedence rules would prevent an implementation from stopping resolution after the first effective signal.

---

Automated review by Gemini · gemini-4-argon · custom prompt

[github-actions]

🤖 Grok Code Review

The death-point split, kill provenance, and ordered-pair locking are sound, and the negative controls match the faults they name. The holes are places the model under-approximates the contract, plus one shutdown restart rule that is only half-specified.

Model under-approximations (verification/tla/Lifecycle.tla)

1. Trapped signals while stopping are dropped. Signal only queues when st = "run". If the actor is already exiting and trapping, the action is a no-op (ELSE IF st[a] # "run"). The precedence table says that Exit is still queued (and never dispatched). That drops per-sender FIFO for ctx.exit during stopped(), and it is observable if a later message from the same sender is still admitted (D3).

2. Non-trapping late link is not fenced. In Link, a non-trapping caller Begins with NoProc in the same step and leaves no pending record. E4/E6 say a late link always leaves a pending record and is delivered through the receiver-side step so a concurrent unlink can cancel it. CancelFenced / MCLifecycleFence never exercise that race, so an implementation that exits the caller inside the registration locks would still pass.

3. Kill does not skip a not-yet-started stopped(). On the stopping branch, Kill leaves hook unchanged and the comment says a running stopped() finishes. There is no “exit requested, stopped() not entered” state, so a kill (including SupKill) cannot clear hook. Decision 2 and the E3 escalation row depend on that race; SkipHook does not catch “kill arrived before the hook was called”.

4. PanicWhileExiting ignores hook. It can relabel an untrapped signal or link notice to Panic even when stopped() was skipped, and it clears lateSig, so LateSignalWins stays true. The precedence table only allows that panic in the current handler or in stopped().

5. Mutual death sends one notice. Fire deletes the undirected edge before the peer dies, so concurrent D on both ends cannot exchange notices. Decision 8 makes the missing notice a reason change, not just a duplicate message. Two actors exiting together is a real interleaving the invariants never see.

Unlink / Demonitor also require st = "run", so a fence cannot run during stopping, which is exactly when a late notice can still replace the reason. Phase 0 (signals held across started()) is unspecified in the model; that is fine if the claim stays “post-start”, but it does not back the phase-0 rules.

Design

• Transient restart on cleanup failure vs shutdown. The phases rule restarts a Transient child whenever a cleanup failure is set. The migration table adds “unless the supervisor is closing” only for the Shutdown row. Without that guard in the phases rule and in the Supervision.tla projection (cleanup failure mapped to the abnormal class), a destructor panic during shutdown restarts the child and can livelock shutdown. Put the closing exception on the decision itself.

• G1 vs S1. A runtime drop during the first generation is both “placement/group closure → abort start()” (S1) and “Killed → restart Permanent/Transient” (G1). Pick one for “future/thread dropped before readiness”, or the two PRs will implement opposite supervisor outcomes.

• try_link’s signature is not a type. Result<(), NoProc> will not compile; NoProc is a variant. Use Result<(), ExitReason> or a dedicated error. The kill() comment = exit(ExitReason::Kill) is easy to implement as “store Kill”; only the delivery table says a Kill signal becomes Killed while exit(Killed) stays an ordinary reason.

Docs

verification/tla/README.md says “Seventeen negative-control faults (17 safety checks, 2 liveness checks)”. That is 17 faults and 19 checks (DirectStop and SplitDeathPoint each hit two properties). The design’s “19 checks” count is the right one.

I did not find a deadlock in the locking protocol: D takes only the dying actor’s table, registration uses address order, and delivery re-checks the receiver record. That part is ready to implement as written.

---

Automated review by Grok (xAI) · grok-4.7 · custom prompt

[github-actions]

🤖 Kimi Code Review

Found three specification/model issues. This PR contains no Rust runtime implementation, so there are no direct code-level concurrency or memory-safety changes to assess.

• High — S1’s proposed model change still permits the startup retries it is meant to remove.
  In docs/design/otp-exit-signals.md, S1 (“Model work for the implementation PR”) proposes:

  Retries(m, r, ready, init) ==
      init /\ (Restarts(m, r) \/ (~ready /\ m # "Temporary"))

  Assuming init denotes the initial start, this still retries a non-Temporary child’s failed first start and permits policy restarts during startup. That contradicts both “any first-start failure aborts” and deferral of ready-child exits until the initial start completes. The retry/restart predicate should be gated on completion of the initial start—consistent with the proposed sready requirement—while pre-readiness failures should take the abort path. As written, an implementation PR could follow this formula and preserve the v0.7 behavior.

• Medium — Lifecycle.tla cannot distinguish “stopped() has not begun” from “stopped() is already running.”
  Begin sets hook[a] immediately for self-exits, administrative stops, and parent exits (Lifecycle.tla, around lines 147–159). A subsequent Kill deliberately leaves hook unchanged (around lines 163–180), and Send treats hook[a] as permission to execute code from stopped() (around lines 233–238). Consequently, a kill arriving while the current handler is still finishing is modeled as though stopped() had already started, even though the design requires the hook to be skipped in that case. RuntimeDrop similarly leaves hook unchanged. SkipHook therefore does not fully establish the claimed kill/runtime-drop behavior. Add a phase or hookStarted flag, clear pending hooks when appropriate, and exercise both interleavings: kill before the hook starts and kill while it is running.

• Medium — ShutdownEndsChild does not establish shutdown completion “without the kill.”
  SupKill may run immediately after SupShutdown, with no deadline or other ordering constraint (Lifecycle.tla, around lines 424–433). Meanwhile, ShutdownEndsChild only requires c \in psent ~> st[c] = "dead" (around line 559). It can therefore be satisfied by escalation, a self-exit, or another unrelated exit rather than graceful parent-shutdown handling. Either disable SupKill in the configuration intended to prove graceful shutdown and strengthen the consequent to identify parent-initiated termination, or narrow the documentation/property description to “the child eventually dies.”

The D/publication separation and receiver-side fence protocol otherwise appear internally consistent, and the negative-control coverage is thoughtfully structured.

---

Automated review by Kimi (Moonshot AI) · kimi-k3.1-pro · custom prompt

[github-actions]

🤖 DeepSeek Code Review

This is a docs/TLA+ design PR, not production Rust. The design doc is thorough and the model does cover many of the intended exit-signal/lifecycle rules. However, the TLA+ model has a few fidelity/coverage issues worth fixing before relying on the verification claims.

Lifecycle.tla

1. Trapped exit signals are dropped while an actor is already "stopping"
   In Signal (around lines 165–177), the branch:

   ELSE IF st[a] # "run" THEN UNCHANGED <<life, mbox>>

   catches both "gone"/"dead" and "stopping". For a trapping actor that is already "stopping", the design says the signal is queued as an Exit/parent exit and never dispatched:

   “a non-kill exit signal … trapping actor: unchanged; the Exit is queued and never dispatched”

   The model instead discards it entirely. This under-approximates mailbox admission and can hide ordering/NoProcIffLate violations.

   Suggested fix: only ignore after D, and otherwise allow Push for trapping actors regardless of run/stopping:

   ELSE IF Past(a, st[a])
   THEN UNCHANGED <<life, mbox>>
   ELSE IF trap[a]
   THEN Push(a, Item(...))

2. Late kill does not clear hook
   In Kill’s st[a] = "stopping" branch (around lines 116–126), hook is left unchanged:

   /\ UNCHANGED <<st, trapAt, dropFrom, hook, began>>

   The design says a kill received before stopped() starts skips stopped(). Since this model only has a boolean hook, it cannot distinguish “stopped() scheduled but not started” from “stopped() already running”. As a result, SkipHook does not really verify the late-kill rule: an actor that self-exits (began = "self") and then receives a kill still has hook = TRUE, satisfying SkipHook while wrongly allowing Send via hook[a].

   Worth adding a hookStarted/hookSkipped ghost, or otherwise tightening this so the claimed SkipHook property covers late kills.

3. Dispatch OTHER branch contradicts its own comment
   Around the Dispatch handler cases:

   [] OTHER ->          \* msg or down (a panic here is SelfExit)
        UNCHANGED <<life, req>>

   The comment says a panic in a message/down handler is SelfExit, but the action provides no panic option. This under-approximates handler panics and loses a class of exits from normal message/down handlers.

   Add an explicit panic alternative, e.g.:

   [] OTHER ->
        \/ UNCHANGED <<life, req>>
        \/ Begin(a, "Panic", "self") /\ UNCHANGED req

4. PanicWhileExiting is too broad
   Currently:

   PanicWhileExiting(a) ==
       /\ st[a] = "stopping" /\ why[a] # "Panic"
       /\ ~killed[a] \/ Fault = "PanicOverKill"
       ...

   This allows a panic during "stopping" even when hook[a] = FALSE, i.e. for kills/untrapped signals where no user code is running. That over-approximates the design’s “panic in the current handler or in stopped()”.

   Consider requiring hook[a] = TRUE or introducing explicit “current handler” / “stopped() running” state to avoid modelling impossible panics.

5. Minor: Demonitor disabled after a fired monitor’s Down is delivered
   In Demonitor, the precondition requires:

   mstate[m] \in {"active", "fired", "late"} /\
   (mstate[m] = "active" \/ pending # {})

   This means once a monitor is "fired" and its Down has already been delivered (pending = {}), demonitor cannot be called. The real API allows a no-op demonitor at any time. It’s a small under-approximation, but worth a comment or adjustment if full API coverage is intended.

Overall the documentation and model are strong, but items 1–4 particularly affect the precision of the verification claims made in README.md and otp-exit-signals.md. The model should be tightened before the accompanying negative controls are relied upon as evidence for the proposed v0.8 contract.

---

Automated review by DeepSeek · deepseek-v4-pro · custom prompt