Java asks: how do we execute this?
TLA+ asks: what behaviors are possible?

concurrent workflow transitions
idempotent commands
outbox/inbox messaging
retry and timeout
optimistic locking
scheduler race
state machine terminality
distributed coordination

Case Command Processor
- menerima command ResolveCase
- harus idempotent
- memakai case status dan version
- menulis outbox event
- command bisa dikirim ulang
- dua worker bisa memproses case yang sama
- publisher bisa menerbitkan outbox event belakangan

state0 -> state1 -> state2 -> state3 -> ...

CONSTANTS  = nilai yang ditentukan oleh model checker
VARIABLES  = state sistem
Init       = kondisi state awal
Next       = semua action yang boleh mengubah state
Spec       = Init dan selalu Next
Invariant  = properti yang harus selalu benar
Liveness   = properti yang akhirnya harus terjadi

---- MODULE Example ----
EXTENDS Naturals, FiniteSets, Sequences

CONSTANTS Cases, Commands

VARIABLES status, processed, outbox

vars == << status, processed, outbox >>

Init ==
  /\ status = [c \in Cases |-> "OPEN"]
  /\ processed = {}
  /\ outbox = << >>

Next ==
  \/ SomeAction
  \/ SomeOtherAction

Spec == Init /\ [][Next]_vars

Invariant == TRUE
====

Setelah Init, setiap langkah berikutnya harus mengikuti salah satu action di Next atau stuttering step yang tidak mengubah vars.

@Transactional
public ResolveResult resolve(ResolveCaseCommand command) {
    IdempotencyRecord existing = idempotency.find(command.idempotencyKey());
    if (existing != null) {
        return existing.toResult();
    }

    CaseEntity entity = caseRepository.findByIdForUpdate(command.caseId());

    if (entity.status().isTerminal()) {
        ResolveResult result = ResolveResult.alreadyTerminal(entity.id());
        idempotency.save(command.idempotencyKey(), command.requestHash(), result);
        return result;
    }

    entity.resolve(command.resolution());
    caseRepository.save(entity);
    outbox.insert(CaseResolvedEvent.from(entity));

    ResolveResult result = ResolveResult.resolved(entity.id(), entity.version());
    idempotency.save(command.idempotencyKey(), command.requestHash(), result);
    return result;
}

class name
repository interface
JSON deserialization
JDBC statement
transaction annotation
logging format

same command processed twice
same case resolved twice
outbox event without committed state
command outcome changes across retries
two workers interleave
failure occurs between state update and outbox append

Case status:
- OPEN
- RESOLVED

Command:
- command id
- case id

P1: A case can have at most one CaseResolved event.
P2: A processed command id always maps to stable outcome.
P3: No CaseResolved event exists unless the case is RESOLVED.
P4: A RESOLVED case never returns to OPEN.

status     : case -> status
processed  : set of processed command ids
outcome    : command id -> outcome
outbox     : sequence of events

which command arrives
whether duplicate command arrives
which worker processes it
whether publisher runs

---- MODULE CaseResolveNaive ----
EXTENDS Naturals, FiniteSets, Sequences

CONSTANTS Cases, Commands

VARIABLES status, processed, outcome, outbox

vars == << status, processed, outcome, outbox >>

Statuses == {"OPEN", "RESOLVED"}
Outcomes == {"RESOLVED", "ALREADY_TERMINAL"}

Init ==
  /\ status = [c \in Cases |-> "OPEN"]
  /\ processed = {}
  /\ outcome = [cmd \in Commands |-> "NONE"]
  /\ outbox = << >>

Resolve(cmd, c) ==
  /\ cmd \in Commands
  /\ c \in Cases
  /\ status[c] = "OPEN"
  /\ status' = [status EXCEPT ![c] = "RESOLVED"]
  /\ processed' = processed \cup {cmd}
  /\ outcome' = [outcome EXCEPT ![cmd] = "RESOLVED"]
  /\ outbox' = Append(outbox, [type |-> "CaseResolved", case |-> c, command |-> cmd])

RetryAlreadyProcessed(cmd) ==
  /\ cmd \in processed
  /\ UNCHANGED << status, processed, outcome, outbox >>

