property + generator + oracle

Sistem tidak hanya menerima input.
Sistem berubah state.
Sistem memproses command.
Sistem menghasilkan event.
Sistem punya lifecycle.
Sistem punya invariant lintas entity.
Sistem harus benar setelah ratusan kombinasi aksi.

@Test
void submittedCaseCanBeApproved() {
    EnforcementCase c = EnforcementCase.draft(...);

    c.submit(...);
    c.approve(...);

    assertThat(c.status()).isEqualTo(CaseStatus.APPROVED);
}

submit twice
cancel after submit
approve after reject
escalate after close
retry command with same id
receive event out of order
update stale version
apply compensation twice
change owner while approval pending

Do not only generate values.
Generate histories.

Arbitraries.integers().between(1, 100)

caseId required
subject required
jurisdiction required
status must match lifecycle
submittedAt exists only after submit
closedAt exists only after close
assignedOfficer required after assignment
sanction cannot exist before decision
appeal deadline depends on decision date
case cannot be closed while active appeal exists

new EnforcementCase(
    randomId,
    randomStatus,
    randomSubmittedAt,
    randomClosedAt,
    randomDecision,
    randomAppeal
)

A domain generator must generate possible worlds.
Not random field assignments.

static Arbitrary<String> safeAlphaNumeric(int min, int max) {
    return Arbitraries.strings()
        .withChars("abcdefghijklmnopqrstuvwxyz0123456789")
        .ofMinLength(min)
        .ofMaxLength(max);
}

static Arbitrary<CaseId> caseIds() {
    return safeAlphaNumeric(8, 16).map(CaseId::new);
}

static Arbitrary<Subject> subjects() {
    return Combinators.combine(
        safeAlphaNumeric(3, 20),
        Arbitraries.of(SubjectType.PERSON, SubjectType.COMPANY)
    ).as(Subject::new);
}

static Arbitrary<EnforcementCase> draftCases() {
    return Combinators.combine(
        caseIds(),
        subjects(),
        jurisdictions()
    ).as((id, subject, jurisdiction) ->
        EnforcementCase.openDraft(id, subject, jurisdiction)
    );
}

sealed interface CaseCommand permits SubmitCase, AssignOfficer, ApproveCase, RejectCase, CloseCase {}

record CaseTrace(EnforcementCase initial, List<CaseCommand> commands) {}

status = DRAFT, submittedAt = 2026-07-02
status = CLOSED, closedAt = null
status = APPROVED, decision = null
status = CANCELLED, approvalEvent exists

static EnforcementCase submittedCase(...) {
    EnforcementCase c = EnforcementCase.openDraft(...);
    c.submit(...);
    return c;
}

static EnforcementCase underReviewCase(...) {
    EnforcementCase c = submittedCase(...);
    c.assign(...);
    return c;
}

Use domain operations to build states.
Do not bypass invariants through constructors.

record Order(
    OrderId id,
    String currency,
    List<OrderLine> lines,
    OrderStatus status,
    Instant submittedAt,
    int version
) {}

final class OrderArbitraries {

    static Arbitrary<Order> draftOrders() {
        Arbitrary<String> currency = Arbitraries.of("IDR", "USD");

        return currency.flatMap(c ->
            Combinators.combine(
                orderIds(),
                orderLines(c).list().ofMinSize(1).ofMaxSize(20)
            ).as((id, lines) -> Order.draft(id, c, lines))
        );
    }

    static Arbitrary<OrderLine> orderLines(String currency) {
        return Combinators.combine(
            skus(),
            Arbitraries.integers().between(1, 100),
            money(currency)
        ).as(OrderLine::new);
    }
}

Combinators.combine(orderCurrency(), lineCurrency(), amount())

valid generator   = object yang harus diterima
invalid generator = object yang harus ditolak

@Provide
Arbitrary<Order> validDraftOrders() {
    return OrderArbitraries.draftOrders();
}

@Property
void validDraftOrdersCanBePriced(@ForAll("validDraftOrders") Order order) {
    Money total = pricing.total(order);

    assertThat(total).isGreaterThanOrEqualTo(Money.zero(order.currency()));
}

