Along these lines, we used Codex to collaboratively build an alloy model for verifying the authorization model of GoodMem. After building the model, we implemented the code based on it, and, while there could be a gap in the translation process, several hours of red-teaming the server (w/attacker source code access) to try and produce a privilege escalation attack using GLM 5.3 failed.
Alloy is a tool I tried to learn many years ago, but I never learned it well enough to use it for formal verification of a complex production system. Credit goes to agentic coding tools for making it a reality.
Alloy is a tool I tried to learn many years ago, but I never learned it well enough to use it for formal verification of a complex production system. Credit goes to agentic coding tools for making it a reality.
[1] https://alloytools.org/
[2] https://docs.goodmem.ai/docs/concepts/security-model/