Next ==
  \/ \E cmd \in Commands, c \in Cases : Resolve(cmd, c)
  \/ \E cmd \in Commands : RetryAlreadyProcessed(cmd)

Spec == Init /\ [][Next]_vars

ResolvedEvents(c) ==
  {i \in 1..Len(outbox) : outbox[i].type = "CaseResolved" /\ outbox[i].case = c}

AtMostOneResolvedEvent ==
  \A c \in Cases : Cardinality(ResolvedEvents(c)) <= 1

TerminalNeverReopens ==
  \A c \in Cases : status[c] \in Statuses
====

If your model action is too atomic, you can hide the exact race you wanted to find.

1. worker reads case
2. worker decides case is open
3. worker commits resolution
4. worker appends outbox event

inflight[worker] = case read by worker and decision captured

---- MODULE CaseResolveRace ----
EXTENDS Naturals, FiniteSets, Sequences

CONSTANTS Cases, Commands, Workers

VARIABLES status, processed, outcome, outbox, inflight

vars == << status, processed, outcome, outbox, inflight >>

Statuses == {"OPEN", "RESOLVED"}
Outcomes == {"NONE", "RESOLVED", "ALREADY_TERMINAL"}

NoWork == [cmd |-> "NONE", case |-> "NONE", observed |-> "NONE"]

Init ==
  /\ status = [c \in Cases |-> "OPEN"]
  /\ processed = {}
  /\ outcome = [cmd \in Commands |-> "NONE"]
  /\ outbox = << >>
  /\ inflight = [w \in Workers |-> NoWork]

BeginResolve(w, cmd, c) ==
  /\ w \in Workers
  /\ cmd \in Commands
  /\ c \in Cases
  /\ inflight[w] = NoWork
  /\ cmd \notin processed
  /\ inflight' = [inflight EXCEPT ![w] = [cmd |-> cmd, case |-> c, observed |-> status[c]]]
  /\ UNCHANGED << status, processed, outcome, outbox >>

CommitResolveNaive(w) ==
  LET work == inflight[w] IN
  /\ w \in Workers
  /\ work # NoWork
  /\ work.observed = "OPEN"
  /\ status' = [status EXCEPT ![work.case] = "RESOLVED"]
  /\ processed' = processed \cup {work.cmd}
  /\ outcome' = [outcome EXCEPT ![work.cmd] = "RESOLVED"]
  /\ outbox' = Append(outbox, [type |-> "CaseResolved", case |-> work.case, command |-> work.cmd])
  /\ inflight' = [inflight EXCEPT ![w] = NoWork]

CommitAlreadyTerminal(w) ==
  LET work == inflight[w] IN
  /\ w \in Workers
  /\ work # NoWork
  /\ work.observed = "RESOLVED"
  /\ processed' = processed \cup {work.cmd}
  /\ outcome' = [outcome EXCEPT ![work.cmd] = "ALREADY_TERMINAL"]
  /\ inflight' = [inflight EXCEPT ![w] = NoWork]
  /\ UNCHANGED << status, outbox >>

Next ==
  \/ \E w \in Workers, cmd \in Commands, c \in Cases : BeginResolve(w, cmd, c)
  \/ \E w \in Workers : CommitResolveNaive(w)
  \/ \E w \in Workers : CommitAlreadyTerminal(w)

Spec == Init /\ [][Next]_vars

ResolvedEvents(c) ==
  {i \in 1..Len(outbox) : outbox[i].type = "CaseResolved" /\ outbox[i].case = c}

AtMostOneResolvedEvent ==
  \A c \in Cases : Cardinality(ResolvedEvents(c)) <= 1
====

w1 begins resolve c1, observes OPEN
w2 begins resolve c1, observes OPEN
w1 commits, appends event
w2 commits, appends event
AtMostOneResolvedEvent violated

A worker may decide based on old read, but commit must check current state/version.

