tl;dr a "program" here is a government program (get an FFL, file a discrimination charge, apply for a benefit), codified so that every step has an actor, typed inputs and outputs, and a citation to the provision that authorizes it. Agents then walk each party through it. And note it points the opposite way from ChatGPT-drafts-your-tribunal-claim in TFA: that dynamic broke because AI made filing free while adjudicating stayed expensive, so the queue explodes. Codifying the procedure attacks the other side; what's actually required, where it actually goes, and whether you have it; before it becomes a hearing in 2030.
Fair question, and the "training course" read is not an accident; it's the same shape underneath. A program is an ordered chain of modules, each with a declared actor and typed inputs/outputs. Courses are also that. So it renders with the same components. The sequence diagram you found isn't a sample scenario, it's the deal template's actual step graph; the thing an instance runs on.
Three authored files per domain:
- an ontology: the domain's vocabulary, its regulatory frameworks with real citations, the O*NET occupations that staff it, the systems of record it touches
- intents: what a person actually shows up wanting ("open a gun store, need an FFL"), with typed parameters
- deal templates, one per intent: ordered pipeline_steps, each with an actor, inputs, outputs, and a policy_check
The page you clicked is generated from the last two deterministically. No model in that path.
The part that speaks to your TLA+ instinct: I deliberately don't formalize what the law means. I formalize the procedure, and bind each step to the provision that authorizes it. Formalizing semantics is exactly where you get the creative, detached interpretations you're worried about, because every gap gets filled by the model's guess. Formalizing procedure asks the model to transcribe and cite, which is checkable:
- every step input is a ref; param:x, step:3.some_output, system:NICS.event; and it has to resolve. A step: ref must name an earlier step's declared output, so the dataflow is a DAG with referential integrity.
- every step's policy_check must name a framework declared in the ontology. A step that no provision authorizes fails validation.
So most hallucination becomes a build error instead of a plausible sentence. That's the whole trick. Not a smarter model; a narrower artifact.
Concretely, since you're right to expect slop: my first pass at four new agencies came back with 100% of step inputs referencing parameters that didn't exist, and prompts that literally said "Subject?". The validator refused all forty programs. That's the mechanism working; I'd have merged them on a read-through.
Intents and flows for ATF, if you want to see the layer under the program page: https://wiki.doj.dev/agent/atf
Limits, since you'll ask. It decides nothing; no adjudication, and consequential steps are human-gated. It's also not a formal method: the invariants are referential integrity and citation binding, not model checking. The genuinely temporal parts are the deadlines, and those do bite; the NLRB's six-month charge window runs from filing and service, with service being the filer's own duty, so a filing-date-only clock computes the wrong date on a deadline that destroys the claim if you miss it.
Re: the sibling comment about discretion; that's the actual pitch. Discretion hides in the gap between the written rule and the practiced procedure. Writing the practiced procedure down, with a citation per step, is what makes the gap visible.