@Property
void orderWithoutLinesIsRejected(@ForAll("validDraftOrders") Order valid) {
    Order invalid = valid.withLines(List.of());

    assertThatThrownBy(() -> pricing.total(invalid))
        .isInstanceOf(DomainValidationException.class)
        .hasMessageContaining("at least one line");
}

generate valid base
mutate one invariant
assert exact rejection

sealed interface CaseCommand {
    CommandId commandId();
}

record SubmitCase(CommandId commandId, OfficerId submittedBy, Instant submittedAt) implements CaseCommand {}
record AssignOfficer(CommandId commandId, OfficerId officerId) implements CaseCommand {}
record ApproveCase(CommandId commandId, OfficerId approvedBy, Instant decidedAt) implements CaseCommand {}
record RejectCase(CommandId commandId, OfficerId rejectedBy, String reason, Instant decidedAt) implements CaseCommand {}
record CloseCase(CommandId commandId, OfficerId closedBy, Instant closedAt) implements CaseCommand {}

static Arbitrary<CaseCommand> validCommandFor(CaseStatus status) {
    return switch (status) {
        case DRAFT -> Arbitraries.oneOf(submitCommands(), cancelCommands());
        case SUBMITTED -> assignOfficerCommands();
        case UNDER_REVIEW -> Arbitraries.oneOf(approveCommands(), rejectCommands());
        case APPROVED, REJECTED -> closeCommands();
        case CANCELLED, CLOSED -> Arbitraries.of();
    };
}

DraftTrace := Cancel | Submit SubmittedTrace
SubmittedTrace := Assign ReviewTrace
ReviewTrace := Approve ClosedTrace | Reject ClosedTrace
ClosedTrace := Close | epsilon

static Arbitrary<List<CaseCommand>> validCaseTraces() {
    return Arbitraries.oneOf(
        cancelTrace(),
        submitAssignApproveCloseTrace(),
        submitAssignRejectCloseTrace(),
        submitAssignApproveTrace(),
        submitAssignRejectTrace()
    );
}

static Arbitrary<List<CaseCommand>> submitAssignApproveCloseTrace() {
    return Combinators.combine(
        submitCommands(),
        assignOfficerCommands(),
        approveCommands(),
        closeCommands()
    ).as((submit, assign, approve, close) ->
        List.of(submit, assign, approve, close)
    );
}

@Property
void validCaseTraceAlwaysPreservesInvariants(
    @ForAll("draftCases") EnforcementCase initial,
    @ForAll("validCaseTraces") List<CaseCommand> commands
) {
    EnforcementCase c = initial;

    for (CaseCommand command : commands) {
        c = c.handle(command);

        assertCaseInvariants(c);
    }
}

private static void assertCaseInvariants(EnforcementCase c) {
    assertThat(c.id()).isNotNull();
    assertThat(c.subject()).isNotNull();

    switch (c.status()) {
        case DRAFT -> {
            assertThat(c.submittedAt()).isNull();
            assertThat(c.closedAt()).isNull();
            assertThat(c.decision()).isNull();
        }
        case SUBMITTED -> {
            assertThat(c.submittedAt()).isNotNull();
            assertThat(c.closedAt()).isNull();
        }
        case UNDER_REVIEW -> {
            assertThat(c.assignedOfficer()).isNotNull();
            assertThat(c.closedAt()).isNull();
        }
        case APPROVED, REJECTED -> {
            assertThat(c.decision()).isNotNull();
            assertThat(c.closedAt()).isNull();
        }
        case CLOSED -> {
            assertThat(c.closedAt()).isNotNull();
            assertThat(c.decision()).isNotNull();
        }
        case CANCELLED -> {
            assertThat(c.cancelledAt()).isNotNull();
        }
    }
}

Generate history.
Execute history.
Assert invariant after each step.

@Property
void terminalCasesRejectAllMutatingCommands(
    @ForAll("terminalCases") EnforcementCase terminal,
    @ForAll("mutatingCommands") CaseCommand command
) {
    assertThatThrownBy(() -> terminal.handle(command))
        .isInstanceOf(IllegalStateTransitionException.class);
}

static Arbitrary<EnforcementCase> terminalCases() {
    return Arbitraries.oneOf(
        closedCases(),
        cancelledCases()
    );
}