CommitResolveWithCheck(w) ==
  LET work == inflight[w] IN
  /\ w \in Workers
  /\ work # NoWork
  /\ work.observed = "OPEN"
  /\ status[work.case] = "OPEN"
  /\ status' = [status EXCEPT ![work.case] = "RESOLVED"]
  /\ processed' = processed \cup {work.cmd}
  /\ outcome' = [outcome EXCEPT ![work.cmd] = "RESOLVED"]
  /\ outbox' = Append(outbox, [type |-> "CaseResolved", case |-> work.case, command |-> work.cmd])
  /\ inflight' = [inflight EXCEPT ![w] = NoWork]

CommitStaleDecision(w) ==
  LET work == inflight[w] IN
  /\ w \in Workers
  /\ work # NoWork
  /\ work.observed = "OPEN"
  /\ status[work.case] = "RESOLVED"
  /\ processed' = processed \cup {work.cmd}
  /\ outcome' = [outcome EXCEPT ![work.cmd] = "ALREADY_TERMINAL"]
  /\ inflight' = [inflight EXCEPT ![w] = NoWork]
  /\ UNCHANGED << status, outbox >>

UPDATE case_table
SET status = 'RESOLVED', version = version + 1
WHERE case_id = :caseId
  AND status = 'OPEN'
  AND version = :observedVersion;

int updated = caseRepository.resolveIfOpen(caseId, observedVersion, resolution);

if (updated == 1) {
    outbox.insert(CaseResolvedEvent.of(caseId, observedVersion + 1));
    return resolved();
}

return alreadyTerminalOrConflict();

outbox insert must happen in the same transaction as the successful state update.

command id
request hash
stored outcome
side effect count

same command id never maps to two outcomes
same command id never creates two resolved events
same command id with different request hash is rejected

CONSTANTS Cases, Commands, RequestHashes, Workers

VARIABLES status, processed, requestHash, outcome, outbox, inflight

StableProcessedOutcome ==
  \A cmd \in processed : outcome[cmd] # "NONE"

VARIABLES outcomeHistory

outcomeHistory' = Append(outcomeHistory, [cmd |-> work.cmd, result |-> "RESOLVED"])

NoTwoOutcomesForSameCommand ==
  \A cmd \in Commands :
    Cardinality({r \in Outcomes :
      \E i \in 1..Len(outcomeHistory) :
        outcomeHistory[i].cmd = cmd /\ outcomeHistory[i].result = r}) <= 1

If you want to check history-dependent properties, explicitly model history.

Update aggregate in one transaction, insert outbox in another transaction.

state changed but no event exists

CommitStateOnly(w) ==
  LET work == inflight[w] IN
  /\ work # NoWork
  /\ status[work.case] = "OPEN"
  /\ status' = [status EXCEPT ![work.case] = "RESOLVED"]
  /\ processed' = processed \cup {work.cmd}
  /\ outcome' = [outcome EXCEPT ![work.cmd] = "RESOLVED"]
  /\ inflight' = [inflight EXCEPT ![w] = NoWork]
  /\ UNCHANGED outbox

ResolvedHasOutbox ==
  \A c \in Cases :
    status[c] = "RESOLVED" =>
      \E i \in 1..Len(outbox) : outbox[i].case = c /\ outbox[i].type = "CaseResolved"

The atomic unit is not “case row update”.
The atomic unit is “case row update + outbox row insert”.

CommitStateAndOutbox(w) ==
  LET work == inflight[w] IN
  /\ work # NoWork
  /\ status[work.case] = "OPEN"
  /\ status' = [status EXCEPT ![work.case] = "RESOLVED"]
  /\ processed' = processed \cup {work.cmd}
  /\ outcome' = [outcome EXCEPT ![work.cmd] = "RESOLVED"]
  /\ outbox' = Append(outbox, [type |-> "CaseResolved", case |-> work.case, command |-> work.cmd])
  /\ inflight' = [inflight EXCEPT ![w] = NoWork]

@Transactional
public ResolveResult resolve(ResolveCaseCommand command) {
    int updated = caseRepository.resolveIfOpen(command.caseId(), command.observedVersion());

    if (updated == 1) {
        outboxRepository.insert(new CaseResolvedOutboxEvent(...));
        idempotencyRepository.record(command.key(), RESOLVED);
        return ResolveResult.resolved();
    }

    idempotencyRepository.record(command.key(), ALREADY_TERMINAL);
    return ResolveResult.alreadyTerminal();
}

