Skip to main content

IAM Contract Source of Truth

IAM behavior is owned by executable specification and runtime code, not by a standalone draft plan.

Canonical Sources​

  • Formal model and proofs: apps/specifications/dafny/iam/main.dfy
  • Functional companion spec: apps/specifications/md/merchant/iam/IAM_SPEC.md
  • Runtime engine adapter: libs/microservices/iam-engine/src/main/java/com/myriad/shared/iam/DafnyIamAdapter.kt
  • Runtime service wrapper: libs/microservices/iam-engine/src/main/java/com/myriad/shared/iam/IamService.kt
  • Merchant policy provider: apps/microservices/merchant-api/src/main/java/com/myriad/merchant_api/repository/IamRepository.kt

Current Runtime Shape​

IamService resolves the authenticated user's internal ID, ensures the org IAM seed exists, loads policies for that user/org, and evaluates the request through the compiled Dafny engine via DafnyIamAdapter.

The decision model is flat permit/deny:

  • explicit matching deny wins
  • otherwise matching permit allows
  • otherwise default deny
  • structurally invalid policies or policies with conditions are skipped

Store-scoped controllers still use membership gates before fine-grained IAM checks because IAM conditions are reserved but not evaluated today.

Validation​

Run the formal verification target and IAM engine tests when changing this surface:

bazel build //apps/specifications/dafny:verify
bazel test //libs/microservices/iam-engine:iam_engine_test