@Property
void invalidCommandsAreRejectedWithoutChangingState(
    @ForAll("caseAndInvalidCommand") CaseInvalidCommand sample
) {
    EnforcementCase before = sample.caseAggregate();
    CaseCommand invalid = sample.command();

    assertThatThrownBy(() -> before.handle(invalid))
        .isInstanceOf(IllegalStateTransitionException.class);

    assertThat(before).isEqualTo(sample.caseAggregate());
}

EnforcementCase snapshot = before.copy();

Applying the same command twice with the same commandId must not duplicate effects.

@Property
void duplicateSubmitCommandIsIdempotent(
    @ForAll("draftCases") EnforcementCase draft,
    @ForAll("submitCommands") SubmitCase submit
) {
    EnforcementCase once = draft.handle(submit);
    EnforcementCase twice = once.handle(submit);

    assertThat(twice.status()).isEqualTo(once.status());
    assertThat(twice.domainEvents())
        .filteredOn(e -> e instanceof CaseSubmitted)
        .hasSize(1);
}

@Property
void sameCommandIdWithDifferentPayloadIsRejected(
    @ForAll("draftCases") EnforcementCase draft,
    @ForAll("submitCommands") SubmitCase submit,
    @ForAll("differentOfficerIds") OfficerId otherOfficer
) {
    SubmitCase conflicting = new SubmitCase(
        submit.commandId(),
        otherOfficer,
        submit.submittedAt()
    );

    EnforcementCase submitted = draft.handle(submit);

    assertThatThrownBy(() -> submitted.handle(conflicting))
        .isInstanceOf(IdempotencyConflictException.class);
}

sealed interface CaseEvent {}
record CaseOpened(CaseId id, Subject subject, Jurisdiction jurisdiction) implements CaseEvent {}
record CaseSubmitted(CaseId id, OfficerId by, Instant at) implements CaseEvent {}
record OfficerAssigned(CaseId id, OfficerId officerId) implements CaseEvent {}
record CaseApproved(CaseId id, OfficerId by, Instant at) implements CaseEvent {}
record CaseClosed(CaseId id, OfficerId by, Instant at) implements CaseEvent {}

@Property
void replayingGeneratedValidEventHistoryBuildsValidAggregate(
    @ForAll("validEventHistories") List<CaseEvent> history
) {
    EnforcementCase c = EnforcementCase.replay(history);

    assertCaseInvariants(c);
}

@Property
void commandGeneratedEventsCanBeReplayedToSameState(
    @ForAll("draftCases") EnforcementCase initial,
    @ForAll("validCaseTraces") List<CaseCommand> commands
) {
    EnforcementCase live = initial;
    List<CaseEvent> allEvents = new ArrayList<>();

    for (CaseCommand command : commands) {
        HandlingResult result = live.handle(command);
        live = result.newState();
        allEvents.addAll(result.events());
    }

    EnforcementCase replayed = EnforcementCase.replay(allEvents);

    assertThat(replayed).usingRecursiveComparison()
        .ignoringFields("transientRuntimeFields")
        .isEqualTo(live);
}

event missing field
apply method diverges from command handler
snapshot/replay mismatch
event order bug
version increment bug

rich entity, validation, audit, events, persistence concerns

small immutable state machine with expected transitions

record CaseModel(CaseStatus status, boolean hasAssignee, boolean hasDecision) {

    CaseModel apply(CaseCommand command) {
        return switch (status) {
            case DRAFT -> switch (command) {
                case SubmitCase ignored -> new CaseModel(CaseStatus.SUBMITTED, false, false);
                case CancelCase ignored -> new CaseModel(CaseStatus.CANCELLED, false, false);
                default -> throw new ModelInvalidTransition();
            };
            case SUBMITTED -> switch (command) {
                case AssignOfficer ignored -> new CaseModel(CaseStatus.UNDER_REVIEW, true, false);
                default -> throw new ModelInvalidTransition();
            };
            case UNDER_REVIEW -> switch (command) {
                case ApproveCase ignored -> new CaseModel(CaseStatus.APPROVED, true, true);
                case RejectCase ignored -> new CaseModel(CaseStatus.REJECTED, true, true);
                default -> throw new ModelInvalidTransition();
            };
            case APPROVED, REJECTED -> switch (command) {
                case CloseCase ignored -> new CaseModel(CaseStatus.CLOSED, hasAssignee, hasDecision);
                default -> throw new ModelInvalidTransition();
            };
            case CLOSED, CANCELLED -> throw new ModelInvalidTransition();
        };
    }
}