integration test verifies case update and outbox insert commit/rollback together
property test generates duplicate resolve commands
model counterexample becomes regression test
production metric tracks resolved cases without outbox event

SPECIFICATION Spec

CONSTANTS
  Cases = {c1}
  Commands = {cmd1, cmd2}
  Workers = {w1, w2}

INVARIANTS
  AtMostOneResolvedEvent
  ResolvedHasOutbox

If a design fails with 1 case and 2 workers, it will fail in production.

1 case, 2 commands, 2 workers
2 cases, 2 commands, 2 workers
2 cases, 3 commands, 3 workers

What was the first state where the invariant became doomed?
What action created the unsafe condition?
Was the action unrealistic or correctly modeled?
Did we omit a guard?
Did we make an action too atomic or not atomic enough?
Did the invariant overstate the requirement?

NoDuplicateTerminalEvent ==
  \A c \in Cases : Cardinality(ResolvedEvents(c)) <= 1

unique index on event semantic key
conditional update
idempotency key
consumer deduplication

NoEventWithoutResolvedState ==
  \A i \in 1..Len(outbox) :
    outbox[i].type = "CaseResolved" => status[outbox[i].case] = "RESOLVED"

same transaction for state and outbox
payload generated from persisted aggregate version
transactional tests

TerminalStateValid ==
  \A c \in Cases : status[c] \in {"OPEN", "RESOLVED"}

NeverReopened ==
  \A c \in Cases :
    WasResolved(c) => status[c] = "RESOLVED"

StableOutcome ==
  \A cmd \in Commands :
    cmd \in processed => outcome[cmd] # "NONE"

NoOutcomeChange ==
  \A cmd \in Commands :
    Cardinality(OutcomesObservedFor(cmd)) <= 1

Every outbox event is eventually published.

VARIABLES outbox, published

Publish(i) ==
  /\ i \in 1..Len(outbox)
  /\ i \notin published
  /\ published' = published \cup {i}
  /\ UNCHANGED outbox

AllOutboxEventuallyPublished ==
  \A i \in 1..Len(outbox) : <> (i \in published)

If an action remains continuously enabled, it eventually occurs.

Spec == Init /\ [][Next]_vars /\ WF_vars(PublishNext)

If publisher keeps running and broker/database eventually respond, queued events should drain.

Assuming publisher is scheduled, database is available, and broker eventually accepts writes, every committed outbox row is eventually published or moved to a terminal dead-letter state.

The model is correct, but nobody knows which part of Java enforces it.

w1 reads OPEN
w2 reads OPEN
w1 commits resolved event
w2 commits resolved event

@Test
void twoConcurrentResolveAttemptsMustProduceSingleResolvedEvent() throws Exception {
    CaseId caseId = fixtures.openCase();

    CyclicBarrier bothRead = new CyclicBarrier(2);
    CountDownLatch allowCommit = new CountDownLatch(1);

    ResolveWorker worker1 = new ResolveWorker(caseId, bothRead, allowCommit);
    ResolveWorker worker2 = new ResolveWorker(caseId, bothRead, allowCommit);

    Future<ResolveResult> f1 = executor.submit(worker1);
    Future<ResolveResult> f2 = executor.submit(worker2);

    bothRead.await(5, TimeUnit.SECONDS);
    allowCommit.countDown();

    ResolveResult r1 = f1.get(5, TimeUnit.SECONDS);
    ResolveResult r2 = f2.get(5, TimeUnit.SECONDS);

    assertThat(List.of(r1, r2))
        .filteredOn(ResolveResult::resolved)
        .hasSize(1);

    assertThat(outboxRepository.findByCaseId(caseId))
        .filteredOn(event -> event.type().equals("CaseResolved"))
        .hasSize(1);
}

The test reproduces the interleaving from the formal counterexample.

No duplicate terminal event under any modeled interleaving.

For generated command sequences with duplicate ids and random order, Java implementation maintains domain invariant.

