0xh3lios/dossier
A toolkit for building a model of a system, checking it with formal methods and keeping it current as the system changes. An agent drafts the specification and the models, then runs the checks. TLC, Apalache and Alloy, not the agent, decide whether each property holds. You read the result from the agent's account of what the system does, written as behaviors, where each claim is tied to the evidence for and against it. You review the specification and decide what a counterexample means.
allowed-tools
- Bash(dossier *)3 skills
- Bash(dossier doctor *)1 skill
- Bash(dossier doctor)1 skill
- Bash(dossier explore *)1 skill
- Bash(dossier recheck *)1 skill
- Bash(dossier review-basis *)1 skill
- Bash(dossier show *)1 skill
- Bash(dossier verify *)1 skill
1 more
- Bash(dossier where *)1 skill
- name
- dossier
- version
- 0.2.0
- description
- A toolkit for building a model of a system, checking it with formal methods and keeping it current as the system changes. An agent drafts the specification and the models, then runs the checks. TLC, Apalache and Alloy, not the agent, decide whether each property holds. You read the result from the agent's account of what the system does, written as behaviors, where each claim is tied to the evidence for and against it. You review the specification and decide what a counterexample means.
- license
- CC0-1.0
- repository
- https://github.com/0xh3lios/dossier
- extensions
- com.openai
{
"$schema": "https://agent-plugins.org/schemas/1.0.0/plugin.schema.json",
"name": "dossier",
"version": "0.2.0",
"description": "A toolkit for building a model of a system, checking it with formal methods and keeping it current as the system changes. An agent drafts the specification and the models, then runs the checks. TLC, Apalache and Alloy, not the agent, decide whether each property holds. You read the result from the agent's account of what the system does, written as behaviors, where each claim is tied to the evidence for and against it. You review the specification and decide what a counterexample means.",
"homepage": "https://github.com/0xh3lios/dossier",
"repository": "https://github.com/0xh3lios/dossier",
"license": "CC0-1.0",
"keywords": [
"agent-skills",
"formal-methods",
"model-checking",
"tla",
"apalache",
"alloy",
"xstate",
"statecharts"
],
"extensions": {
"com.openai": {
"onboardingSkill": "./skills/setup/SKILL.md",
"interface": {
"displayName": "Dossier",
"shortDescription": "Model a system, check it with formal methods, keep it current",
"longDescription": "A toolkit for building a model of a system, checking it with formal methods and keeping it current as the system changes. An agent drafts the specification and the models, then runs the checks. TLC, Apalache and Alloy, not the agent, decide whether each property holds. You read the result from the agent's account of what the system does, written as behaviors, where each claim is tied to the evidence for and against it. You review the specification and decide what a counterexample means.",
"category": "Developer Tools",
"capabilities": [
"Read",
"Write"
],
"websiteURL": "https://github.com/0xh3lios/dossier",
"defaultPrompt": [
"Set this repository up for dossiers.",
"Start a dossier for a part of this system.",
"Where do the dossiers stand?"
]
}
}
}
}
What else this package ships
These files come with the package and this site does not publish them. They are listed so you know what is there before you install it.
- openai.yaml
- LICENSE
Client extensions
Data this package carries for particular clients. The directory lists the clients named and never reads what is addressed to them.
- com.openai