@Property
void aggregateMatchesReferenceModel(
    @ForAll("validCaseTraces") List<CaseCommand> commands
) {
    EnforcementCase aggregate = EnforcementCase.openDraft(...);
    CaseModel model = new CaseModel(CaseStatus.DRAFT, false, false);

    for (CaseCommand command : commands) {
        aggregate = aggregate.handle(command);
        model = model.apply(command);

        assertThat(aggregate.status()).isEqualTo(model.status());
        assertThat(aggregate.assignedOfficer().isPresent()).isEqualTo(model.hasAssignee());
        assertThat(aggregate.decision().isPresent()).isEqualTo(model.hasDecision());
    }
}

A case cannot be closed if there is an active appeal.
A customer cannot have more active credit exposure than limit.
A quote cannot be ordered after expiry.
A payment cannot be captured above authorized amount.
A user cannot approve their own request.
An enforcement action cannot reference a deleted subject.

record CaseWorld(
    EnforcementCase enforcementCase,
    List<Appeal> appeals,
    List<OfficerAssignment> assignments,
    List<Sanction> sanctions
) {}

static Arbitrary<CaseWorld> worldsWithActiveAppeal() {
    return Combinators.combine(
        casesWithDecision(),
        activeAppeals().list().ofMinSize(1).ofMaxSize(3),
        assignments(),
        sanctions()
    ).as(CaseWorld::new);
}

@Property
void caseWithActiveAppealCannotBeClosed(
    @ForAll("worldsWithActiveAppeal") CaseWorld world,
    @ForAll("closeCommands") CloseCase close
) {
    CaseService service = serviceWith(world);

    assertThatThrownBy(() -> service.handle(world.enforcementCase().id(), close))
        .isInstanceOf(DomainPolicyViolation.class)
        .hasMessageContaining("active appeal");
}

appeal must be submitted within 14 days after decision
quote expires after validUntil
SLA escalates after 2 business days
payment capture must happen before authorization expiry
case cannot be reopened after retention lock

static Arbitrary<Instant> instantsAround(Instant anchor) {
    return Arbitraries.longs().between(-20, 20)
        .map(days -> anchor.plus(Duration.ofDays(days)));
}

static Arbitrary<Instant> appealSubmissionTimes(Instant decisionAt) {
    return Arbitraries.of(
        decisionAt,
        decisionAt.plus(Duration.ofDays(13)),
        decisionAt.plus(Duration.ofDays(14)),
        decisionAt.plus(Duration.ofDays(15)),
        decisionAt.minus(Duration.ofSeconds(1))
    );
}

@Property
void appealDeadlineBoundaryIsEnforced(
    @ForAll("decidedCases") EnforcementCase decided,
    @ForAll("appealSubmissionTimes") Instant submittedAt
) {
    boolean withinDeadline = !submittedAt.isAfter(decided.decisionAt().plus(Duration.ofDays(14)));

    if (withinDeadline) {
        assertThatCode(() -> decided.submitAppeal(submittedAt)).doesNotThrowAnyException();
    } else {
        assertThatThrownBy(() -> decided.submitAppeal(submittedAt))
            .isInstanceOf(AppealDeadlineExceeded.class);
    }
}

Case DRAFT
Case submitted
Case assigned
Finding created
Notice issued
Response received
Decision made
Sanction imposed
Appeal possible
Case closed

notice cannot be issued before investigation starts
response cannot be received before notice issued
decision cannot be made while response window open unless response received
sanction requires adverse decision
appeal exists only for sanction decision
case cannot close with unresolved appeal
all externally visible decisions must be audit logged

@Property
void regulatoryLifecycleTracePreservesLegalInvariants(
    @ForAll("regulatoryTraces") RegulatoryTrace trace
) {
    RegulatoryCase c = RegulatoryCase.openDraft(trace.caseId(), trace.subject());

    for (RegulatoryCommand command : trace.commands()) {
        c = c.handle(command);
        assertLegalInvariants(c);
    }
}

