Last week we tested that approach on a new composition: Attributed Permissions Admin. It requires every permission grant and revocation to be backed by a cryptographic attestation (from the Actor Identity atom) before the grant record is written.
We spent a few days refining the prose spec, then modeled it in Alloy. The model immediately surfaced a critical gap our manual review had missed: nothing enforced disjoint attestation pools (issuance, revocation, and orphan log). A single attestation could theoretically be reused for both an issuance and a revocation. Alloy produced a clean counterexample.
We added Invariant 7 (Attestation Exclusivity), the counterexample vanished, and the design became much stronger.
Once the Alloy model was solid, we handed the spec to AI and said “build it.”
Result: A full Deno + Hono + SQLite web app with complete invariant verification and a test suite — built in under an hour. 36 tests passed on the first real run (one minor import quirk fixed in seconds).
It’s a working clinical-trial portal (PI/CRA roles, external onboarding, login, session-gated access, and subject enrollment) running over a hash-chained, tamper-evident audit trail. Its identity, authorization, onboarding, and audit machinery is composed entirely of freestanding concepts, each specified in structured English:
Concepts: Actor Identity, Party Identity, Credential, Session, Permissions, Invitation, Retention Window, Tamper Evidence, Event Log
Compositions: Login, Session-Gated Authorization, External Onboarding, Audit Trail
The point I’m trying to make concrete: each concept is written as a freestanding spec — its own state, actions, operational principle — pressure-tested until the concern boundaries hold, and the running TypeScript plus its 107-test conformance surface are derived from those specs rather than authored independently. The English spec is the canonical artifact; the code is a projection of it. Emergent invariants (audit completeness; the credential-revocation cascade — revoke a login credential and every session derived from it dies) are surfaced explicitly at composition time, since they belong to no single concept. (Today the derivation is a disciplined manual + AI process; mechanizing it is the next step.)
The full catalog — 25 concepts, 12 compositions — is at https://gracecommons.dev.
I’d genuinely value scrutiny of the boundaries: which of these “atoms” an EOS reading would say over-absorbs, or ought to split.
Really nice! Can you explain what the violation of disjointness would mean in practice? Don’t the grants get created from grant proposals, each of which has an associated attestation? Is that where the problem would arise – in an action that creates grants from attestations?
One more Alloy comment: you should be able to make the model dynamic without having to add new signatures that are dynamic variants of the static ones.
isn’t strictly needed because the sig declaration covers it, but that “stating it explicitly documents the intent and catches type-level errors in model edits.” Why isn’t the sig declaration enough for that?
Yes — your reading of the flow is right: grant proposal → attest(proposal_ref) → grant record and attribution pairing written together. But the violation isn’t located in any single action, because the static model has no actions — it characterizes valid states. The gap was that the state space permitted sharing, which means a conforming implementation’s actions were allowed to produce it.
Where it would bite in practice, two ways. A retried issue_grant after a partial failure pairs the same attestation with a second grant record — two grants, one signed authorization (the injectivity half). Or a revocation flow reuses the original issuance attestation as its revocation proof — “we already hold evidence the admin touched this grant” — so the revocation record points at an attestation whose action_ref attests to an issuance decision (the disjointness half).
Either way the operational failure is the same: an auditor asks “show me the authorization for this act” and lands on a record authorizing a different act. One attestation double-spent across two administrative decisions — and the evidentiary chain is the entire point of the composition.
The part that stung: our prose review had dismissed this with “the nonce mechanism prevents it.” True of our proposal format — but that argument lived in Configuration, not in the composition’s invariants. An implementation with a different proposal format would have conformed and still been broken. Invariant 7 moves it from “our mechanism happens to prevent it” to “any conforming implementation must.”
Taking the three Alloy notes together —
Enum shorthand: adopting it, thanks. Our instinct in the formal layer is the compressed canonical form (same reason we went pure TLA+ rather than PlusCal) — the teaching burden lives in the comments, not the syntax. The verbose form was the draft, not a position.
Dynamic model: you’re right. The Dyn* duplication was a workaround to let the static facts and the trace model coexist in one file without making the original sigs mutable. The cleaner structure is var fields throughout, transitions as facts, and the snapshot invariants checked under always — which also collapses T2/T3, since those were re-proving the static invariants anyway. Refactoring Round 4 this way.
Redundant fact: fair catch — the comment claims something the construct can’t deliver. A fact entailed by the sig declaration is inert, and if a later edit weakens the declaration, the fact doesn’t flag the change — it silently re-imposes the old constraint and masks the edit. If regression-catching is the goal, the right instrument is an assert + check that fails loudly. Removing the fact; the intent stays in prose.
Worth being plain about workflow, since it’s the thesis anyway: I’m not an Alloy hand. The models are drafted by AI from the prose spec; my job is verifying that every counterexample and every clean check maps back to something true in the spec. Review like yours is the layer that process can’t generate for itself.
So thank you!
Round 4 is up: Alloy Round 4: unify static+dynamic models on Alloy 6 var state; add … · scottromack/grace-commons@8c4b1e5 · GitHub
All three structural points adopted. The Dyn* namespace is gone — one model now, var status on Grant, var stores and maps on System. Pairing_Map_Range_Valid is removed as a fact and restated as assert + check: clean by typing today, loud if a future edit weakens the declarations, which I took to be your instrument point. And enum GrantStatus { Active, Revoked }, teaching burden moved to a comment.
One deliberate semantic change to the trace model, flagged for scrutiny: the snapshot invariants are now non-temporal facts, so they constrain only the initial state, and traces begin in arbitrary valid snapshots rather than the empty store. Their persistence is no longer assumed anywhere — it’s checked, as preservation assertions under always at 1..2 steps, which with arbitrary valid inits is the inductive step and so covers every trace depth. A side effect I didn’t expect going in: that promotes Invariant 7’s temporal half from “true by construction of the freshness preconditions” to a verified property — the model now proves the nonce mechanism maintains the invariant, rather than assuming it.
The Round 1 record stays executable: comment out the Invariant 7 fact and exactly the original three checks fail, plus the new Invariant_7_Always. That variant is now committed as a buggy twin the harness must reject.
My verification pass (per the workflow note above): the refactored model reproduces the same evidentiary story — same three counterexamples without Invariant 7, clean with it — and no English in the spec changed.
