full-domain-example

A realistic Kotlin + Spring Boot 3 HTTP service in hexagonal (ports & adapters) style, where the domain logic is proven with bmc4j — its @BmcProof suite verifies the safety-critical rules for every input, not a sampled few.

It is a showcase: a normal-looking microservice (controllers, JPA, validation, a stubbed upstream service) with a clearly-drawn line between the part that is machine-checked and the part that is ordinary, unproven scaffolding.

Architecture (hexagonal)

HTTP (adapter)            Domain (framework-free core)              Driven adapters
─────────────────         ────────────────────────────             ───────────────────
OrderController     ─────► OrderService ─────► UserStatusPort ◄──── StubUserStatusAdapter
ProductController   ─────► RecommendationService ─► ProductRepo ◄── Legacy/New stub repos
   (Jakarta-validated      OrderAuthorization        OrderRepo  ◄── JpaOrderAdapter
    request DTOs)          (pure decision)           StockRepo  ◄── JpaStockAdapter (@Version)
                           value objects w/ invariants

• com.example.fde.domain — the core. Zero Spring/Jakarta/JPA annotations. Value objects with constructor invariants (Money, Quantity, RecommendationScore, OrderId, UserId, OrderValue), the ports (plain interfaces), the framework-free services (OrderService, RecommendationService), and the pure OrderAuthorization decision.
• com.example.fde.adapter.http — @RestControllers + Jakarta-validated request DTOs + the outcome→HTTP-status mapping. Converts DTOs into domain value objects at the boundary.
• com.example.fde.adapter.persistence — JPA entities (@Version optimistic locking on stock; unique index on orderId for idempotency) and the OrderRepo/StockRepo adapters.
• com.example.fde.adapter.stub — stub upstream user-status service + the two stub product catalogues.
• com.example.fde.config — the composition root that hand-wires the framework-free services from the adapter beans (the only place the domain meets Spring).

Domain rules

• User status ∈ {OK, ORDERS_BLOCKED, ORDERS_RESTRICTED} (fetched from a stubbed upstream service).
• Order authorization (OrderAuthorization.decide, a pure function):
  • ORDERS_BLOCKED → never allowed.
  • insufficient stock → blocked.
  • ORDERS_RESTRICTED → allowed iff order value ≤ $50 (the low-value cap); value > $50 → blocked.
  • OK (with stock) → allowed.
  • the decision is total — every (status, value, stock) maps to a defined outcome, never throws.
• Idempotency — POST /orders with an orderId that already exists returns 202 Accepted. This rests on the DB unique index: the adapter maps a duplicate-key violation (DataIntegrityViolationException) → ORDER_ALREADY_EXISTS → 202, rather than read-then-write.
• Stock — decremented under optimistic locking (@Version); an order is blocked if stock is insufficient.
• Products — GET /products/recommended merges the legacy + new catalogues (3 each) and sorts by recommendationScore descending, in code.

Endpoints

Method	Path	Outcome → status
POST	/orders	placed → 201 · duplicate → 202 · status-blocked / restricted-over-cap → 403 · out-of-stock → 409 · invalid body → 400
DELETE	/orders/{orderId}	204 / 404
GET	/products/recommended?userId=…	200 (merged + sorted)

The stub user-status adapter derives status from the id prefix so the API is exercisable: blk… → blocked, rst… → restricted, anything else → OK.

What bmc4j proves vs. what is scaffolding

This is the point of the showcase — the boundary is explicit.

PROVEN (machine-checked, for every input):