private static void assertLegalInvariants(RegulatoryCase c) {
    if (c.status().isAfterOrEqual(RegulatoryStatus.NOTICE_ISSUED)) {
        assertThat(c.notice()).isPresent();
        assertThat(c.investigationStartedAt()).isPresent();
    }

    if (c.response().isPresent()) {
        assertThat(c.notice()).isPresent();
        assertThat(c.response().get().receivedAt())
            .isAfterOrEqualTo(c.notice().get().issuedAt());
    }

    if (c.sanction().isPresent()) {
        assertThat(c.decision()).isPresent();
        assertThat(c.decision().get().type()).isEqualTo(DecisionType.ADVERSE);
    }

    if (c.status() == RegulatoryStatus.CLOSED) {
        assertThat(c.appeals()).allMatch(Appeal::isResolved);
    }
}

If a submitted case remains unassigned for more than 2 business days, escalate to supervisor.

record EscalationScenario(
    EnforcementCase submittedCase,
    Instant now,
    boolean expectedEscalation
) {}

static Arbitrary<EscalationScenario> escalationScenarios() {
    Instant submittedAt = Instant.parse("2026-07-01T00:00:00Z");

    return Arbitraries.of(
        new EscalationScenario(submittedCaseAt(submittedAt), submittedAt.plus(1, DAYS), false),
        new EscalationScenario(submittedCaseAt(submittedAt), submittedAt.plus(2, DAYS), false),
        new EscalationScenario(submittedCaseAt(submittedAt), submittedAt.plus(3, DAYS), true)
    );
}

@Property
void escalationPolicyMatchesScenario(
    @ForAll("escalationScenarios") EscalationScenario scenario
) {
    EscalationDecision decision = policy.evaluate(
        scenario.submittedCase(),
        scenario.now()
    );

    assertThat(decision.shouldEscalate()).isEqualTo(scenario.expectedEscalation());
}

Requester cannot approve own request.
Approval amount limit depends on approver role.
At least two approvals required for amount > threshold.

record ApprovalWorld(
    Request request,
    User requester,
    User approver,
    ApprovalPolicy policy
) {}

@Property
void requesterCannotApproveOwnRequest(
    @ForAll("approvalWorldsWhereApproverIsRequester") ApprovalWorld world
) {
    assertThatThrownBy(() -> approvalService.approve(
        world.request().id(),
        world.approver().id()
    )).isInstanceOf(SelfApprovalNotAllowed.class);
}

@Property
void approvalRequiresSufficientAuthority(
    @ForAll("approvalWorlds") ApprovalWorld world
) {
    boolean allowed = world.approver().limit().compareTo(world.request().amount()) >= 0
        && !world.approver().id().equals(world.requester().id());

    if (allowed) {
        assertThatCode(() -> approve(world)).doesNotThrowAnyException();
    } else {
        assertThatThrownBy(() -> approve(world)).isInstanceOf(ApprovalPolicyViolation.class);
    }
}

For all valid event histories, if events are delivered with duplicates and permitted reorderings, projection remains eventually consistent.

record DeliveryPlan(
    List<DomainEvent> original,
    List<DomainEvent> delivered
) {}

static Arbitrary<DeliveryPlan> deliveryPlans() {
    return validEventHistories().flatMap(history ->
        duplicateAndReorderWithinConstraints(history)
            .map(delivered -> new DeliveryPlan(history, delivered))
    );
}

@Property
void projectionIsIdempotentUnderDuplicateDelivery(
    @ForAll("deliveryPlans") DeliveryPlan plan
) {
    Projection projection = new Projection();

    for (DomainEvent event : plan.delivered()) {
        projection.handle(event);
    }

    Projection expected = new Projection();
    for (DomainEvent event : plan.original()) {
        expected.handle(event);
    }

    assertThat(projection.snapshot()).isEqualTo(expected.snapshot());
}

handler not idempotent
duplicate event increments counters twice
stale event overwrites newer state
missing version guard
projection assumes perfect ordering

