Attach temporal obligations to stable logical request identities

Acceptance should identify the boundary at which the service takes responsibility for a request, such as durable admission under the modeled contract. A received network packet or an HTTP connection need not cross that boundary. Record the request identity and immutable payload association at acceptance. Define terminal outcomes explicitly: success, rejection, failure, or cancellation may discharge different promises. 'Every accepted request eventually resolves' permits a failure response unless the contract separately requires success under additional conditions. A system that rejects everything can satisfy a weak resolution statement while failing its intended purpose.

Use stable logical identifiers across transport retries, and include a generation or sequence component when a caller starts new work. A reused user identifier cannot distinguish two separate operations. Keep enough history in the model to know that acceptance occurred and which terminal result belongs to that same obligation. If production garbage-collects deduplication records, represent the retention or identity-reuse rule where it affects the contract. Otherwise a proof relying on permanent identity memory may not describe the actual retry horizon.

At-most-once effects constrain how many successful state-changing effects one logical request can cause. Eventual resolution constrains whether its obligation can remain pending forever. Neither implies the other: executing twice and eventually replying violates the first, while doing nothing forever can preserve it. Terminal consistency adds another safety requirement, such as preventing the same request generation from being both committed and cancelled when those meanings are exclusive. A compensating action requires its own semantics; it is not generally equivalent to erasing a previously visible effect.

Aggregate statements such as 'some request eventually completes' can be true while a particular accepted request starves. Quantify over each identity and inspect whether fairness applies to the relevant action instance. A bounded identity model can also hide starvation if an identifier is recycled and its old obligation disappears. If an infinite-request service is analyzed using a finite abstraction, justify how outstanding obligations are preserved. Monitor acceptance and terminal records using the same identifiers so implementation traces can be checked against the same lifecycle interpretation.

Eventually does not mean within five seconds, or within any fixed number of transitions. A deadline specification needs a modeled clock, an acceptance timestamp, and assumptions connecting clock advancement and execution to real time. Counting protocol steps is not a physical-time measurement when steps have variable durations. Clock skew, pauses, and unavailable dependencies can affect the claim. Separate a safety monitor that detects an exceeded deadline from a liveness assumption that the clock and service actually progress. A stopped clock can otherwise conceal indefinite delay in a naive model.

The queue instrument illustrates aggregate draining without identities. Reset, set λ=0 and μ=1, predict backlog one after three seconds, then take six Steps; predict backlog zero after one additional second and take two more Steps. Its starting backlog is four and each Step advances half a second. The fluid formula cannot say which of four logical requests remains outstanding, whether any particular request starves, or whether an effect was duplicated. This limitation is why per-request predicates and identity-preserving traces are necessary beside aggregate backlog metrics.