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.
Record one of the owners' decisions on a dossier in their own words. Accept passages, reject one with a reason, give a doubt's answer, accept the risk on a violated cell, forget a recorded answer, begin or retire a dossier. The owner invokes it with the dossier, the verb and its arguments, then their words after --, such as decide timelock accept S1 -- "the delay as deployed". The words pass through untouched.
Open the explorer, a page in the person's browser that shows the dossiers root and never changes it. It lists every dossier under its next step, opens a dossier on its orientation and its behaviors in order, shows each claim's evidence and review standing, and keeps the charts, walks, traces and formal details within reach. Builds the page once with dossier explore --install, starts dossier explore and gives the address. Use for "show me the dossiers", "open the explorer" or "let me see the oracle's chart". Not for checking or changing anything.
Develop the dossier's account of a system through readable behaviors and precise claims. Form hypotheses, connect them to models and evidence, run checks, and report what the answers establish. Use to begin a part or a composition, check a claim, investigate an actor or an outage, widen a check, refresh after a change, or explain where the work stands. Not for preparing a repository or for an independent second read.
Give one behavior or a whole dossier an independent second read in a fresh context. Examine each claim against the evidence it maps to, test the scope of the explanation, and assess the formal abstraction and the recorded answers. Record the findings, and what was examined, in one review file. Use for a second opinion or an independent review. Not for adding claims, running new trials or making the owner's decisions.
Prepare a repository for dossiers or repair its installation. Run the doctor, create dossiers/ with its marker, README, package.json, .gitignore and actors files, point it at the knowledge base when there is one, install xstate once the team agrees, read the plugin's fixture as a smoke test, and verify without writing reports. Use for "set this repo up for dossiers", "is the dossier toolchain working", or to restore a damaged installation of the current version. Authors no part or composition dossier.