successful command increments version by 1
rejected command does not increment version
stale command is rejected
idempotent duplicate returns same version or no-op according to policy

@Property
void successfulCommandIncrementsVersionByOne(
    @ForAll("caseWithValidNextCommand") CaseWithCommand sample
) {
    EnforcementCase before = sample.caseAggregate();
    int versionBefore = before.version();

    EnforcementCase after = before.handle(sample.command());

    assertThat(after.version()).isEqualTo(versionBefore + 1);
}

@Property
void rejectedCommandDoesNotChangeVersion(
    @ForAll("caseWithInvalidCommand") CaseWithCommand sample
) {
    EnforcementCase before = sample.caseAggregate();
    int versionBefore = before.version();

    assertThatThrownBy(() -> before.handle(sample.command()))
        .isInstanceOf(DomainException.class);

    assertThat(before.version()).isEqualTo(versionBefore);
}

organizational hierarchy
approval delegation tree
product bundle
policy expression tree
query filter expression
workflow graph

sealed interface PolicyExpr permits And, Or, Not, Condition {}
record And(PolicyExpr left, PolicyExpr right) implements PolicyExpr {}
record Or(PolicyExpr left, PolicyExpr right) implements PolicyExpr {}
record Not(PolicyExpr expr) implements PolicyExpr {}
record Condition(String field, Operator op, String value) implements PolicyExpr {}

static Arbitrary<PolicyExpr> policyExpressions(int depth) {
    if (depth == 0) {
        return conditions();
    }

    return Arbitraries.oneOf(
        conditions(),
        Combinators.combine(policyExpressions(depth - 1), policyExpressions(depth - 1)).as(And::new),
        Combinators.combine(policyExpressions(depth - 1), policyExpressions(depth - 1)).as(Or::new),
        policyExpressions(depth - 1).map(Not::new)
    );
}

@Property
void doubleNegationPreservesPolicyMeaning(@ForAll("policyExpressions") PolicyExpr expr,
                                          @ForAll("facts") Facts facts) {
    boolean original = evaluator.evaluate(expr, facts);
    boolean doubleNegated = evaluator.evaluate(new Not(new Not(expr)), facts);

    assertThat(doubleNegated).isEqualTo(original);
}

open -> submit -> assign -> add finding -> issue notice -> receive response -> update response -> decide -> sanction -> appeal -> update appeal -> close

open -> issue notice

open -> submit -> assign -> close

Keep commands immutable and small.
Avoid random unrelated fields.
Prefer lifecycle grammar over arbitrary object graph.
Use value objects with shrinkable primitives.
Keep max trace length bounded.
Avoid generator constraints that break shrinking.

@Property
void validTracePreservesInvariants(@ForAll("validTraces") CaseTrace trace) {
    Statistics.label("trace-path").collect(trace.pathName());
    Statistics.label("trace-length").collect(lengthBucket(trace.commands().size()));
    Statistics.label("terminal-state").collect(trace.expectedTerminalState());

    EnforcementCase c = trace.initial();
    for (CaseCommand command : trace.commands()) {
        c = c.handle(command);
        assertCaseInvariants(c);
    }
}

cancel path
approve path
reject path
appeal path
close path
retry path
duplicate command path
invalid transition path
boundary deadline path

src/testFixtures/java
  com.company.testing.domain
    MoneyArbitraries.java
    OrderArbitraries.java
    CaseArbitraries.java
    ApprovalArbitraries.java
    EventHistoryArbitraries.java
    DomainAssertions.java

Generators must be deterministic under seed.
Generators must be documented by domain intent.
Do not expose low-level random constructors everywhere.
Provide valid and invalid generators separately.
Keep edge cases visible.
Keep max sizes bounded.
Use builders for readability.
Review generators like production code.

@Property(tries = 25)
void commandHandlingPersistsSameStateAsPureModel(
    @ForAll("validCaseTraces") CaseTrace trace
) {
    CaseId id = repository.save(trace.initial());
    CaseModel model = CaseModel.initial();

    for (CaseCommand command : trace.commands()) {
        service.handle(id, command);
        model = model.apply(command);

        EnforcementCase loaded = repository.findById(id).orElseThrow();
        assertThat(loaded.status()).isEqualTo(model.status());
    }
}