• Value-object invariants — every constructible Money/OrderValue is ≥ 0, every Quantity is > 0, and each invariant is genuinely enforced (construction throws exactly on the rejected inputs).
• Jakarta validation → domain precondition — a request the validation layer accepts satisfies the domain value objects' preconditions (quantity ≥ 1, valueCents ≥ 0), via the bmc-constraints-jakarta processor's generated assumeValid.
• The order-authorization decision — the headline safety proof. OrderAuthorization.decide proven clause-by-clause (ORDERS_BLOCKED ⇒ never allowed; ORDERS_RESTRICTED ∧ value > $50 ⇒ blocked, ≤ $50 ⇒ allowed; OK ⇒ allowed; no-stock ⇒ blocked) and total.
• Idempotency → 202 (the outcome contract) — a duplicate orderId signalled by the repo flows through the real OrderService (controller → service → stub-repo, hand-wired) to the ALREADY_EXISTS outcome, and the total outcome→status mapper sends ALREADY_EXISTS → 202 (and every outcome to a defined 2xx–4xx code — no domain outcome leaks a 5xx). A pinned-REFUTED demo guards that the idempotent replay never silently becomes a 201.
• Stock decrement decision/arithmetic — StockDecrement.decide proven: never decide to oversell (available < qty ⇒ refused), an allowed decrement is exactly available − qty and never negative, and the allow/deny boundary is exactly the stock check. Sequential framing (honest): jbmc is a sequential model checker, so this proves the application-level decision + arithmetic, not multithreaded race-freedom — the actual atomicity under concurrency is the DB's @Version optimistic lock; bmc4j proves the logic around that lock is correct.
• Products merge/sort — the recommendation merge is proven sorted descending by score and a permutation of the union (size preserved + multiset-equal). Tractability bound: proven over a bounded 2 + 2 = 4-element fully-symbolic-score input (production is 3 + 3 = 6); the property is size-bounded and depends only on the score key, so this demonstrates the algorithm for all score values. A pinned-REFUTED demo guards the sort direction.

NOT proven (ordinary, trusted scaffolding):

• the Spring HTTP layer, Jackson (de)serialization, JPA/Hibernate, and the H2 database;
• the stubbed upstream user-status service (its mapping is a stub, out of the proof boundary);
• the actual persistence/optimistic-lock/idempotency execution (the DB enforces these at runtime — bmc4j proves the application-level decisions, the DB provides the concurrency/uniqueness atomicity).

The proofs cover the domain logic + value invariants + validation contract + the error→status mapping's totality — the parts where a bug is a correctness/safety defect, not an integration detail.

How the proofs run

bmc4j analyzes JVM bytecode and runs as an ordinary Gradle plugin: each @BmcProof is a JUnit 5 test, so ./gradlew test runs the proof suite alongside any Spring tests. The bmc-constraints-jakarta annotation processor reads the validated bean (PlaceOrderForm, a Java mirror of the Kotlin DTO — the processor is a Java APT) and generates PlaceOrderFormConstraints.assumeValid(...), which the validation proof uses.

CI (.github/workflows/proofs.yml) runs every proof with -Dbmc.summaryDir=… and posts a per-proof report (Expected | Actual | Counterexample) as a PR comment — mirroring bmc4j's own CI report. A couple of proofs are pinned @BmcProof(expect = REFUTED): they assert a deliberately-false claim and pass by being refuted, so the report surfaces the counterexample bmc4j found (e.g. quantity = 0) and a regression that made the claim un-refutable would fail the build.

Current verdicts

29 proofs → 29 verified, 0 refuted, 0 unknown

(25 VERIFIED + 4 REFUTED-as-expected, each in ~6–23s.)

Running

./gradlew bootRun     # starts on :8080 against an in-memory H2 DB (seeded stock)
./gradlew test        # runs the @BmcProof suite (and any tests)

bmc4j is consumed from a GitHub Packages snapshot (its pre-Central channel), which needs an authenticated token with read:packages even though the packages are public — in CI the workflow's own GITHUB_TOKEN; locally gh auth token (if scoped) or -Pgpr.user=<you> -Pgpr.token=<PAT>. To validate proofs offline against a publishToMavenLocal dev build of bmc4j, pass -PbmcVersion=0.0.1-local (mavenLocal is first in settings.gradle.kts, so no token is needed).

Consumer Kotlin 2.4 is the floor (bmc4j 0.4.x); the build runs on JDK 21.

License

Apache-2.0 (matching bmc4j).