@Property
void generatedResolveCommandsDoNotCreateDuplicateTerminalEvents(
        @ForAll("resolveCommandSequences") List<ResolveCaseCommand> commands) {

    CaseId caseId = fixtures.openCase();

    for (ResolveCaseCommand command : commands) {
        service.resolve(command.withCaseId(caseId));
    }

    assertThat(outboxRepository.caseResolvedEvents(caseId)).hasSizeLessThanOrEqualTo(1);
}

time increases automatically and continuously

Tick is an action
scheduler behavior is explicit
SLA threshold is abstracted into small finite values

VARIABLES age, status, escalated

Tick(c) ==
  /\ c \in Cases
  /\ age' = [age EXCEPT ![c] = age[c] + 1]
  /\ UNCHANGED << status, escalated >>

Escalate(c) ==
  /\ c \in Cases
  /\ status[c] = "ASSIGNED"
  /\ age[c] >= SlaLimit
  /\ escalated' = escalated \cup {c}
  /\ UNCHANGED << status, age >>

Clock injection
scheduler test harness
assignment epoch
SLA pause/resume state
idempotent escalation command

use small finite constants
model only relevant state
avoid unbounded sequences when possible
abstract payloads into symbols
reduce number of workers/entities
split specs by concern
check safety before liveness
add symmetry when appropriate

Cases = 1000
Commands = 10000
Workers = 50
full event payload records
full user objects
full timestamp values

Cases = {c1, c2}
Commands = {cmd1, cmd2, cmd3}
Workers = {w1, w2}
Status = symbolic values
Time = 0..2

A concurrency design that is wrong often fails with tiny numbers.

What production incident are we trying to prevent?
What is the smallest subsystem that contains the risk?
What are the state variables?
What actions change state?
Which actions are concurrent?
Which actions can retry?
Which actions can fail halfway?
Which operation must be atomic?
What invariant would be expensive to violate?
What progress condition matters?

Are actions too atomic?
Are actions not atomic enough?
Are duplicate messages modeled?
Are stale reads modeled?
Are crash windows modeled?
Are terminal states modeled?
Are environment assumptions explicit?

Did we run with at least two workers where concurrency matters?
Did we try at least two commands where duplication matters?
Did we check non-trivial invariants?
Did we document what the model omits?
Did we map each invariant to Java enforcement?
Did we create tests for previous counterexamples?

No violation found in this finite model with these properties.

/specs/tla/case-resolve
  CaseResolve.tla
  CaseResolve.cfg
  README.md
/src/test/java/.../CaseResolveConcurrencyTest.java
/src/test/java/.../CaseResolvePropertyTest.java
/docs/adr/ADR-021-idempotent-case-resolution.md

Purpose
State variables
Actions
Invariants
Liveness assumptions
How to run TLC
Known omissions
Counterexamples found
Java mapping
Related tests

## Java Mapping

- `status[c]` maps to `case_table.status`.
- `processed` maps to `idempotency_key.command_id`.
- `outbox` maps to `outbox_event`.
- `CommitResolveWithCheck` maps to `resolveIfOpen(caseId, observedVersion)`.
- `AtMostOneResolvedEvent` is enforced by conditional update and unique semantic event key.

resolved_case_without_outbox_count
case_resolved_event_duplicate_count
idempotency_key_conflict_count
outbox_publish_lag_seconds
resolve_optimistic_lock_conflict_count
stale_command_attempt_count

command id
case id
observed version
committed version
idempotency key
outbox event id
worker id
correlation id

Week 1: pick one painful stateful/concurrent risk
Week 1: write invariant catalog
Week 2: write small TLA+ model
Week 2: run TLC and collect counterexamples
Week 3: patch Java design and tests
Week 3: document mapping and assumptions
Week 4: use spec in design review

idempotent command processing
outbox correctness
workflow terminality
lease ownership
scheduler duplicate execution
approval separation-of-duties handoff

entire platform architecture
all business rules
large database schema
full Kafka topology
all HTTP endpoints

from example thinking
to state-space thinking

from “this path works”
to “no allowed path violates the invariant”

from “we think retry is safe”
to “duplicate and stale retries were modeled”

from “outbox exists”
to “state + outbox atomicity is enforced”

finding a concurrency bug in a model trace today

explaining a production incident months later

workers
queues
locks
retry loops
publishers
consumers
scheduler processes