transaction rollback per property run
small tries
isolated database schema/container
unique IDs
no shared mutable static state
tag as integration/property

For all valid commands expressible through API payload,
HTTP handler maps payload to domain command correctly,
and response reflects domain result.

@Property(tries = 50)
void submitCaseApiMatchesDomainBehavior(
    @ForAll("submitCaseRequests") SubmitCaseRequest request
) {
    HttpResponse response = api.post("/cases/{id}/submit", request);

    if (request.isValid()) {
        assertThat(response.status()).isEqualTo(200);
    } else {
        assertThat(response.status()).isEqualTo(400);
    }
}

@Property(tries = 50)
void validSubmitRequestsReturnOk(@ForAll("validSubmitRequests") SubmitCaseRequest request) {
    HttpResponse response = api.post(..., request);

    assertThat(response.status()).isEqualTo(200);
}

@Property(tries = 50)
void invalidSubmitRequestsReturnValidationError(@ForAll("invalidSubmitRequests") SubmitCaseRequest request) {
    HttpResponse response = api.post(..., request);

    assertThat(response.status()).isEqualTo(400);
    assertThat(response.body().errors()).isNotEmpty();
}

For all valid event payloads,
consumer processes event idempotently,
updates projection consistently,
and records poison events without crashing worker.

@Property(tries = 100)
void consumerIsIdempotentForDuplicateEvents(
    @ForAll("caseEvents") CaseEvent event
) {
    consumer.handle(event);
    ProjectionSnapshot once = projection.snapshotFor(event.caseId());

    consumer.handle(event);
    ProjectionSnapshot twice = projection.snapshotFor(event.caseId());

    assertThat(twice).isEqualTo(once);
}

@Property(tries = 50)
void malformedEventsGoToDeadLetterWithoutCrashing(
    @ForAll("malformedEventPayloads") byte[] payload
) {
    assertThatCode(() -> consumer.handleRaw(payload))
        .doesNotThrowAnyException();

    assertThat(deadLetterQueue).containsPayload(payload);
}

reserve inventory
authorize payment
create shipment
capture payment

For all failure points, final world has no leaked reservation or unauthorized capture.

record SagaScenario(Order order, FailurePoint failurePoint) {}

@Property
void sagaDoesNotLeakResourcesOnFailure(
    @ForAll("sagaScenarios") SagaScenario scenario
) {
    TestWorld world = TestWorld.withFailureAt(scenario.failurePoint());

    saga.execute(scenario.order(), world);

    assertThat(world.inventory().hasLeakedReservation()).isFalse();
    assertThat(world.payment().hasCapturedWithoutShipment()).isFalse();
}

reserved but never released
authorized but never voided
captured without downstream completion
compensation command emitted twice
retry creates duplicate shipment

If someone breaks this rule, does the property fail?

// original
if (riskScore <= 30) allow();

// mutant
if (riskScore < 30) allow();

generator missed boundary
property assertion weak
oracle duplicated mutant behavior
test did not reach rule

Use TLA+/Alloy to discover impossible states.
Encode discovered invariants into Java property assertions.
Encode allowed transition traces into generators.
Use Java PBT for implementation-level verification.

Request starts DRAFT.
Requester submits request.
Approver can approve if not requester and within limit.
Large requests need two distinct approvals.
Rejected request becomes terminal.
Approved request can be executed once.

sealed interface RequestCommand {}
record Submit(UserId requester) implements RequestCommand {}
record Approve(UserId approver) implements RequestCommand {}
record Reject(UserId approver, String reason) implements RequestCommand {}
record Execute() implements RequestCommand {}

executed implies approved
approved large request has at least two distinct approvers
requester not in approvers
terminal request cannot mutate

@Property
void approvalWorkflowPreservesInvariants(
    @ForAll("approvalTraces") ApprovalTrace trace
) {
    ApprovalRequest request = trace.initial();

    for (RequestCommand command : trace.commands()) {
        try {
            request = request.handle(command);
        } catch (DomainException expectedForInvalidCommand) {
            // invalid trace variant: rejection must not corrupt state
        }

        assertApprovalInvariants(request);
    }
}

