# Latest **URL:** https://alloytools.discourse.group/latest.md [Latest](https://alloytools.discourse.group/latest.md) · [Categories](https://alloytools.discourse.group/categories.md) --- ## [Welcome to Alloytools](https://alloytools.discourse.group/t/welcome-to-alloytools/7)
**Author:** [@system](https://alloytools.discourse.group/u/system)\ **Replies:** 4\ **Last updated:** [August 11, 2020, 4:59pm UTC](https://alloytools.discourse.group/t/welcome-to-alloytools/7 "2020-08-11T16:59:14Z")
This is the Alloytools discussion site. Discuss any issue you feel like as long as it is related to formal modeling and/or Alloy. --- ## [Relational Algebra versus Algebra of Relations](https://alloytools.discourse.group/t/relational-algebra-versus-algebra-of-relations/573)
**Author:** [@mica](https://alloytools.discourse.group/u/mica)\ **Replies:** 0\ **Last updated:** [September 22, 2026, 4:07am UTC](https://alloytools.discourse.group/t/relational-algebra-versus-algebra-of-relations/573 "2026-09-22T04:07:00Z")
Relation algebra ≠ relational algebra One major piece of software built on it is the Alloy analyzer which calls it “relational logic” (which was incorrectly redirected to the page for relational algebra until I fixed i… --- ## [Adversarial review request: soundness of a TLA+ state projection after resource exhaustion](https://alloytools.discourse.group/t/adversarial-review-request-soundness-of-a-tla-state-projection-after-resource-exhaustion/568)
**Author:** [@ausgs](https://alloytools.discourse.group/u/ausgs)\ **Replies:** 1\ **Last updated:** [September 14, 2026, 11:25pm UTC](https://alloytools.discourse.group/t/adversarial-review-request-soundness-of-a-tla-state-projection-after-resource-exhaustion/568 "2026-09-14T23:25:13Z")
Hello, I’m seeking an adversarial formal-methods review of a narrow abstraction question arising from a TLA+ model-checking run. The original model, which I call Step 17, stored four append-only histories directly in t… --- ## [A human-subject study on how people create visualizations for Alloy](https://alloytools.discourse.group/t/a-human-subject-study-on-how-people-create-visualizations-for-alloy/571)
**Author:** [@yiliangl](https://alloytools.discourse.group/u/yiliangl)\ **Replies:** 0\ **Last updated:** [September 8, 2026, 3:32pm UTC](https://alloytools.discourse.group/t/a-human-subject-study-on-how-people-create-visualizations-for-alloy/571 "2026-09-08T15:32:59Z")
Hi everyone, I am Yiliang Liang, a PhD student at Carnegie Mellon University advised by Prof. Eunsuk Kang and Prof. Joshua Sunshine. My research is on the roles that visualizations play in making formal modeling more ac… --- ## [I created an AI skill for using Alloy](https://alloytools.discourse.group/t/i-created-an-ai-skill-for-using-alloy/562)
**Author:** [@Sam-Lam-LabLambWorks](https://alloytools.discourse.group/u/Sam-Lam-LabLambWorks)\ **Replies:** 5\ **Last updated:** [September 7, 2026, 10:00pm UTC](https://alloytools.discourse.group/t/i-created-an-ai-skill-for-using-alloy/562 "2026-09-07T22:00:10Z")
I have been using Alloy 6 with AI models and I had some success but often I need to revise a few times and the AI model will also self heal on different failure modes like syntax. This skill aims to solve those issues … --- ## [Independent Alloy review request — ChronoRealm Assurance Protocol v1.2 state-transition model](https://alloytools.discourse.group/t/independent-alloy-review-request-chronorealm-assurance-protocol-v1-2-state-transition-model/570)
**Author:** [@ausgs](https://alloytools.discourse.group/u/ausgs)\ **Replies:** 0\ **Last updated:** [August 11, 2026, 3:44pm UTC](https://alloytools.discourse.group/t/independent-alloy-review-request-chronorealm-assurance-protocol-v1-2-state-transition-model/570 "2026-08-11T15:44:40Z")
TITLE: Independent Alloy review request — ChronoRealm Assurance Protocol v1.2 state-transition model BODY: Daniel Jackson recommended that I post this here. I’m seeking adversarial review of this bounded relational/st… --- ## [Am I Creating The Correct Alloy Model To Match My ERD?](https://alloytools.discourse.group/t/am-i-creating-the-correct-alloy-model-to-match-my-erd/559)
**Author:** [@OnorioCatenacci](https://alloytools.discourse.group/u/OnorioCatenacci)\ **Replies:** 0\ **Last updated:** [July 8, 2026, 3:31pm UTC](https://alloytools.discourse.group/t/am-i-creating-the-correct-alloy-model-to-match-my-erd/559 "2026-07-08T15:31:27Z")
I’m just trying to confirm that the Alloy model I’ve created sort of corresponds to a high-level ERD. I’m trying to model a database to allow me to capture all the various comic book issues I’ve got in anthology books. F… --- ## [Scopes for sigs constrained by the ordering module](https://alloytools.discourse.group/t/scopes-for-sigs-constrained-by-the-ordering-module/557)
**Author:** [@nday](https://alloytools.discourse.group/u/nday)\ **Replies:** 1\ **Last updated:** [July 8, 2026, 2:44pm UTC](https://alloytools.discourse.group/t/scopes-for-sigs-constrained-by-the-ordering-module/557 "2026-07-08T14:44:48Z")
I’ve been looking at the following small Alloy model trying to understand how scopes are chosen for sigs constrained by the ordering module: open util/ordering\[A1\] open util/ordering\[A2\] sig A {} sig A1,A2 extends A {… --- ## [Working on an Alloy Model for Protocol Specification in Web Security](https://alloytools.discourse.group/t/working-on-an-alloy-model-for-protocol-specification-in-web-security/558)
**Author:** [@laz0rde](https://alloytools.discourse.group/u/laz0rde)\ **Replies:** 0\ **Last updated:** [July 3, 2026, 11:34am UTC](https://alloytools.discourse.group/t/working-on-an-alloy-model-for-protocol-specification-in-web-security/558 "2026-07-03T11:34:58Z")
Hi everyone, I’m relatively new to Alloy and formal verification, but my core background is in offensive cyber-security and web/mobile security research. I’m looking to bridge the gap between practical security enginee… --- ## [A field report of using Alloy with agent-based development](https://alloytools.discourse.group/t/a-field-report-of-using-alloy-with-agent-based-development/555)
**Author:** [@ohpauleez](https://alloytools.discourse.group/u/ohpauleez)\ **Replies:** 12\ **Last updated:** [June 29, 2026, 1:58pm UTC](https://alloytools.discourse.group/t/a-field-report-of-using-alloy-with-agent-based-development/555 "2026-06-29T13:58:48Z")
Hi all! I wanted to share some results and high-level techniques of using Alloy as part of AI-based development, specifically using agents and harnesses. I’ll leave my own conclusions until the end of the post. And pleas… --- ## [How to tell a story using alloy models?](https://alloytools.discourse.group/t/how-to-tell-a-story-using-alloy-models/556)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 2\ **Last updated:** [June 28, 2026, 6:36pm UTC](https://alloytools.discourse.group/t/how-to-tell-a-story-using-alloy-models/556 "2026-06-28T18:36:21Z")
The books on alloy and blog posts reveal a model step by step, by additions and modifications in files, and we have a list of versions: model\_1.als, …, model\_n.als. I’d like to make this workflow less file-centric and mo… --- ## [Do not forget to play your wordle today!](https://alloytools.discourse.group/t/do-not-forget-to-play-your-wordle-today/554)
**Author:** [@alcino](https://alloytools.discourse.group/u/alcino)\ **Replies:** 0\ **Last updated:** [June 4, 2026, 5:32pm UTC](https://alloytools.discourse.group/t/do-not-forget-to-play-your-wordle-today/554 "2026-06-04T17:32:12Z")
:slightly\_smiling\_face: And sorry for ruining your game… Alcino --- ## [What does "expect 1" mean?](https://alloytools.discourse.group/t/what-does-expect-1-mean/308)
**Author:** [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\ **Replies:** 4\ **Last updated:** [May 10, 2026, 6:23am UTC](https://alloytools.discourse.group/t/what-does-expect-1-mean/308 "2026-05-10T06:23:45Z")
When you open up Alloy, the default run in the menu is “Run Default for 4 but 4 int, 4 seq expect 1.” I know what for 4 and but 4 int mean but I don’t know what “expect 1” means! Further, it doesn’t look like the spec me… --- ## [How to initialize a hard-coded sequence?](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553)
**Author:** [@cam](https://alloytools.discourse.group/u/cam)\ **Replies:** 6\ **Last updated:** [April 24, 2026, 11:27am UTC](https://alloytools.discourse.group/t/how-to-initialize-a-hard-coded-sequence/553 "2026-04-24T11:27:04Z")
I have a set of ~20 singletons. What’s the best way to create a sequence of those singletons in the order I specify? \`\`\` sig A {} // #A = 20 things that need to be in a particular order sig B { myOrder: seq A // … --- ## ["MiniSat with Unsat Core" missing as option](https://alloytools.discourse.group/t/minisat-with-unsat-core-missing-as-option/479)
**Author:** [@Auri](https://alloytools.discourse.group/u/Auri)\ **Replies:** 2\ **Last updated:** [April 23, 2026, 4:11pm UTC](https://alloytools.discourse.group/t/minisat-with-unsat-core-missing-as-option/479 "2026-04-23T16:11:16Z")
I am currently working on an description of the behavior of Red-Black-Trees in Alloy. This is a greater project than any I have done before in Alloy (I am a beginner). I have run into some problems, which I couldn’t sol… --- ## [Associativity and meaning of multi-arity signature declarations](https://alloytools.discourse.group/t/associativity-and-meaning-of-multi-arity-signature-declarations/550)
**Author:** [@nday](https://alloytools.discourse.group/u/nday)\ **Replies:** 1\ **Last updated:** [April 23, 2026, 12:09pm UTC](https://alloytools.discourse.group/t/associativity-and-meaning-of-multi-arity-signature-declarations/550 "2026-04-23T12:09:12Z")
We have been studying the associativity of the → in multi-arity relations and also the meaning of multiplicities in these declarations. Can an Alloy developer please confirm that the associativity of → is RIGHT?, i.e. … --- ## [Problems Generating Table outputs with Alloy 6.2 CLI interface](https://alloytools.discourse.group/t/problems-generating-table-outputs-with-alloy-6-2-cli-interface/537)
**Author:** [@kirk](https://alloytools.discourse.group/u/kirk)\ **Replies:** 2\ **Last updated:** [March 17, 2026, 10:00pm UTC](https://alloytools.discourse.group/t/problems-generating-table-outputs-with-alloy-6-2-cli-interface/537 "2026-03-17T22:00:32Z")
Hi, I’m running into problems using the Alloy 6.2 CLI interface to generate the tabular representation for a solution. Here’s an example using the addressBook3a.als example from the included examples directory. When I … --- ## [What are the possibilities of using alloy?](https://alloytools.discourse.group/t/what-are-the-possibilities-of-using-alloy/549)
**Author:** [@joel6603](https://alloytools.discourse.group/u/joel6603)\ **Replies:** 0\ **Last updated:** [March 5, 2026, 2:32pm UTC](https://alloytools.discourse.group/t/what-are-the-possibilities-of-using-alloy/549 "2026-03-05T14:32:30Z")
Hi, I am a post graduate student and pretty new to model checking. I got interest in alloy . I hope to do a good work in it. Can anyone suggest some problems or potential area for research which make use of alloy? --- ## [How to enforce concurrent operations?](https://alloytools.discourse.group/t/how-to-enforce-concurrent-operations/546)
**Author:** [@krisis](https://alloytools.discourse.group/u/krisis)\ **Replies:** 7\ **Last updated:** [February 27, 2026, 4:47am UTC](https://alloytools.discourse.group/t/how-to-enforce-concurrent-operations/546 "2026-02-27T04:47:23Z")
I’m trying to model a storage system which is composed of multiple shards. Any file uploaded will be placed in one of these shards. This system supports versioning, which means subsequent uploads of a file end up in the … --- ## [Implicit facts with multirelations](https://alloytools.discourse.group/t/implicit-facts-with-multirelations/548)
**Author:** [@MathewKJ2048](https://alloytools.discourse.group/u/MathewKJ2048)\ **Replies:** 0\ **Last updated:** [February 25, 2026, 1:14pm UTC](https://alloytools.discourse.group/t/implicit-facts-with-multirelations/548 "2026-02-25T13:14:52Z")
Hi, I have a question about the associativity of the arrow operator when generating implicit facts associated with multi-relations: sig A {} sig B {} sig C {} sig X { f : one A } sig Y { g : A -\> B -\> C } When creating… --- ## [Multiplicity Keyword in Subset Constraint](https://alloytools.discourse.group/t/multiplicity-keyword-in-subset-constraint/539)
**Author:** [@jackc](https://alloytools.discourse.group/u/jackc)\ **Replies:** 1\ **Last updated:** [February 21, 2026, 10:06am UTC](https://alloytools.discourse.group/t/multiplicity-keyword-in-subset-constraint/539 "2026-02-21T10:06:37Z")
Hi, I am encountering a problem with using Multiplicity keywords within a subset constraint. In the Software Abstractions Revised edition, on bottom page 275 it says In either a declaration decl ::= \[disj\] name,+ : \[… --- ## [Date Constrained To Only Month and Year](https://alloytools.discourse.group/t/date-constrained-to-only-month-and-year/545)
**Author:** [@OnorioCatenacci](https://alloytools.discourse.group/u/OnorioCatenacci)\ **Replies:** 3\ **Last updated:** [February 6, 2026, 3:31pm UTC](https://alloytools.discourse.group/t/date-constrained-to-only-month-and-year/545 "2026-02-06T15:31:06Z")
I’m working on creating a model for a set of anthology books. The anthologies themselves reprint back issues of comic books. I want to be able to record the month and year of the comic book being reprinted. The day is… --- ## [Current use of Alloy in the age of AI](https://alloytools.discourse.group/t/current-use-of-alloy-in-the-age-of-ai/544)
**Author:** [@roehst](https://alloytools.discourse.group/u/roehst)\ **Replies:** 1\ **Last updated:** [January 27, 2026, 3:39pm UTC](https://alloytools.discourse.group/t/current-use-of-alloy-in-the-age-of-ai/544 "2026-01-27T15:39:37Z")
I have been using Alloy as my daily driver now. I can spec from whole system do algorithm or protocol designs and hand it over to an LLM to code it. This was step one. Step two was tweaking Alloy to extract code from th… --- ## [Why did Alloy Analyzer stop supporting the exh and part keywords?](https://alloytools.discourse.group/t/why-did-alloy-analyzer-stop-supporting-the-exh-and-part-keywords/543)
**Author:** [@Rafa10](https://alloytools.discourse.group/u/Rafa10)\ **Replies:** 0\ **Last updated:** [December 29, 2025, 3:17am UTC](https://alloytools.discourse.group/t/why-did-alloy-analyzer-stop-supporting-the-exh-and-part-keywords/543 "2025-12-29T03:17:13Z")
/\*\* \* Generate an error message saying the given keyword is no longer supported. \*/ static ErrorSyntax hint(Pos pos, String name) { String msg = "The name \\"" + name + "\\" cannot be found."; if ("exh".equals(na… --- ## [Software Abstractions Example With Alloy 6](https://alloytools.discourse.group/t/software-abstractions-example-with-alloy-6/541)
**Author:** [@OnorioCatenacci](https://alloytools.discourse.group/u/OnorioCatenacci)\ **Replies:** 2\ **Last updated:** [November 7, 2025, 4:13pm UTC](https://alloytools.discourse.group/t/software-abstractions-example-with-alloy-6/541 "2025-11-07T16:13:49Z")
Looking at the Software Abstractions book, on page 9 there’s the following example: pred add(b, b’: Book, n: Name, a: Addr) { b’.addr = b.addr + n → a } Since Alloy 6 now reserves the single quote, I tried this (and… --- ## [How to model transactions?](https://alloytools.discourse.group/t/how-to-model-transactions/540)
**Author:** [@Alejandro](https://alloytools.discourse.group/u/Alejandro)\ **Replies:** 1\ **Last updated:** [October 27, 2025, 1:26pm UTC](https://alloytools.discourse.group/t/how-to-model-transactions/540 "2025-10-27T13:26:35Z")
Hello. I’m reading the Designing Data-Intensive Applications book by Martin Kleppmann, there’s a chapter on transaction isolation levels, and I wonder: are there any examples how transactions could be modeled? Actually,… --- ## [How do I specify options to Alloy 6.2 CLI \`exec\` command?](https://alloytools.discourse.group/t/how-do-i-specify-options-to-alloy-6-2-cli-exec-command/538)
**Author:** [@kirk](https://alloytools.discourse.group/u/kirk)\ **Replies:** 0\ **Last updated:** [August 29, 2025, 10:36pm UTC](https://alloytools.discourse.group/t/how-do-i-specify-options-to-alloy-6-2-cli-exec-command/538 "2025-08-29T22:36:44Z")
The prefs subcommand of the alloy6 CLI interface has an option to dump all options to a CLI-parsable format, which I assume that we can configure and then pass into the exec commands \[ -c, --cli \] - Sh… --- ## [New Parser using ANTLR](https://alloytools.discourse.group/t/new-parser-using-antlr/517)
**Author:** [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Replies:** 11\ **Last updated:** [August 5, 2025, 4:01pm UTC](https://alloytools.discourse.group/t/new-parser-using-antlr/517 "2025-08-05T16:01:05Z")
The current code base of Alloy started in the '90’s and has been worked on by a lot of very smart graduate students. Some of the code is absolutely brilliant but the age of the code base is clearly showing. Since Alloy s… --- ## [Looking for Mac testers](https://alloytools.discourse.group/t/looking-for-mac-testers/536)
**Author:** [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\ **Replies:** 0\ **Last updated:** [June 16, 2025, 9:27am UTC](https://alloytools.discourse.group/t/looking-for-mac-testers/536 "2025-06-16T09:27:01Z")
I’ve created a Mac version that is signed. This makes it a lot easier to use after installation. Apple seems to be more and more in the process of making it impossible to run unsigned code. I need some people that are w… --- ## [Working with integers to solve math puzzles](https://alloytools.discourse.group/t/working-with-integers-to-solve-math-puzzles/534)
**Author:** [@dpapathanasiou](https://alloytools.discourse.group/u/dpapathanasiou)\ **Replies:** 3\ **Last updated:** [April 23, 2025, 9:43am UTC](https://alloytools.discourse.group/t/working-with-integers-to-solve-math-puzzles/534 "2025-04-23T09:43:25Z")
I’ve been trying to see if I can model the following puzzle, which does have at least one solution: Find the coefficients a, b, and c for this equation such that x = 1, 2, 3, 4 results in a perfect square, but x = 5 is… [Next page](https://alloytools.discourse.group/latest.md?page=1)