private static void assertApprovalInvariants(ApprovalRequest request) {
    if (request.status() == RequestStatus.EXECUTED) {
        assertThat(request.statusHistory()).contains(RequestStatus.APPROVED);
    }

    if (request.amount().isGreaterThan(request.policy().largeRequestThreshold())
        && request.status().isAtLeast(RequestStatus.APPROVED)) {
        assertThat(request.approvers()).hasSizeGreaterThanOrEqualTo(2);
    }

    assertThat(request.approvers()).doesNotContain(request.requester());

    if (request.status().isTerminal()) {
        assertThat(request.openTasks()).isEmpty();
    }
}

customer tier
region
currency
product family
quantity bracket
voucher
promotion
tax
rounding mode
contract override

record PricingScenario(
    Customer customer,
    Product product,
    int quantity,
    Optional<Voucher> voucher,
    Region region,
    PricingExpectation expectation
) {}

@Property
void totalIsNeverNegative(@ForAll("pricingScenarios") PricingScenario scenario) {
    Price price = pricing.price(scenario);

    assertThat(price.total()).isGreaterThanOrEqualTo(Money.zero(price.currency()));
}

@Property
void higherQuantityDoesNotIncreaseUnitPriceWhenVolumeDiscountApplies(
    @ForAll("volumeDiscountScenarios") PricingScenario scenario,
    @ForAll @IntRange(min = 1, max = 1000) int extraQuantity
) {
    PricingScenario higher = scenario.withQuantity(scenario.quantity() + extraQuantity);

    Price original = pricing.price(scenario);
    Price increased = pricing.price(higher);

    assertThat(increased.unitPrice()).isLessThanOrEqualTo(original.unitPrice());
}

place order
reserve stock
authorize payment
confirm order
cancel order
ship order

duplicate place order with same idempotency key creates one order
cancel after ship is rejected
payment capture never exceeds authorized amount
shipment cannot exist before confirmation
stock reservation released when order cancelled before shipment

@Property
void duplicatePlaceOrderCreatesSingleOrder(
    @ForAll("placeOrderCommands") PlaceOrder command
) {
    OrderResult first = service.place(command);
    OrderResult second = service.place(command);

    assertThat(second.orderId()).isEqualTo(first.orderId());
    assertThat(orderRepository.countByIdempotencyKey(command.idempotencyKey())).isEqualTo(1);
    assertThat(eventStore.eventsFor(first.orderId()))
        .filteredOn(e -> e instanceof OrderPlaced)
        .hasSize(1);
}

@Provide
Arbitrary<Order> orders() {
    // 150 lines of nested generator code
}

public final class OrderArbitraries {

    public static Arbitrary<Order> draftOrders() { ... }

    public static Arbitrary<Order> submittedOrders() { ... }

    public static Arbitrary<OrderLine> lines(String currency) { ... }

    public static Arbitrary<PlaceOrder> placeOrderCommands() { ... }

    public static Arbitrary<OrderTrace> validOrderTraces() { ... }
}

validSubmittedCases()
casesWithActiveAppeal()
ordersEligibleForCancellation()
expiredQuotes()
paymentsAuthorizedButNotCaptured()
largeRequestsNeedingTwoApprovals()

new Case(randomStatus, randomDecision, randomDates)

[ ] Generator creates possible domain worlds.
[ ] Valid and invalid generators are separated.
[ ] Aggregates are built through domain operations where possible.
[ ] Trace length is bounded.
[ ] Trace paths are classified.
[ ] Invariants are checked after every step.
[ ] Oracle is independent enough from production logic.
[ ] Idempotency/retry behavior is explicit.
[ ] Temporal boundaries are included.
[ ] Cross-entity invariants are tested at service/world level.
[ ] Persistence tests are isolated and tagged.
[ ] Failing traces shrink to readable counterexamples.

Are those tests actually strong?

property too weak
generator missed important input
oracle not independent
path not exercised
assertion not specific

Generate possible worlds.
Generate meaningful traces.
Apply commands/events.
Check invariants after every step.
Compare against a simpler model where possible.
Shrink failure into readable story.

open -> submit -> assign -> close while appeal active
place order -> duplicate retry -> duplicate event
approve -> stale reject -> overwritten decision
issue notice -> decision before response deadline