diff --git a/changes/unreleased/grouped-help.changed.md b/changes/unreleased/grouped-help.changed.md
new file mode 100644
index 0000000000..bee3523475
--- /dev/null
+++ b/changes/unreleased/grouped-help.changed.md
@@ -0,0 +1,3 @@
+- **`sysml -help` and the manual page list the options by task.** The 84 flags come under headings — General, Evaluating, Checking a model, Running behaviors, Analysis engines, Checking every schedule, Converting and migrating, Compiling natively, Rendering views, Rendering documents, Styling HTML documents, Syncing against a repository, Diagnostics and profiling, Deprecated — instead of in one alphabetical list. Each is spelled once with its shorthand folded in (`-e, -eval <expr>`, `-o, -output <file>`) and its argument named (`<format>`, `<duration>`, `<policy>`) rather than typed (`string`, `value`); a description is a wrapped line or two, with the detail it carried moved into the section on that mode (`Checking a model`, `Running actions and state machines`, `Checking every schedule`, ...), and the three `-pdf-*` spellings sit under *Deprecated* pointing at their `-doc-*` names. The examples come first. A flag added without a heading fails a test.
+- **A mistyped flag prints the error, the synopsis and `Run 'sysml -help' for the options.`** — three lines, rather than the whole help after the error.
+- **`%help` groups every REPL command under a heading and wraps its description.** The commands that had none come under *Session*, *Settings*, *Analysis engines* and *Checking every schedule*; a description wraps into the column after its command, and a signature too wide for that column takes a line of its own. `%exit` is noted beside `%quit` rather than listed as a command.
diff --git a/cmd/sysml/main.go b/cmd/sysml/main.go
index 6d0f89e6e8..5740662402 100644
--- a/cmd/sysml/main.go
+++ b/cmd/sysml/main.go
@@ -274,10 +274,10 @@ func flagGiven(name string) bool {
 	return given
 }
 
-// printUsage writes the help to w: the caller chooses the stream, since help
-// asked for is a result and help shown over a misuse belongs with the error.
-func printUsage(w io.Writer) {
-	doc().WriteText(w, flag.CommandLine)
+// printUsage writes the help for the flags of fs to w: help asked for is a
+// result, so it goes on stdout.
+func printUsage(w io.Writer, fs *flag.FlagSet) {
+	doc().WriteText(w, fs)
 }
 
 // printMan writes the command's manual page, rendered from the same description
@@ -289,8 +289,9 @@ func printMan(w io.Writer) {
 // runCLI carries out what the command line asked for and returns the exit
 // status, so a profile started for the run is written before the process exits.
 func runCLI() int {
-	// Usage shown over a misuse goes on the stream the error naming it goes on.
-	flag.Usage = func() { printUsage(flag.CommandLine.Output()) }
+	// A misuse is answered on the error's stream with the synopsis and where the
+	// help is, not the help itself, which would bury the error.
+	flag.Usage = func() { doc().WriteHint(flag.CommandLine.Output()) }
 
 	// The tool manifest is read before the flags, since -engine is checked against its engines.
 	if err := resolveEngines(); err != nil {
@@ -306,7 +307,7 @@ func runCLI() int {
 	// Help that was asked for is the result of the run: it belongs on stdout, where
 	// it can be piped, and the run did what was asked.
 	if showHelp {
-		printUsage(os.Stdout)
+		printUsage(os.Stdout, flag.CommandLine)
 		return exitHolds
 	}
 
diff --git a/cmd/sysml/streams_test.go b/cmd/sysml/streams_test.go
index f74ed09636..410c34c0db 100644
--- a/cmd/sysml/streams_test.go
+++ b/cmd/sysml/streams_test.go
@@ -156,14 +156,14 @@ func TestStreamsAndStatus(t *testing.T) {
 		model:     checkModel,
 		args:      []string{"-h"},
 		status:    exitHolds,
-		stdout:    []string{"Usage: sysml [options] [file...]", "-convert string"},
+		stdout:    []string{"Usage: sysml [options] [file...]", "-convert <format>"},
 		emptyErrs: true,
 	}, {
-		name:     "a flag that is not defined is reported with the usage on stderr",
+		name:     "a flag that is not defined is reported with a pointer to the help on stderr",
 		model:    checkModel,
 		args:     []string{"--nosuchflag"},
 		status:   exitUnevaluable,
-		stderr:   []string{"flag provided but not defined: -nosuchflag", "Usage: sysml [options] [file...]"},
+		stderr:   []string{"flag provided but not defined: -nosuchflag", "Usage: sysml [options] [file...]", "Run 'sysml -help' for the options."},
 		emptyOut: true,
 	}}
 
diff --git a/cmd/sysml/usage.go b/cmd/sysml/usage.go
index 9c88963e9e..a95ae3ff16 100644
--- a/cmd/sysml/usage.go
+++ b/cmd/sysml/usage.go
@@ -24,8 +24,10 @@ func doc() usage.Doc {
 				"otherwise it does what was asked and exits on the verdict, which " +
 				"is what lets a run gate a build.",
 		},
+		Options: optionGroups(),
 		Sections: []usage.Section{{
-			Title: "Examples",
+			Title:         "Examples",
+			BeforeOptions: true,
 			Examples: []usage.Example{
 				usage.Ex("sysml", "Start interactive REPL"),
 				usage.Ex(`sysml -e "5 + 3"`, "Evaluate and exit"),
@@ -56,7 +58,42 @@ func doc() usage.Doc {
 				usage.Ex("sysml -schedule explore -action Drive m.sysml", "Run every linearization; table the outcomes"),
 				usage.Ex("sysml -satisfy -json model.sysml", "Report the verdicts as JSON"),
 			},
-			Paragraphs: []string{"Each check flag may be repeated."},
+			Paragraphs: []string{
+				"Each check flag may be repeated. -validate=<object> checks every " +
+					"assertion about an object -instantiate created and the objects it " +
+					"holds: an object named, #<id>, or a path such as car.engine. " +
+					"-requirement and -satisfy report beside each verdict the verdict of " +
+					"every verification case verifying the requirement. -analysis takes " +
+					"arguments for the case's inputs and an object as its subject, as " +
+					"-analysis \"Pkg::Case(3.0) Pkg::part\"; a verification case also " +
+					"reports the verdict its body produced.",
+			},
+		}, {
+			Title: "Running actions and state machines",
+			Paragraphs: []string{
+				"-action runs an action to completion and -state a state machine, both " +
+					"on one shared clock that -advance runs for the given simulated time " +
+					"units; without -advance a state machine takes only its initial " +
+					"transition. Either names a definition or usage, or one followed by " +
+					"the object to perform it on, as -action \"Drive rover1\".",
+				"-schedule is the policy every run resolves its choice points under — " +
+					"concurrent tokens, overlapping guards, competing transitions: " +
+					"declared, reverse (the default), seed:<n> for a reproducible " +
+					"pseudo-random order, explore[:runs=N,depth=D] to run every " +
+					"linearization within the budget and table the distinct outcomes, " +
+					"or replay:<file> to follow a witness file's choice lines move for " +
+					"move, then reverse.",
+				"Under -schedule explore, -engine check, smt or all, each run creates " +
+					"objects of its own before the behaviors start: one per -instantiate, " +
+					"which a -state or -action named alone attaches to, and one per " +
+					"-action or -state naming a definition or usage to create or a path " +
+					"into one such as mission.rover. The declaration is created once per " +
+					"run, so machines on sibling parts share it and its connectors.",
+				"-jobs is how many runs of one check may go concurrently — the " +
+					"linearizations of an exploration, the engines -engine all consults " +
+					"— each on a worker of its own over the shared model; the result is " +
+					"the same at any count.",
+			},
 		}, {
 			Title: "Analysis engines",
 			Examples: []usage.Example{
@@ -85,6 +122,56 @@ func doc() usage.Doc {
 					"engine reached lowers the strength and is named. Under -json each " +
 					"check carries the plan and one results[] entry per engine that " +
 					"answered, with its engine, claim, strength, bounds and witness.",
+				"-engines lists each engine's name, kind (built-in, tool, engine, policy, " +
+					"sampler), protocol, authority, the questions it answers and whether " +
+					"its process is found, with the manifest entry and resolved command " +
+					"of each external one; -probe also starts each external engine once " +
+					"and checks its describe against its manifest entry field by field. " +
+					"An engine is named run, explore, check, smt, sweep, solve, " +
+					"tool:<name> from OPENSYSML_TOOLS, or as an external engine from " +
+					"OPENSYSML_ENGINES. -engine explore is -schedule explore; -engine " +
+					"check searches every schedule of each -action for a violation, " +
+					"deadlock, failure or divergence; -engine smt decides each " +
+					"-check-property over every schedule and every value of the action's " +
+					"free inputs through an SMT solver.",
+			},
+		}, {
+			Title: "Checking every schedule",
+			Examples: []usage.Example{
+				usage.Ex("sysml -engine check -action Go -check-property Safe m.sysml", "Search every schedule for Safe"),
+				usage.Ex("sysml -engine check -action Go -check-diverge speed m.sysml", "Is speed schedule-dependent?"),
+				usage.Ex("sysml -engine smt -action Go -check-input t -check-property Safe m.sysml", ""),
+				usage.Ex("sysml -engine check -action Go -check-witness out m.sysml", "A witness file per finding"),
+			},
+			Paragraphs: []string{
+				"-check-property evaluates a constraint or requirement at every stable " +
+					"state of the action, on the performing object when there is one, " +
+					"and reports a schedule at which it is false. -check-diverge reports " +
+					"a feature sensitive when schedules leave it with different final " +
+					"values — check searching the schedules, smt asking the solver for " +
+					"two that end it apart — named as x, step.out for a performed node's " +
+					"output or this.level for the performing object's (not covered under " +
+					"smt); a name nothing holds is refused, and without it every " +
+					"attribute of the action and of its performing object is checked, " +
+					"the action's own when it has none.",
+				"Under smt every input the model leaves unbound is free and every bound " +
+					"one is pinned; -check-input leaves a bound feature free in its " +
+					"declared domain, and a name that is not a feature the action reads " +
+					"is refused. -check-assume assumes a constraint or requirement over " +
+					"the initial state; a set no initial state satisfies is reported not " +
+					"covered, never proved.",
+				"-check-witness writes a file for each violation and each divergent " +
+					"value — the inputs the solver chose, the schedule's choices, a blank " +
+					"line, then the run's trace — which -schedule replay:<file> and " +
+					"%replay follow. A bound is named when it is hit: -check-depth is the " +
+					"most moves one schedule may make before the search backtracks, or " +
+					"the moves smt unrolls the action to; -check-states the most distinct " +
+					"states the search may visit, the same figure -engine all gives an " +
+					"exploration as its runs; -check-unroll the most iterations of one " +
+					"loop smt unrolls; -check-timeout the time the plan may run for and " +
+					"the time each solver query may take in place of " +
+					"OPENSYSML_SMT_TIMEOUT — a search it stops is reported incomplete " +
+					"with the states and depth reached, not as a verdict.",
 			},
 		}, {
 			Title: "Sweeping and sampling a parameter",
@@ -162,7 +249,10 @@ func doc() usage.Doc {
 			},
 			Paragraphs: []string{
 				"The input format is taken from the file extension (.sysml, .kerml, " +
-					".ttl) unless -from names it. Converting to the format it is " +
+					".ttl) unless -from names it: sysml, kerml, ttl, turtle, rdf, or " +
+					"xmi, uml or mdzip for a SysML v1 model to migrate, whose " +
+					"element-by-element report -migration-report writes out. " +
+					"Converting to the format it is " +
 					"already in rewrites the input: notation is reformatted, Turtle " +
 					"is normalized.",
 				// Printed rather than restated, so the help cannot drift from what a
@@ -229,6 +319,9 @@ func doc() usage.Doc {
 					"it. Notices — an empty view, an element the rendering cannot " +
 					"represent — go on stderr. Every file named is loaded as one " +
 					"model, so a view may expose elements a sibling file declares. " +
+					"-render-form names the form written — text, mermaid, markdown, dot " +
+					"or plantuml; by default -render takes it from the destination and " +
+					"-render-all writes each kind's machine form. " +
 					"A graph-shaped rendering is written as a Mermaid diagram by " +
 					"default, as Graphviz DOT with -render-form dot and as PlantUML with " +
 					"-render-form plantuml, which also writes a sequence rendering; neither " +
@@ -364,94 +457,249 @@ func solverEnvironment() []usage.Item {
 	}
 }
 
-// registerFlags declares the command's flags on fs, so the help, the man page
-// and a run all read one declaration of each.
+// registerFlags declares the command's flags on fs; each flag's group and
+// placeholder live in optionGroups, and a flag missing there fails the tests.
 func registerFlags(fs *flag.FlagSet) {
 	fs.BoolVar(&showHelp, "help", false, "Show this help and exit")
-	fs.BoolVar(&showHelp, "h", false, "Show this help (shorthand)")
+	fs.BoolVar(&showHelp, "h", false, "Show this help and exit")
+	fs.BoolVar(&showVersion, "version", false, "Show the version and exit")
+	fs.BoolVar(&showVersion, "v", false, "Show the version and exit")
 	fs.BoolVar(&showMan, "man", false, "Write this command's manual page, in roff, to stdout and exit")
-	fs.Var(&evalExprs, "eval", "Evaluate expression and exit (can be specified multiple times)")
-	fs.Var(&evalExprs, "e", "Evaluate expression and exit (shorthand)")
-	fs.BoolVar(&showVersion, "version", false, "Show version information")
-	fs.BoolVar(&showVersion, "v", false, "Show version (shorthand)")
-	fs.BoolVar(&debugMode, "debug", false, "Report every diagnostic over the whole session buffer, with the pass that produced it")
-	fs.BoolVar(&quietMode, "quiet", false, "Report errors only, suppressing warnings")
+
+	fs.Var(&evalExprs, "eval", "Evaluate this expression, against the model when one is loaded, and exit (repeatable)")
+	fs.Var(&evalExprs, "e", "Evaluate this expression, against the model when one is loaded, and exit (repeatable)")
+	fs.StringVar(&queryText, "query", "", "Evaluate this OSLC Query text against the model and exit")
+
+	fs.Var(&modelChecks.validate, "validate", "Report the model's diagnostics and exit, nonzero on an error; -validate=<object> checks instead every assertion about that object (repeatable)")
 	fs.BoolVar(&strictMode, "strict", false, "Judge the model as conforming SysML v2: notation no pinned production admits is an error, not a warning")
-	fs.BoolVar(&traceMode, "trace", false, "Report each execution step: expression evaluation, calc invocation, action tokens, state transitions")
-	fs.Var(&schedule, "schedule", "Scheduling policy every run resolves its choice points under (concurrent tokens, overlapping guards, competing transitions): declared, reverse (default), seed:<n> for a reproducible pseudo-random order, explore[:runs=N,depth=D] to run every linearization within the budget and table the distinct outcomes, or replay:<file> to follow a witness file's choice lines move for move, then reverse")
-	fs.BoolVar(&listEngines, "engines", false, "List the analysis engines this build knows — name, kind (built-in, tool, engine, policy, sampler), protocol, authority, the questions each answers and whether its process is found — with the manifest entry and resolved command of each external one, spawning nothing, and exit")
-	fs.BoolVar(&probeEngines, "probe", false, "With -engines, also start each external engine once, check its describe against its manifest entry field by field and report the outcome as its status")
-	fs.Var(&engine, "engine", "Analysis engine every check is put to: auto (default) picks the strongest engine covering the question, all puts it to every covering engine in name order and composes their answers, or an engine by name (run, explore, check, smt, sweep, solve, tool:<name> from OPENSYSML_TOOLS, or an external engine from OPENSYSML_ENGINES), whose refusal is then the answer; -engine explore is -schedule explore, -engine check searches every schedule of each -action for a violation, deadlock, failure or divergence, and -engine smt decides each -check-property over every schedule and every value of the action's free inputs through an SMT solver")
-	fs.Var(&jobsFlag, "jobs", "Runs of one check that may go concurrently — the linearizations of an exploration, the engines -engine all consults — each on a worker of its own over the shared model; the result is the same at any count. Default OPENSYSML_JOBS, else the number of CPUs")
+	fs.Var(&modelChecks.constraints, "constraint", "Evaluate this constraint and exit (repeatable)")
+	fs.Var(&modelChecks.requirements, "requirement", "Evaluate this requirement, and every verification case verifying it, and exit (repeatable)")
+	fs.Var(&modelChecks.satisfy, "satisfy", "Evaluate every satisfaction assertion, or with -satisfy=<name> those the named element states, and exit (repeatable)")
+	fs.Var(&modelChecks.calcs, "calc", "Invoke this calculation and report its result, as -calc \"Fall(3, 4)\" (repeatable)")
+	fs.Var(&modelChecks.analyses, "analysis", "Run this analysis or verification case and report its outputs and verdict, as -analysis \"Pkg::Case(3.0) Pkg::part\" (repeatable)")
+	fs.Var(&modelChecks.queries, "run-query", "Execute this document query and report its rows, as -run-query \"Heavy root=telescope\" (repeatable)")
+	fs.Var(&modelChecks.instantiate, "instantiate", "Create an object of this definition or usage before the checks, so a verdict is about it (repeatable)")
+	fs.BoolVar(&modelChecks.jsonOut, "json", false, "Report checks as one JSON document rather than as lines")
+
+	fs.Var(&modelChecks.actions, "action", "Run this action to completion, as -action \"Drive rover1\" to run it on an object (repeatable)")
+	fs.Var(&modelChecks.states, "state", "Run this state machine, as -state \"Mission rover1\" to run it on an object (repeatable)")
+	fs.Var(&modelChecks.advance, "advance", "Simulated time units to run the -action and -state behaviors for, on one shared clock; without it a state machine takes only its initial transition")
+	fs.Var(&schedule, "schedule", "Policy every run resolves its choice points under: declared, reverse (default), seed:<n>, explore[:runs=N,depth=D] or replay:<file>")
+	fs.Var(&modelChecks.seed, "seed", "Seed the model's own draws — weighted decisions, random functions — and those of -samples and -runs; the same seed draws the same run or table")
+	fs.Var(&modelChecks.runs, "runs", "Run the -action this many times, each run seeded from -seed, and table the -observe features; needs -seed")
+	fs.Var(&modelChecks.observe, "observe", "Report this feature of the -runs action, or clock for the time it completed at; default every feature it holds and the clock (repeatable)")
+	fs.Var(&modelChecks.sweeps, "sweep", "Run the -analysis or -calc once per value of this range, as -sweep \"n=1..8:2\"; several ranges run their cartesian product (repeatable)")
+	fs.Var(&modelChecks.samples, "samples", "Draw this many values uniformly from each -sweep range instead of stepping through it; needs -seed")
+	fs.Var(&jobsFlag, "jobs", "Runs of one check that may go concurrently, each on a worker of its own; default OPENSYSML_JOBS, else the number of CPUs")
+
+	fs.BoolVar(&listEngines, "engines", false, "List the analysis engines this build knows and their status, spawning nothing, and exit")
+	fs.BoolVar(&probeEngines, "probe", false, "With -engines, also start each external engine once and report the outcome as its status")
+	fs.Var(&engine, "engine", "Analysis engine every check is put to: auto (default), all, or one by name — run, explore, check, smt, sweep, solve, tool:<name> or an external engine")
+
+	fs.Var(&modelChecks.checker.properties, "check-property", "Evaluate this constraint or requirement at every stable state of the action and report a schedule at which it is false (repeatable)")
+	fs.Var(&modelChecks.checker.diverge, "check-diverge", "Report this feature sensitive when schedules leave it with different final values, as x, step.out or this.level; default every attribute (repeatable)")
+	fs.Var(&modelChecks.checker.inputs, "check-input", "Under smt, leave this feature of the action free in its declared domain although the model binds it (repeatable)")
+	fs.Var(&modelChecks.checker.assume, "check-assume", "Under smt, assume this constraint or requirement over the initial state of the action (repeatable)")
+	fs.StringVar(&modelChecks.checker.witness, "check-witness", "", "Write a witness file for each violation and each divergent value to this directory, for -schedule replay:<file> and %replay to follow")
+	modelChecks.checker.depth.flag, modelChecks.checker.states.flag, modelChecks.checker.unroll.flag = "check-depth", "check-states", "check-unroll"
+	fs.Var(&modelChecks.checker.depth, "check-depth", "The most moves one schedule may make before the search backtracks, or the moves smt unrolls the action to (default 10000 for check, 40 for smt)")
+	fs.Var(&modelChecks.checker.states, "check-states", "Under check, the most distinct states the search may visit (default 1000000)")
+	fs.Var(&modelChecks.checker.unroll, "check-unroll", "Under smt, the most iterations of one loop the solver unrolls before it stops (default 4)")
+	fs.Var(&modelChecks.checker.timeout, "check-timeout", "The time the check's plan may run for, as 30s or 2m, and the time each smt solver query may take in place of OPENSYSML_SMT_TIMEOUT")
+
 	fs.StringVar(&convertFormat, "convert", "", "Convert the model to this format instead of running it: sysml, kerml, ttl, turtle or rdf (RDF is experimental)")
-	fs.StringVar(&queryText, "query", "", "Evaluate OSLC Query text against the model instead of running the REPL")
-	fs.StringVar(&outputPath, "output", "", "Write conversion output to this file (default: stdout)")
-	fs.StringVar(&outputPath, "o", "", "Write conversion output to this file (shorthand)")
-	fs.StringVar(&fromFormat, "from", "", "Input format for -convert: sysml, kerml, ttl, turtle, rdf, or xmi/uml/mdzip for a SysML v1 model to migrate (experimental; default: from the input's extension)")
-	fs.StringVar(&migrationReport, "migration-report", "", "With -convert from xmi: write the element-by-element migration report to this file (JSON when it ends in .json, text otherwise)")
-	fs.StringVar(&renderView, "render", "", "Render this view of the model (every file named, loaded as one) instead of running it, in the form its render member states")
+	fs.StringVar(&fromFormat, "from", "", "Input format for -convert: sysml, kerml, ttl, turtle, rdf, or xmi, uml or mdzip for a SysML v1 model to migrate (experimental); default the input's extension")
+	fs.StringVar(&outputPath, "output", "", "Write what -convert, -compile, -render or -render-document produces to this file instead of stdout")
+	fs.StringVar(&outputPath, "o", "", "Write what -convert, -compile, -render or -render-document produces to this file instead of stdout")
+	fs.StringVar(&migrationReport, "migration-report", "", "With -convert from xmi, write the element-by-element migration report to this file: JSON when it ends in .json, text otherwise")
+
+	fs.StringVar(&compileCalc, "compile", "", "Compile this calc def to a native executable named by -o, as -compile Pkg::Fib")
+	fs.StringVar(&compileTarget, "target", "c", "Backend -compile generates code for: c or go")
+	fs.BoolVar(&compileSource, "source", false, "With -compile, write the generated source to -o instead of building it")
+
+	fs.StringVar(&renderView, "render", "", "Render this view of the model instead of running it, in the form its render member states")
 	fs.StringVar(&renderAllDir, "render-all", "", "Render every declared view into this directory")
-	fs.StringVar(&renderDoc, "render-document", "", "Compile this document definition, run its queries and write the rendered Markdown")
-	fs.StringVar(&renderDocsDir, "render-documents", "", "Render every document definition as linked Markdown into this directory")
-	fs.StringVar(&renderForm, "render-form", "", "Form -render or -render-all writes: text, mermaid, markdown, dot or plantuml (default: destination-dependent for -render, each kind's machine form for -render-all)")
-	fs.StringVar(&renderPalette, "render-palette", "", "Palette the DOT or PlantUML form of -render or -render-all fills nodes from, by keyword family: okabe-ito, tol-bright, tol-muted, tol-light, brewer-set2, brewer-dark2, viridis or cividis (default: black and white)")
-	fs.StringVar(&docForm, "doc-form", "", "Form -render-document and -render-documents write: markdown (default), html or pdf, which drives an external converter")
-	fs.StringVar(&diagramForm, "diagram-form", "", "Form the graph-shaped diagrams of -render-document and -render-documents are written in: mermaid (default), dot or plantuml; a table-kind view is a table either way")
+	fs.StringVar(&renderForm, "render-form", "", "Form -render or -render-all writes: text, mermaid, markdown, dot or plantuml; default from the destination for -render, each kind's machine form for -render-all")
+	fs.StringVar(&renderPalette, "render-palette", "", "Palette the dot or plantuml form fills nodes from, by keyword family: okabe-ito, tol-bright, tol-muted, tol-light, brewer-set2, brewer-dark2, viridis or cividis; default black and white")
+
+	fs.StringVar(&renderDoc, "render-document", "", "Compile this document definition, run its queries and write the rendered document")
+	fs.StringVar(&renderDocsDir, "render-documents", "", "Render every document definition, linked to one another, into this directory")
+	fs.StringVar(&docForm, "doc-form", "", "Form the documents are written in: markdown (default), html or pdf, which drives an external converter")
+	fs.StringVar(&diagramForm, "diagram-form", "", "Form the documents' graph-shaped diagrams are written in: mermaid (default), dot or plantuml; a table-kind view is a table either way")
+	fs.BoolVar(&pdfTitlePage, "doc-title-page", false, "Put the document title on a page of its own (html or pdf)")
+	fs.BoolVar(&pdfTOC, "doc-toc", false, "Write a table of contents ahead of the content (html or pdf)")
+	fs.BoolVar(&pdfNumbering, "doc-number-sections", false, "Number the section headings hierarchically (html or pdf)")
 	fs.StringVar(&pdfEngine, "pdf-engine", "", "Converter -doc-form pdf drives: weasyprint (default), pandoc or prince")
-	fs.BoolVar(&pdfTitlePage, "pdf-title-page", false, "Put the document title on a page of its own (-doc-form pdf)")
-	fs.BoolVar(&pdfTOC, "pdf-toc", false, "Write a table of contents ahead of the content (-doc-form pdf)")
-	fs.BoolVar(&pdfNumbering, "pdf-number-sections", false, "Number the section headings hierarchically (-doc-form pdf)")
-	fs.BoolVar(&pdfTitlePage, "doc-title-page", false, "Put the document title on a page of its own (-doc-form html or pdf)")
-	fs.BoolVar(&pdfTOC, "doc-toc", false, "Write a table of contents ahead of the content (-doc-form html or pdf)")
-	fs.BoolVar(&pdfNumbering, "doc-number-sections", false, "Number the section headings hierarchically (-doc-form html or pdf)")
-	fs.Var(&htmlCSS, "html-css", "Style the HTML with this stylesheet: a file is inlined, a URL is linked (repeatable, applied in order after the default sheet)")
-	fs.StringVar(&htmlTheme, "html-theme", "", "Style the HTML page with a bundled theme layered over the default stylesheet: default, modern, print or report (default: the default stylesheet alone)")
+
+	fs.StringVar(&htmlTheme, "html-theme", "", "Style the page with a bundled theme layered over the default stylesheet: default, modern, print or report")
+	fs.Var(&htmlCSS, "html-css", "Style the page with this stylesheet too: a file is inlined, a URL is linked (repeatable, applied in order after the default sheet)")
 	fs.BoolVar(&htmlNoCSS, "html-no-default-css", false, "Leave the default stylesheet out, so only -html-css sheets style the document")
-	fs.BoolVar(&htmlShowCSS, "html-default-css", false, "Write the default document stylesheet and exit, as a starting point for your own")
 	fs.BoolVar(&htmlFragment, "html-fragment", false, "Write the document element alone, without the page shell or a stylesheet, to embed in a page of your own")
-	fs.StringVar(&htmlMermaid, "html-mermaid", "", "Have the HTML page load Mermaid to draw its diagrams: cdn loads a pinned release from jsDelivr, a URL loads the script it names (default: diagrams stay Mermaid source)")
-	fs.StringVar(&htmlMath, "html-math", "", "Have the HTML page load MathJax to typeset its formulas: cdn loads a pinned release from jsDelivr, a URL loads the script it names (default: formulas stay LaTeX source)")
-	fs.StringVar(&syncDiffWith, "sync-diff", "", "Show the change set between the model and this repository — a graph file (.ttl) or a SysML v2 API endpoint URL — keyed by effective element id, instead of running it; never writes")
-	fs.StringVar(&syncApplyTo, "sync-apply", "", "Apply the change set to the model's project branch at this SysML v2 API endpoint URL, then record the commit in the sync state (token from "+flexo.EnvToken+")")
+	fs.BoolVar(&htmlShowCSS, "html-default-css", false, "Write the default document stylesheet, or with -html-theme that theme's whole sheet, and exit")
+	fs.StringVar(&htmlMermaid, "html-mermaid", "", "Have the page load Mermaid to draw its diagrams: cdn loads a pinned release from jsDelivr, a URL the script it names")
+	fs.StringVar(&htmlMath, "html-math", "", "Have the page load MathJax to typeset its formulas: cdn loads a pinned release from jsDelivr, a URL the script it names")
+
+	fs.StringVar(&syncDiffWith, "sync-diff", "", "Show the change set between the model and this repository — a graph file (.ttl) or a SysML v2 API endpoint URL — and exit; never writes")
+	fs.StringVar(&syncApplyTo, "sync-apply", "", "Apply the change set to the model's project branch at this SysML v2 API endpoint URL, then record the commit in the sync state")
 	fs.StringVar(&syncBase, "sync-base", "", "Repository graph at the last-seen commit; with it, repository changes since then surface as conflicts")
-	fs.StringVar(&syncState, "sync-state", "", "Sync state file recording project, branch and last-seen commit (default: <model>.sync.json beside the model)")
+	fs.StringVar(&syncState, "sync-state", "", "Sync state file recording project, branch and last-seen commit; default <model>.sync.json beside the model")
 	fs.BoolVar(&syncConfirmDeletes, "sync-confirm-deletes", false, "Confirm repository-side deletes; without it the diff reports them but applying is refused")
 	fs.BoolVar(&syncMintIDs, "sync-mint-ids", false, "Mint a UUID for each unannotated element being created, so the repository can address it stably")
 	fs.StringVar(&syncAnnotate, "sync-annotate", "", "Write the model to this file with each minted id declared as an @ElementId annotation (needs -sync-mint-ids)")
-	fs.Var(&deprecatedFlag{instead: "-to has been replaced by -convert, as `sysml model.sysml -convert ttl`"}, "to", "Replaced by -convert, which names the output format")
-	fs.Var(&modelChecks.instantiate, "instantiate", "Create an object of this definition or usage before the checks, so a verdict is about it; under -schedule explore, -engine check, smt or all, each run creates an object of it of its own before the behaviors start, one per -instantiate, which a -state or -action named alone attaches to and a path such as mission.vehicle walks into (repeatable)")
-	fs.Var(&modelChecks.constraints, "constraint", "Evaluate this constraint and exit (repeatable)")
-	fs.Var(&modelChecks.requirements, "requirement", "Evaluate this requirement and exit, reporting beside its verdict the verdict of every verification case verifying it (repeatable)")
-	fs.Var(&modelChecks.satisfy, "satisfy", "Evaluate every satisfaction assertion, or with -satisfy=<name> those the named element states, reporting beside each verdict the verdict of every verification case verifying the requirement (repeatable)")
-	fs.Var(&modelChecks.validate, "validate", "Analyse the model and report its diagnostics, exiting nonzero on an error; with -validate=<object> check instead every assertion about an object -instantiate created and the objects it holds, an object named, #<id>, or a path such as car.engine (repeatable)")
-	fs.Var(&modelChecks.calcs, "calc", "Invoke this calculation and report what it computed, as -calc \"Fall(3, 4)\" (repeatable)")
-	fs.Var(&modelChecks.analyses, "analysis", "Run this analysis or verification case and report its outputs and the verdict of its objective, as -analysis \"Pkg::Case(3.0) Pkg::part\" with arguments for its inputs and an object as its subject; a verification case also reports the verdict its body produced (repeatable)")
-	fs.Var(&modelChecks.sweeps, "sweep", "Run the named -analysis or -calc once per value of this range, as -sweep \"speed=0.0 [SI::'m/s']..10.0 [SI::'m/s']:2.0 [SI::'m/s']\"; the values are produced in the parameter's declared type; several ranges run their cartesian product (repeatable)")
-	fs.Var(&modelChecks.samples, "samples", "Draw this many values uniformly from each -sweep range instead of stepping through them, Integers or reals as the parameter is typed; needs -seed")
-	fs.Var(&modelChecks.seed, "seed", "Seed the model's own draws — Probability-weighted decisions, RandomFunctions — come from in every run made, whatever -schedule, and the seed -samples or -runs draws from; the same seed draws the same run or table")
-	fs.Var(&modelChecks.runs, "runs", "Run the -action this many times, each run's modeled randomness (weighted decisions, random functions) seeded from -seed, and report the table of the -observe features with each one's distribution; needs -seed")
-	fs.Var(&modelChecks.observe, "observe", "Report this feature of the -runs action, or `clock` for the time it completed at; default every feature it holds and the clock (repeatable)")
-	fs.Var(&modelChecks.queries, "run-query", "Execute this document query and report its rows, as -run-query \"HeavySubsystems root=telescope\" (repeatable)")
-	fs.Var(&modelChecks.actions, "action", "Run this action to completion, as -action \"Drive rover1\" to run it on an object; under -schedule explore each run performs it on an object of its own, named as a definition or usage to create, a path into one such as mission.rover, or, named alone, the run's one -instantiate object performing it (repeatable)")
-	fs.Var(&modelChecks.states, "state", "Run this state machine, as -state \"Mission rover1\" to run it on an object; under -schedule explore each run creates the object of its own, named as a definition or usage to create or a path such as mission.rover into one — the declaration is created once per run, so machines on sibling parts share it and its connectors — or, named alone, the run's one -instantiate object exhibiting it (repeatable)")
-	fs.Var(&modelChecks.advance, "advance", "Simulated time units to run the -action and -state behaviors for, on one shared clock (default: a state machine takes only its initial transition; an action runs to completion)")
-	fs.Var(&modelChecks.checker.diverge, "check-diverge", "With -engine check, -engine smt or -engine all: report this feature sensitive when schedules leave it with different final values — check searching the schedules, smt asking the solver for two that end it apart — as -check-diverge x, -check-diverge step.out for a performed node's output or -check-diverge this.level for the performing object's (not covered under smt), a name nothing holds refused; default every attribute of the action and of its performing object, the action's own when it has none (repeatable)")
-	fs.Var(&modelChecks.checker.properties, "check-property", "With -engine check or -engine all: evaluate this constraint or requirement at every stable state of the action, on the performing object when there is one, and report a schedule at which it is false (repeatable)")
-	fs.Var(&modelChecks.checker.inputs, "check-input", "With -engine smt or -engine all: leave this feature of the action free in its declared domain although the model binds it, as -check-input inletTemp; a name that is not a feature the action reads is refused. Without it, every input the model leaves unbound is free and every bound one is pinned (repeatable)")
-	fs.Var(&modelChecks.checker.assume, "check-assume", "With -engine smt or -engine all: assume this constraint or requirement over the initial state of the action, as -check-assume Plant::EnvelopeLimits; a set no initial state satisfies is reported not covered, never proved (repeatable)")
-	fs.StringVar(&modelChecks.checker.witness, "check-witness", "", "With -engine check, -engine smt or -engine all: write a witness file to this directory for each violation and each divergent value — the inputs the solver chose, the schedule's choices, a blank line, then the run's trace — which -schedule replay:<file> and %replay follow")
-	modelChecks.checker.depth.flag, modelChecks.checker.states.flag, modelChecks.checker.unroll.flag = "check-depth", "check-states", "check-unroll"
-	fs.Var(&modelChecks.checker.depth, "check-depth", "With -engine check, -engine smt or -engine all: the most moves one schedule may make before the search backtracks, or the moves the smt engine unrolls the action to, named as the depth bound hit (default 10000 for check, 40 for smt)")
-	fs.Var(&modelChecks.checker.states, "check-states", "With -engine check or -engine all: the most distinct states the search may visit, named as the states bound hit; the same figure -engine all gives an exploration as its runs (default 1000000)")
-	fs.Var(&modelChecks.checker.unroll, "check-unroll", "With -engine smt or -engine all: the most iterations of one loop the smt engine unrolls before it stops, named as the unroll bound hit (default 4)")
-	fs.Var(&modelChecks.checker.timeout, "check-timeout", "With -engine check, -engine smt or -engine all: the time the check's plan may run for, as 30s or 2m, and the time each of the smt engine's solver queries may take in place of OPENSYSML_SMT_TIMEOUT; a search it stops is reported incomplete with the states and depth reached, not as a verdict")
-	fs.BoolVar(&modelChecks.jsonOut, "json", false, "Report checks as one JSON document rather than as lines")
-	fs.StringVar(&compileCalc, "compile", "", "Compile this calc def to a native executable named by -o, as -compile Pkg::Fib")
-	fs.StringVar(&compileTarget, "target", "c", "Backend -compile generates code for: c (default) or go")
-	fs.BoolVar(&compileSource, "source", false, "With -compile, write the generated source to -o instead of building it")
+
+	fs.BoolVar(&debugMode, "debug", false, "Report every diagnostic over the whole session buffer, with the pass that produced it")
+	fs.BoolVar(&quietMode, "quiet", false, "Report errors only, suppressing warnings")
+	fs.BoolVar(&traceMode, "trace", false, "Report each execution step: expression evaluation, calc invocation, action tokens, state transitions")
 	fs.StringVar(&cpuProfilePath, "cpuprofile", "", "Write a CPU profile of the run to this file, for go tool pprof")
 	fs.StringVar(&memProfilePath, "memprofile", "", "Write a heap profile of the run to this file, for go tool pprof")
 	fs.BoolVar(&memStats, "memstats", false, "Report on stderr what the run cost: wall time, memory allocated, memory taken from the OS")
+
+	fs.Var(&deprecatedFlag{instead: "-to has been replaced by -convert, as `sysml model.sysml -convert ttl`"}, "to", "Replaced by -convert, which names the output format")
+	fs.BoolVar(&pdfTitlePage, "pdf-title-page", false, "Former name of -doc-title-page, which also shapes HTML")
+	fs.BoolVar(&pdfTOC, "pdf-toc", false, "Former name of -doc-toc, which also shapes HTML")
+	fs.BoolVar(&pdfNumbering, "pdf-number-sections", false, "Former name of -doc-number-sections, which also shapes HTML")
+}
+
+// optionGroups lays the flags out by task, each with the placeholder its
+// argument is shown as, in the order the help and the man page list them.
+func optionGroups() []usage.OptionGroup {
+	return []usage.OptionGroup{{
+		Title: "General",
+		Options: []usage.Option{
+			usage.Opt("help", "", "h"),
+			usage.Opt("version", "", "v"),
+			usage.Opt("man", ""),
+		},
+	}, {
+		Title: "Evaluating",
+		Options: []usage.Option{
+			usage.Opt("eval", "<expr>", "e"),
+			usage.Opt("query", "<text>"),
+		},
+	}, {
+		Title: "Checking a model",
+		Options: []usage.Option{
+			usage.Opt("validate", "[=<object>]"),
+			usage.Opt("strict", ""),
+			usage.Opt("constraint", "<name>"),
+			usage.Opt("requirement", "<name>"),
+			usage.Opt("satisfy", "[=<name>]"),
+			usage.Opt("calc", "<call>"),
+			usage.Opt("analysis", "<call>"),
+			usage.Opt("run-query", "<query>"),
+			usage.Opt("instantiate", "<name>"),
+			usage.Opt("json", ""),
+		},
+	}, {
+		Title: "Running behaviors",
+		Options: []usage.Option{
+			usage.Opt("action", "<name>"),
+			usage.Opt("state", "<name>"),
+			usage.Opt("advance", "<time>"),
+			usage.Opt("schedule", "<policy>"),
+			usage.Opt("seed", "<n>"),
+			usage.Opt("runs", "<n>"),
+			usage.Opt("observe", "<feature>"),
+			usage.Opt("sweep", "<range>"),
+			usage.Opt("samples", "<n>"),
+			usage.Opt("jobs", "<n>"),
+		},
+	}, {
+		Title: "Analysis engines",
+		Options: []usage.Option{
+			usage.Opt("engines", ""),
+			usage.Opt("probe", ""),
+			usage.Opt("engine", "<name>"),
+		},
+	}, {
+		Title: "Checking every schedule (-engine check, smt or all)",
+		Options: []usage.Option{
+			usage.Opt("check-property", "<name>"),
+			usage.Opt("check-diverge", "<feature>"),
+			usage.Opt("check-input", "<feature>"),
+			usage.Opt("check-assume", "<name>"),
+			usage.Opt("check-witness", "<dir>"),
+			usage.Opt("check-depth", "<n>"),
+			usage.Opt("check-states", "<n>"),
+			usage.Opt("check-unroll", "<n>"),
+			usage.Opt("check-timeout", "<duration>"),
+		},
+	}, {
+		Title: "Converting and migrating",
+		Options: []usage.Option{
+			usage.Opt("convert", "<format>"),
+			usage.Opt("from", "<format>"),
+			usage.Opt("output", "<file>", "o"),
+			usage.Opt("migration-report", "<file>"),
+		},
+	}, {
+		Title: "Compiling natively",
+		Options: []usage.Option{
+			usage.Opt("compile", "<calc>"),
+			usage.Opt("target", "<backend>"),
+			usage.Opt("source", ""),
+		},
+	}, {
+		Title: "Rendering views",
+		Options: []usage.Option{
+			usage.Opt("render", "<view>"),
+			usage.Opt("render-all", "<dir>"),
+			usage.Opt("render-form", "<form>"),
+			usage.Opt("render-palette", "<palette>"),
+		},
+	}, {
+		Title: "Rendering documents",
+		Options: []usage.Option{
+			usage.Opt("render-document", "<name>"),
+			usage.Opt("render-documents", "<dir>"),
+			usage.Opt("doc-form", "<form>"),
+			usage.Opt("diagram-form", "<form>"),
+			usage.Opt("doc-title-page", ""),
+			usage.Opt("doc-toc", ""),
+			usage.Opt("doc-number-sections", ""),
+			usage.Opt("pdf-engine", "<converter>"),
+		},
+	}, {
+		Title: "Styling HTML documents",
+		Options: []usage.Option{
+			usage.Opt("html-theme", "<theme>"),
+			usage.Opt("html-css", "<file|url>"),
+			usage.Opt("html-no-default-css", ""),
+			usage.Opt("html-fragment", ""),
+			usage.Opt("html-default-css", ""),
+			usage.Opt("html-mermaid", "cdn|<url>"),
+			usage.Opt("html-math", "cdn|<url>"),
+		},
+	}, {
+		Title: "Syncing against a repository",
+		Options: []usage.Option{
+			usage.Opt("sync-diff", "<repo>"),
+			usage.Opt("sync-apply", "<url>"),
+			usage.Opt("sync-base", "<file>"),
+			usage.Opt("sync-state", "<file>"),
+			usage.Opt("sync-confirm-deletes", ""),
+			usage.Opt("sync-mint-ids", ""),
+			usage.Opt("sync-annotate", "<file>"),
+		},
+	}, {
+		Title: "Diagnostics and profiling",
+		Options: []usage.Option{
+			usage.Opt("debug", ""),
+			usage.Opt("quiet", ""),
+			usage.Opt("trace", ""),
+			usage.Opt("cpuprofile", "<file>"),
+			usage.Opt("memprofile", "<file>"),
+			usage.Opt("memstats", ""),
+		},
+	}, {
+		Title: "Deprecated",
+		Options: []usage.Option{
+			usage.Opt("to", "<format>"),
+			usage.Opt("pdf-title-page", ""),
+			usage.Opt("pdf-toc", ""),
+			usage.Opt("pdf-number-sections", ""),
+		},
+	}}
 }
 
 // docFlags is a flag set holding the command's flags, for rendering the help or
diff --git a/cmd/sysml/usage_test.go b/cmd/sysml/usage_test.go
index 2e68a1062e..b01325360b 100644
--- a/cmd/sysml/usage_test.go
+++ b/cmd/sysml/usage_test.go
@@ -12,7 +12,7 @@ import (
 // reports, wrapped rather than reworded.
 func TestPrintUsageStatesTheExperimentalNotice(t *testing.T) {
 	var help bytes.Buffer
-	printUsage(&help)
+	printUsage(&help, docFlags())
 
 	unwrapped := strings.Join(strings.Fields(help.String()), " ")
 	if !strings.Contains(unwrapped, convert.ExperimentalNotice) {
@@ -24,3 +24,11 @@ func TestPrintUsageStatesTheExperimentalNotice(t *testing.T) {
 		}
 	}
 }
+
+// Every flag is listed under exactly one heading, so a flag added without a
+// place in the help is caught here rather than by a reader who cannot find it.
+func TestEveryFlagIsInOneOptionGroup(t *testing.T) {
+	if err := doc().CheckOptions(docFlags()); err != nil {
+		t.Error(err)
+	}
+}
diff --git a/docs/reference/cli.md b/docs/reference/cli.md
index 7fd69fb780..acbb9b5bcc 100644
--- a/docs/reference/cli.md
+++ b/docs/reference/cli.md
@@ -235,9 +235,9 @@ reported, so a script that reads it takes the output from the first `{`.
 | `--html-mermaid <cdn\|url>` | | Have the HTML page load Mermaid to draw its diagrams: `cdn` loads a pinned release from jsDelivr, a URL loads the script it names (default: diagrams stay Mermaid source) |
 | `--html-math <cdn\|url>` | | Have the HTML page load MathJax to typeset its formulas: `cdn` loads a pinned release from jsDelivr, a URL loads the script it names (default: formulas stay LaTeX source) |
 | `--pdf-engine <engine>` | | Converter `--doc-form pdf` drives: `weasyprint` (default), `pandoc` or `prince` |
-| `--pdf-title-page` | | Alias of `--doc-title-page` |
-| `--pdf-toc` | | Alias of `--doc-toc` |
-| `--pdf-number-sections` | | Alias of `--doc-number-sections` |
+| `--pdf-title-page` | | Former name of `--doc-title-page` |
+| `--pdf-toc` | | Former name of `--doc-toc` |
+| `--pdf-number-sections` | | Former name of `--doc-number-sections` |
 | `--output <file>` | `-o` | Write the conversion, the rendering or the rendered document to a file instead of stdout |
 | `--version` | `-v` | Show version information |
 | `--help` | `-h` | Show usage information |
diff --git a/internal/frontend/repl/meta.go b/internal/frontend/repl/meta.go
index e31240969b..18aec7ffb9 100644
--- a/internal/frontend/repl/meta.go
+++ b/internal/frontend/repl/meta.go
@@ -14,6 +14,7 @@ import (
 	"github.com/Open-MBEE/OpenSysML/internal/exec/analysis"
 	"github.com/Open-MBEE/OpenSysML/internal/exec/objref"
 	"github.com/Open-MBEE/OpenSysML/internal/exec/runtime"
+	"github.com/Open-MBEE/OpenSysML/internal/frontend/usage"
 	"github.com/Open-MBEE/OpenSysML/internal/ir/lower"
 	"github.com/Open-MBEE/OpenSysML/internal/ir/view"
 	"github.com/Open-MBEE/OpenSysML/internal/semantic/resolve"
@@ -130,6 +131,10 @@ const (
 	argName           = "<name>"
 	timeLabel         = "  Time: "
 
+	groupSession    = "Session:"
+	groupSettings   = "Settings:"
+	groupEngines    = "Analysis engines:"
+	groupChecks     = "Checking every schedule:"
 	groupLibrary    = "Library discovery:"
 	groupRuntime    = "Runtime commands:"
 	groupBehavioral = "Behavioral commands:"
@@ -148,94 +153,120 @@ type metaCommand struct {
 }
 
 var metaCommandTable = []metaCommand{
-	{name: "%help", desc: "show this help"},
-	{name: "%list", desc: "list current session declarations"},
-	{name: "%clear", desc: "reset the session"},
-	{name: "%load", args: "<path>...", desc: "submit the contents of files, directories or globs"},
-	{name: "%print", args: "[name]", desc: "print the session model as SysML notation, or just the named element"},
-	{name: "%save", args: "<file>", desc: "write the session model to a file (.sysml notation, or .ttl RDF — experimental)"},
-	{name: cmdQuery, args: "<oslc-query>", desc: "identify model elements using OSLC Query text"},
-	{name: "%verbosity", args: "[level]", desc: "show or set output level: quiet, normal or debug"},
-	{name: "%trace", args: "[on|off]", desc: "show or set execution tracing (evaluation, calc, action and state steps)"},
-	{name: "%strict", args: "[on|off]", desc: "show or set strict conformance: report notation no SysML v2 production admits as an error"},
-	{name: "%schedule", args: "[<policy>]", desc: "show or set the scheduling policy runs started from here on resolve choice points under: declared, reverse or seed:<n>"},
-	{name: "%seed", args: "[<n>|off]", desc: "show or set the seed runs started from here on draw their modeled randomness from — Probability-weighted decisions, RandomFunctions — whatever the schedule; off leaves it to the schedule's seed:<n>"},
-	{name: "%budget", desc: "show the bounds one run may spend, and the variable raising each"},
-	{name: "%jobs", args: "[<n>]", desc: "show or set how many runs of one check go concurrently: an exploration's linearizations, the engines all consults"},
-	{name: "%engines", args: "[probe]", desc: "list the analysis engines, with the kind, protocol and authority of each, the questions it answers and whether it can run; probe also starts each external engine once and checks it against its manifest"},
-	{name: "%engine", args: "[<name>|auto|all]", desc: "show or set the engine questions asked from here on are put to: one by name, auto for the strongest covering one, or all for every covering one"},
-	{name: "%check-diverge", args: "[<feature>...|off]", desc: "show or set the features the check engine compares final values of across schedules; off compares every attribute of the action and of its performing object, or of the action alone when it has none"},
-	{name: "%check-property", args: "[<name>...|off]", desc: "show or set the constraints and requirements the check engine evaluates at every stable state of an action"},
-	{name: "%check-input", args: "[<feature>...|off]", desc: "show or set the features the smt engine leaves free in their declared domains although the model binds them; off frees only the inputs the model leaves unbound"},
-	{name: "%check-assume", args: "[<name>...|off]", desc: "show or set the constraints and requirements the smt engine assumes over the initial state of an action"},
-	{name: "%check-witness", args: "[<dir>|off]", desc: "show or set the directory the check and smt engines write a witness to for each violation and divergent value"},
-	{name: "%check-bounds", args: "[depth=<n>] [states=<n>] [unroll=<n>] [timeout=<duration>] | off", desc: "show or set the bounds the check and smt engines search within: the moves of one schedule, the distinct states, the iterations of a loop the smt engine unrolls, and the clock; off restores their defaults"},
-	{name: "%replay", args: "<witness>", desc: "install the schedule a witness file fixes, so the next %action or %state steps the run it records"},
-	{name: "%quit", desc: "exit the REPL"},
-	{name: "%exit", desc: "exit the REPL", alias: true},
-
-	{group: groupLibrary, name: "%search", args: "<substring>", desc: "list the declared and library symbols whose qualified name contains <substring>"},
-	{group: groupLibrary, name: "%builtins", desc: "list the library functions this build implements directly"},
-	{group: groupLibrary, name: "%view", args: argName, desc: "show what a view exposes, and the views nested in it"},
-	{group: groupLibrary, name: "%render", args: "<name> [form [palette]]", desc: "render a view as the rendering it states — as text, as a Mermaid diagram or a Markdown table, or as Graphviz DOT or PlantUML, filled from a named palette"},
-
-	{group: groupRuntime, name: "%instantiate", args: argName, desc: "create an instance of a part def"},
-	{group: groupRuntime, name: "%eval", args: "[in <name>|<path>|#<id> :] <expr>", desc: "evaluate an expression, in the named element or object when one is named"},
-	{group: groupRuntime, name: "%features", args: "<object> [all|depth <n>] [json]", desc: "show an object's feature values and what its behaviors are doing, bounded unless all or a depth is asked for; json writes the object graph as the API does; an object is named, #<id>, or a path such as car.fl or #1.wheels[2]"},
-	{group: groupRuntime, name: "%instances", desc: "list all instantiated objects"},
-	{group: groupRuntime, name: "%invoke", args: "<object> <op> [<p>=<expr>]", desc: "invoke an operation of an object's type, performed by that object; an object is named, #<id>, or a path such as car.fl"},
-
-	{group: groupBehavioral, name: "%calc", args: "<name> <args>", desc: "invoke a calculation with arguments"},
-	{group: groupBehavioral, name: cmdAnalysis, args: "<name>[(<args>)] [<object>]", desc: "run an analysis case and report its outputs and the verdict of its objective; arguments bind its inputs and an object is its subject"},
-	{group: groupBehavioral, name: cmdSweep, args: "<name>[(<args>)] [<object>] <p>=<from>..<to>[:<step>]...", desc: "run an analysis case or calc once per value of each range, one run per row of the cartesian product, and print the table"},
-	{group: groupBehavioral, name: cmdSamples, args: "<n> <seed> <name>[(<args>)] [<object>] <p>=<from>..<to>...", desc: "run an analysis case or calc over <n> values drawn uniformly from each range with the given seed, and print the table"},
-	{group: groupBehavioral, name: cmdRuns, args: "<n> <seed> <action> [<observable>...]", desc: "run an action <n> times, each run's modeled randomness seeded from the given seed, and print the table of the observables with each one's distribution"},
-	{group: groupBehavioral, name: cmdRunQuery, args: "<name> [<p>=<expr>...]", desc: "execute a document query and print its rows, with each binding written as <parameter>=<expression>"},
-	{group: groupBehavioral, name: cmdRenderDocument, args: "<name> [mermaid|dot|plantuml]", desc: "compile a document definition, run its queries and print the rendered Markdown, its graph-shaped diagrams as Mermaid, Graphviz DOT or PlantUML"},
-	{group: groupBehavioral, name: "%constraint", args: argName, desc: "evaluate a constraint definition"},
-	{group: groupBehavioral, name: "%requirement", args: argName, desc: "evaluate a requirement definition"},
-	{group: groupBehavioral, name: "%satisfy", args: "[name]", desc: "evaluate the satisfaction assertions of the model, or of one element"},
-	{group: groupBehavioral, name: "%validate", args: "<object>", desc: "check every assertion about an object and the objects it holds: the asserted constraints of their types, the requirements they carry and the satisfactions they are subject of; an object is named, #<id>, or a path such as car.engine"},
-	{group: groupBehavioral, name: "%check", args: argName, desc: "ask an SMT solver whether a constraint, requirement or satisfaction can be satisfied (experimental)"},
-	{group: groupBehavioral, name: "%explain", args: argName, desc: "ask an SMT solver which conditions of an unsatisfiable element conflict (experimental)"},
-	{group: groupBehavioral, name: "%solve", args: argName, desc: "ask an SMT solver for values satisfying an element, keeping what is already fixed (experimental)"},
-	{group: groupBehavioral, name: "%configure", args: "<name> [<variation>=<variant>...] [all [<count>]]", desc: "ask an SMT solver which variants an element's conditions permit (experimental)"},
-	{group: groupBehavioral, name: "%optimize", args: argName, desc: "ask an SMT solver for the best values an analysis case's objectives admit (experimental)"},
-
-	{group: groupAction, name: "%action", args: "<name> [<object>]", desc: "start action executor debugging session, performed by an object"},
-	{group: groupAction, name: "%step", desc: "advance one token step, or one step of the state machine being debugged"},
-	{group: groupAction, name: "%continue", desc: "run action to completion"},
-	{group: groupAction, name: "%tokens", desc: "show active tokens"},
-	{group: groupAction, name: "%break", args: "<node>", desc: "set breakpoint at node"},
-	{group: groupAction, name: "%stop", desc: "stop current debugging session"},
-
-	{group: groupState, name: "%state", args: "<name> [<object>]", desc: "debug the machine an object exhibits (naming that machine alone attaches to the one object exhibiting it; with none or several, name the object), or a state machine performed by an object; an object is named, #<id>, or a path such as car.fl"},
-	{group: groupState, name: "%send", args: "<signal>[(<p>=<expr>, ...)] [to <object>]", desc: "send a signal to an object's machine, by default the one being debugged; an object is named, #<id>, or a path such as car.fl"},
-	{group: groupState, name: "%events", desc: "show event queue and signals in flight"},
-	{group: groupState, name: "%current", desc: "show current state and configuration"},
-	{group: groupState, name: "%advance", args: "<time>", desc: "advance simulation time by <time> units, processing every event due"},
+	{name: "%help", group: groupSession, desc: "show this help"},
+	{name: "%list", group: groupSession, desc: "list current session declarations"},
+	{name: "%clear", group: groupSession, desc: "reset the session"},
+	{name: "%load", group: groupSession, args: "<path>...", desc: "submit the contents of files, directories or globs"},
+	{name: "%print", group: groupSession, args: "[name]", desc: "print the session model as SysML notation, or just the named element"},
+	{name: "%save", group: groupSession, args: "<file>", desc: "write the session model to a file (.sysml notation, or .ttl RDF — experimental)"},
+	{name: cmdQuery, group: groupSession, args: "<oslc-query>", desc: "identify model elements using OSLC Query text"},
+	{name: "%quit", group: groupSession, desc: "exit the REPL (also %exit)"},
+	{name: "%exit", group: groupSession, desc: "exit the REPL", alias: true},
+
+	{name: "%verbosity", group: groupSettings, args: "[level]", desc: "show or set output level: quiet, normal or debug"},
+	{name: "%trace", group: groupSettings, args: "[on|off]", desc: "show or set execution tracing (evaluation, calc, action and state steps)"},
+	{name: "%strict", group: groupSettings, args: "[on|off]", desc: "show or set strict conformance: report notation no SysML v2 production admits as an error"},
+	{name: "%schedule", group: groupSettings, args: "[<policy>]", desc: "show or set the scheduling policy runs started from here on resolve choice points under: declared, reverse or seed:<n>"},
+	{name: "%seed", group: groupSettings, args: "[<n>|off]", desc: "show or set the seed runs started from here on draw their modeled randomness from — Probability-weighted decisions, RandomFunctions — whatever the schedule; off leaves it to the schedule's seed:<n>"},
+	{name: "%budget", group: groupSettings, desc: "show the bounds one run may spend, and the variable raising each"},
+	{name: "%jobs", group: groupSettings, args: "[<n>]", desc: "show or set how many runs of one check go concurrently: an exploration's linearizations, the engines all consults"},
+
+	{name: "%engines", group: groupEngines, args: "[probe]", desc: "list the analysis engines, with the kind, protocol and authority of each, the questions it answers and whether it can run; probe also starts each external engine once and checks it against its manifest"},
+	{name: "%engine", group: groupEngines, args: "[<name>|auto|all]", desc: "show or set the engine questions asked from here on are put to: one by name, auto for the strongest covering one, or all for every covering one"},
+
+	{name: "%check-diverge", group: groupChecks, args: "[<feature>...|off]", desc: "show or set the features the check engine compares final values of across schedules; off compares every attribute of the action and of its performing object, or of the action alone when it has none"},
+	{name: "%check-property", group: groupChecks, args: "[<name>...|off]", desc: "show or set the constraints and requirements the check engine evaluates at every stable state of an action"},
+	{name: "%check-input", group: groupChecks, args: "[<feature>...|off]", desc: "show or set the features the smt engine leaves free in their declared domains although the model binds them; off frees only the inputs the model leaves unbound"},
+	{name: "%check-assume", group: groupChecks, args: "[<name>...|off]", desc: "show or set the constraints and requirements the smt engine assumes over the initial state of an action"},
+	{name: "%check-witness", group: groupChecks, args: "[<dir>|off]", desc: "show or set the directory the check and smt engines write a witness to for each violation and divergent value"},
+	{name: "%check-bounds", group: groupChecks, args: "[depth=<n>] [states=<n>] [unroll=<n>] [timeout=<duration>] | off", desc: "show or set the bounds the check and smt engines search within: the moves of one schedule, the distinct states, the iterations of a loop the smt engine unrolls, and the clock; off restores their defaults"},
+	{name: "%replay", group: groupChecks, args: "<witness>", desc: "install the schedule a witness file fixes, so the next %action or %state steps the run it records"},
+
+	{name: "%search", group: groupLibrary, args: "<substring>", desc: "list the declared and library symbols whose qualified name contains <substring>"},
+	{name: "%builtins", group: groupLibrary, desc: "list the library functions this build implements directly"},
+	{name: "%view", group: groupLibrary, args: argName, desc: "show what a view exposes, and the views nested in it"},
+	{name: "%render", group: groupLibrary, args: "<name> [form [palette]]", desc: "render a view as the rendering it states — as text, as a Mermaid diagram or a Markdown table, or as Graphviz DOT or PlantUML, filled from a named palette"},
+
+	{name: "%instantiate", group: groupRuntime, args: argName, desc: "create an instance of a part def"},
+	{name: "%eval", group: groupRuntime, args: "[in <name>|<path>|#<id> :] <expr>", desc: "evaluate an expression, in the named element or object when one is named"},
+	{name: "%features", group: groupRuntime, args: "<object> [all|depth <n>] [json]", desc: "show an object's feature values and what its behaviors are doing, bounded unless all or a depth is asked for; json writes the object graph as the API does; an object is named, #<id>, or a path such as car.fl or #1.wheels[2]"},
+	{name: "%instances", group: groupRuntime, desc: "list all instantiated objects"},
+	{name: "%invoke", group: groupRuntime, args: "<object> <op> [<p>=<expr>]", desc: "invoke an operation of an object's type, performed by that object; an object is named, #<id>, or a path such as car.fl"},
+
+	{name: "%calc", group: groupBehavioral, args: "<name> <args>", desc: "invoke a calculation with arguments"},
+	{name: cmdAnalysis, group: groupBehavioral, args: "<name>[(<args>)] [<object>]", desc: "run an analysis case and report its outputs and the verdict of its objective; arguments bind its inputs and an object is its subject"},
+	{name: cmdSweep, group: groupBehavioral, args: "<name>[(<args>)] [<object>] <p>=<from>..<to>[:<step>]...", desc: "run an analysis case or calc once per value of each range, one run per row of the cartesian product, and print the table"},
+	{name: cmdSamples, group: groupBehavioral, args: "<n> <seed> <name>[(<args>)] [<object>] <p>=<from>..<to>...", desc: "run an analysis case or calc over <n> values drawn uniformly from each range with the given seed, and print the table"},
+	{name: cmdRuns, group: groupBehavioral, args: "<n> <seed> <action> [<observable>...]", desc: "run an action <n> times, each run's modeled randomness seeded from the given seed, and print the table of the observables with each one's distribution"},
+	{name: cmdRunQuery, group: groupBehavioral, args: "<name> [<p>=<expr>...]", desc: "execute a document query and print its rows, with each binding written as <parameter>=<expression>"},
+	{name: cmdRenderDocument, group: groupBehavioral, args: "<name> [mermaid|dot|plantuml]", desc: "compile a document definition, run its queries and print the rendered Markdown, its graph-shaped diagrams as Mermaid, Graphviz DOT or PlantUML"},
+	{name: "%constraint", group: groupBehavioral, args: argName, desc: "evaluate a constraint definition"},
+	{name: "%requirement", group: groupBehavioral, args: argName, desc: "evaluate a requirement definition"},
+	{name: "%satisfy", group: groupBehavioral, args: "[name]", desc: "evaluate the satisfaction assertions of the model, or of one element"},
+	{name: "%validate", group: groupBehavioral, args: "<object>", desc: "check every assertion about an object and the objects it holds: the asserted constraints of their types, the requirements they carry and the satisfactions they are subject of; an object is named, #<id>, or a path such as car.engine"},
+	{name: "%check", group: groupBehavioral, args: argName, desc: "ask an SMT solver whether a constraint, requirement or satisfaction can be satisfied (experimental)"},
+	{name: "%explain", group: groupBehavioral, args: argName, desc: "ask an SMT solver which conditions of an unsatisfiable element conflict (experimental)"},
+	{name: "%solve", group: groupBehavioral, args: argName, desc: "ask an SMT solver for values satisfying an element, keeping what is already fixed (experimental)"},
+	{name: "%configure", group: groupBehavioral, args: "<name> [<variation>=<variant>...] [all [<count>]]", desc: "ask an SMT solver which variants an element's conditions permit (experimental)"},
+	{name: "%optimize", group: groupBehavioral, args: argName, desc: "ask an SMT solver for the best values an analysis case's objectives admit (experimental)"},
+
+	{name: "%action", group: groupAction, args: "<name> [<object>]", desc: "start action executor debugging session, performed by an object"},
+	{name: "%step", group: groupAction, desc: "advance one token step, or one step of the state machine being debugged"},
+	{name: "%continue", group: groupAction, desc: "run action to completion"},
+	{name: "%tokens", group: groupAction, desc: "show active tokens"},
+	{name: "%break", group: groupAction, args: "<node>", desc: "set breakpoint at node"},
+	{name: "%stop", group: groupAction, desc: "stop current debugging session"},
+
+	{name: "%state", group: groupState, args: "<name> [<object>]", desc: "debug the machine an object exhibits (naming that machine alone attaches to the one object exhibiting it; with none or several, name the object), or a state machine performed by an object; an object is named, #<id>, or a path such as car.fl"},
+	{name: "%send", group: groupState, args: "<signal>[(<p>=<expr>, ...)] [to <object>]", desc: "send a signal to an object's machine, by default the one being debugged; an object is named, #<id>, or a path such as car.fl"},
+	{name: "%events", group: groupState, desc: "show event queue and signals in flight"},
+	{name: "%current", group: groupState, desc: "show current state and configuration"},
+	{name: "%advance", group: groupState, args: "<time>", desc: "advance simulation time by <time> units, processing every event due"},
 }
 
 // helpText renders the command table, one line per command under its heading.
 func helpText() []string {
-	const width = 20
-	var out []string
+	out := []string{
+		"Lines starting with % are commands; anything else is SysML notation.",
+		"Commands are listed by task; <angle brackets> name an argument, [square",
+		"brackets] an optional one.",
+	}
 	group := ""
 	for _, c := range metaCommandTable {
 		if c.alias {
 			continue
 		}
-		if c.group != group && c.group != "" {
+		if c.group != group {
 			group = c.group
 			out = append(out, "", group)
 		}
-		usage := strings.TrimSpace(c.name + " " + c.args)
-		if pad := width - len(usage); pad > 0 {
-			usage += strings.Repeat(" ", pad)
-		} else {
-			usage += "  "
+		out = append(out, helpEntry(c)...)
+	}
+	return out
+}
+
+// helpColumn is where a command's description starts; a signature too wide
+// for it takes a line of its own, and helpWidth is where the text wraps.
+const (
+	helpColumn = 28
+	helpWidth  = 78
+)
+
+// helpEntry is one command's help lines: its signature, folded when too wide
+// for one line, then its description wrapped into the column after it.
+func helpEntry(c metaCommand) []string {
+	margin := strings.Repeat(" ", helpColumn)
+	signature := strings.Split(usage.Wrap(c.name+" "+c.args, helpWidth-6), "\n")
+	out := []string{"  " + signature[0]}
+	for _, line := range signature[1:] {
+		out = append(out, "      "+line)
+	}
+	for i, line := range strings.Split(usage.Wrap(c.desc, helpWidth-helpColumn), "\n") {
+		if i == 0 && len(signature) == 1 && len(out[0]) < helpColumn-1 {
+			out[0] += margin[len(out[0]):] + line
+			continue
 		}
-		out = append(out, usage+c.desc)
+		out = append(out, margin+line)
 	}
 	return out
 }
diff --git a/internal/frontend/repl/meta_test.go b/internal/frontend/repl/meta_test.go
index a827339e73..0e4ab0081f 100644
--- a/internal/frontend/repl/meta_test.go
+++ b/internal/frontend/repl/meta_test.go
@@ -26,6 +26,37 @@ func TestMetaHelpAndList(t *testing.T) {
 	}
 }
 
+// Every command sits under a heading, aliases are folded into the command
+// they spell, and no line, a wide signature included, outruns the width.
+func TestHelpTextIsGroupedAndWrapped(t *testing.T) {
+	lines := helpText()
+	help := strings.Join(lines, "\n")
+	for _, want := range []string{
+		"\nSession:\n", "\nSettings:\n", "\nAnalysis engines:\n", "\nChecking every schedule:\n",
+		"\nLibrary discovery:\n", "\nState machine debugging:\n",
+		"  %quit                     exit the REPL (also %exit)\n",
+		"  %check-witness [<dir>|off]\n                            show or set",
+		"  %check-bounds [depth=<n>] [states=<n>] [unroll=<n>] [timeout=<duration>]\n      | off\n",
+	} {
+		if !strings.Contains(help, want) {
+			t.Errorf("help lacks %q:\n%s", want, help)
+		}
+	}
+	if strings.Contains(help, "\n  %exit") {
+		t.Errorf("help lists the alias %%exit on its own:\n%s", help)
+	}
+	for _, c := range metaCommandTable {
+		if c.group == "" {
+			t.Errorf("%s has no help heading", c.name)
+		}
+	}
+	for _, line := range lines {
+		if len(line) > helpWidth {
+			t.Errorf("help line is %d wide: %q", len(line), line)
+		}
+	}
+}
+
 func TestMetaClear(t *testing.T) {
 	s := NewSession()
 	s.Submit("package P { }")
diff --git a/internal/frontend/usage/roff.go b/internal/frontend/usage/roff.go
index f020882902..a567b7463f 100644
--- a/internal/frontend/usage/roff.go
+++ b/internal/frontend/usage/roff.go
@@ -41,7 +41,15 @@ func (d Doc) WriteRoff(w io.Writer, fs *flag.FlagSet, meta ManMeta) {
 	}
 
 	fmt.Fprintf(w, ".SH OPTIONS\n")
-	writeOptions(w, fs)
+	if len(d.Options) == 0 {
+		writeOptions(w, fs)
+	}
+	for _, g := range d.Options {
+		fmt.Fprintf(w, ".SS %s\n", roffEscape(g.Title))
+		for _, o := range g.Options {
+			writeRoffOption(w, fs, o)
+		}
+	}
 
 	for _, sec := range d.Sections {
 		fmt.Fprintf(w, ".SH %s\n", roffEscape(strings.ToUpper(sec.Title)))
@@ -62,20 +70,52 @@ func (d Doc) WriteRoff(w io.Writer, fs *flag.FlagSet, meta ManMeta) {
 // set visits them, so a flag cannot be documented only in the help.
 func writeOptions(w io.Writer, fs *flag.FlagSet) {
 	fs.VisitAll(func(f *flag.Flag) {
-		placeholder, help := flag.UnquoteUsage(f)
+		placeholder, _ := flag.UnquoteUsage(f)
 		fmt.Fprintf(w, ".TP\n")
 		if placeholder == "" {
 			fmt.Fprintf(w, ".B \\-%s\n", roffEscape(f.Name))
 		} else {
 			fmt.Fprintf(w, ".BI \\-%s \" %s\"\n", roffEscape(f.Name), roffEscape(placeholder))
 		}
-		if !isZeroDefault(f.DefValue) {
-			help = sentence(help) + " The default is " + f.DefValue + "."
-		}
-		fmt.Fprintf(w, "%s\n", roffText(help))
+		fmt.Fprintf(w, "%s\n", roffText(roffHelp(f)))
 	})
 }
 
+// writeRoffOption writes one grouped option as a .BR tag: spellings in bold,
+// commas and argument in roman, the argument's <name> in italic.
+func writeRoffOption(w io.Writer, fs *flag.FlagSet, o Option) {
+	f := fs.Lookup(o.Name)
+	var words []string
+	for i, n := range o.names() {
+		if i > 0 {
+			words = append(words, `", "`)
+		}
+		words = append(words, "\\-"+roffEscape(n))
+	}
+	if o.Arg != "" {
+		arg := strings.NewReplacer("<", "\\fI", ">", "\\fP").Replace(roffEscape(o.Arg))
+		if !strings.HasPrefix(o.Arg, "[") {
+			arg = " " + arg
+		}
+		words = append(words, `"`+arg+`"`)
+	}
+	macro := ".BR"
+	if len(words) == 1 {
+		macro = ".B"
+	}
+	fmt.Fprintf(w, ".TP\n%s %s\n", macro, strings.Join(words, " "))
+	fmt.Fprintf(w, "%s\n", roffText(roffHelp(f)))
+}
+
+// roffHelp is the flag's description with its default stated as a sentence.
+func roffHelp(f *flag.Flag) string {
+	text := help(f)
+	if !isZeroDefault(f.DefValue) {
+		text = sentence(text) + " The default is " + f.DefValue + "."
+	}
+	return text
+}
+
 // sentence ends a flag's usage string so a sentence may follow it.
 func sentence(text string) string {
 	text = strings.TrimRight(text, " ")
@@ -89,7 +129,7 @@ func sentence(text string) string {
 // flag package's own help omits.
 func isZeroDefault(value string) bool {
 	switch value {
-	case "", "0", "false", "0s":
+	case "", "[]", "0", "false", "0s":
 		return true
 	}
 	return false
diff --git a/internal/frontend/usage/text.go b/internal/frontend/usage/text.go
index 8d6a6a65e1..8c020a7b0a 100644
--- a/internal/frontend/usage/text.go
+++ b/internal/frontend/usage/text.go
@@ -11,8 +11,8 @@ import (
 // survive a copied transcript in an 80-column window.
 const textWidth = 78
 
-// WriteText writes the terminal help to w: the synopsis, the flags as the flag
-// set itself describes them, then every section not reserved for the man page.
+// WriteText writes the terminal help to w: the synopsis, the sections wanted
+// first, the flags by group, then every other section not reserved for the man page.
 func (d Doc) WriteText(w io.Writer, fs *flag.FlagSet) {
 	// PrintDefaults writes to the flag set's own stream, restored after so it
 	// does not decide where a later error is reported.
@@ -20,35 +20,86 @@ func (d Doc) WriteText(w io.Writer, fs *flag.FlagSet) {
 	fs.SetOutput(w)
 	defer fs.SetOutput(previous)
 
-	for i, form := range d.Synopsis {
-		label := "Usage:"
-		if i > 0 {
-			label = "      "
-		}
-		fmt.Fprintf(w, "%s %s %s\n", label, d.Command, form)
-	}
+	d.writeSynopsis(w)
 	for _, para := range d.Description {
 		fmt.Fprintf(w, "\n%s\n", Wrap(para, textWidth))
 	}
-	fmt.Fprintf(w, "\nOptions:\n")
-	fs.PrintDefaults()
+	for _, sec := range d.Sections {
+		if sec.BeforeOptions && !sec.ManOnly {
+			writeSection(w, sec)
+		}
+	}
+	if len(d.Options) == 0 {
+		fmt.Fprintf(w, "\nOptions:\n")
+		fs.PrintDefaults()
+	}
+	for _, g := range d.Options {
+		fmt.Fprintf(w, "\n%s:\n", g.Title)
+		for _, o := range g.Options {
+			writeOption(w, fs, o)
+		}
+	}
 
 	for _, sec := range d.Sections {
-		if sec.ManOnly {
+		if sec.ManOnly || sec.BeforeOptions {
 			continue
 		}
-		fmt.Fprintf(w, "\n%s:\n", sec.Title)
-		for _, para := range sec.Lead {
-			fmt.Fprintf(w, "%s\n", Wrap(para, textWidth))
+		writeSection(w, sec)
+	}
+}
+
+// WriteHint writes what a misuse is answered with: the synopsis and where the
+// help is, rather than the help itself, which would bury the error.
+func (d Doc) WriteHint(w io.Writer) {
+	d.writeSynopsis(w)
+	fmt.Fprintf(w, "Run '%s -help' for the options.\n", d.Command)
+}
+
+func (d Doc) writeSynopsis(w io.Writer) {
+	for i, form := range d.Synopsis {
+		label := "Usage:"
+		if i > 0 {
+			label = "      "
 		}
-		writeExamples(w, sec.Examples)
-		writeItems(w, sec.Items)
-		for i, para := range sec.Paragraphs {
-			if i > 0 || len(sec.Examples) > 0 || len(sec.Items) > 0 {
-				fmt.Fprintln(w)
-			}
-			fmt.Fprintf(w, "%s\n", Wrap(para, textWidth))
+		fmt.Fprintf(w, "%s %s %s\n", label, d.Command, form)
+	}
+}
+
+func writeSection(w io.Writer, sec Section) {
+	fmt.Fprintf(w, "\n%s:\n", sec.Title)
+	for _, para := range sec.Lead {
+		fmt.Fprintf(w, "%s\n", Wrap(para, textWidth))
+	}
+	writeExamples(w, sec.Examples)
+	writeItems(w, sec.Items)
+	for i, para := range sec.Paragraphs {
+		if i > 0 || len(sec.Examples) > 0 || len(sec.Items) > 0 {
+			fmt.Fprintln(w)
 		}
+		fmt.Fprintf(w, "%s\n", Wrap(para, textWidth))
+	}
+}
+
+// optionColumn is where an option's description starts, beside a spelling that
+// fits and under one that does not.
+const optionColumn = 30
+
+// writeOption writes the flag's spellings and, wrapped in the column beside
+// them, its description with the default the flag package would show.
+func writeOption(w io.Writer, fs *flag.FlagSet, o Option) {
+	f := fs.Lookup(o.Name)
+	text := help(f)
+	if !isZeroDefault(f.DefValue) {
+		text += fmt.Sprintf(" (default %s)", f.DefValue)
+	}
+	spelling := "  " + o.spelling()
+	margin := strings.Repeat(" ", optionColumn)
+	body := indent(Wrap(text, textWidth-optionColumn), margin)
+	if len(spelling) < optionColumn-1 {
+		// The body opens with the margin; the spelling takes that many of its spaces.
+		fmt.Fprintf(w, "%s%s\n", spelling, body[len(spelling):])
+	} else {
+		fmt.Fprintf(w, "%s\n%s\n", spelling, body)
 	}
 }
 
diff --git a/internal/frontend/usage/text_test.go b/internal/frontend/usage/text_test.go
index 1e3b8c83f5..ee12a7820b 100644
--- a/internal/frontend/usage/text_test.go
+++ b/internal/frontend/usage/text_test.go
@@ -1,6 +1,8 @@
 package usage
 
 import (
+	"bytes"
+	"flag"
 	"strings"
 	"testing"
 )
@@ -17,3 +19,63 @@ func TestWrapKeepsWordsWholeWithinTheWidth(t *testing.T) {
 		t.Errorf("wrapping changed the words: %q", got)
 	}
 }
+
+func groupedDoc() (Doc, *flag.FlagSet) {
+	fs := flag.NewFlagSet("t", flag.ContinueOnError)
+	var b bool
+	var s string
+	fs.BoolVar(&b, "help", false, "Show this help")
+	fs.BoolVar(&b, "h", false, "Show this help")
+	fs.StringVar(&s, "target", "c", "Compile to `language` "+strings.Repeat("and more ", 12))
+	d := Doc{
+		Command:  "t",
+		Synopsis: []string{"[options]"},
+		Options: []OptionGroup{{Title: "General", Options: []Option{
+			Opt("help", "", "h"),
+			Opt("target", "<language>"),
+		}}},
+	}
+	return d, fs
+}
+
+func TestGroupedOptionsFoldAliasesAndWrap(t *testing.T) {
+	d, fs := groupedDoc()
+	var out bytes.Buffer
+	d.WriteText(&out, fs)
+	text := out.String()
+	for _, want := range []string{"\nGeneral:\n", "  -h, -help   ", "  -target <language>   ", "(default c)"} {
+		if !strings.Contains(text, want) {
+			t.Errorf("help lacks %q:\n%s", want, text)
+		}
+	}
+	for _, line := range strings.Split(text, "\n") {
+		if len(line) > textWidth {
+			t.Errorf("line is %d wide: %q", len(line), line)
+		}
+	}
+
+	out.Reset()
+	d.WriteRoff(&out, fs, ManMeta{})
+	roff := out.String()
+	for _, want := range []string{".SS General\n", `.BR \-h ", " \-help` + "\n", `.BR \-target " \fIlanguage\fP"` + "\n", "The default is c."} {
+		if !strings.Contains(roff, want) {
+			t.Errorf("man page lacks %q:\n%s", want, roff)
+		}
+	}
+}
+
+func TestCheckOptionsFindsStrayFlags(t *testing.T) {
+	d, fs := groupedDoc()
+	if err := d.CheckOptions(fs); err != nil {
+		t.Fatalf("complete groups: %v", err)
+	}
+	var extra bool
+	fs.BoolVar(&extra, "extra", false, "not grouped")
+	if err := d.CheckOptions(fs); err == nil || !strings.Contains(err.Error(), "-extra") {
+		t.Errorf("ungrouped flag not reported: %v", err)
+	}
+	d.Options[0].Options = append(d.Options[0].Options, Opt("extra", ""), Opt("missing", ""))
+	if err := d.CheckOptions(fs); err == nil || !strings.Contains(err.Error(), "-missing") {
+		t.Errorf("undeclared option not reported: %v", err)
+	}
+}
diff --git a/internal/frontend/usage/usage.go b/internal/frontend/usage/usage.go
index 8d5b612c1e..fa18269b8e 100644
--- a/internal/frontend/usage/usage.go
+++ b/internal/frontend/usage/usage.go
@@ -3,6 +3,13 @@
 // cannot drift.
 package usage
 
+import (
+	"flag"
+	"fmt"
+	"sort"
+	"strings"
+)
+
 // Doc is everything the help and the man page say about one command, apart from
 // the flags themselves: those are read from the command's own flag set, which is
 // the only place a flag is declared.
@@ -17,12 +24,34 @@ type Doc struct {
 	Synopsis []string
 	// Description holds the paragraphs a reader needs before the flags.
 	Description []string
+	// Options groups the flags by the task they serve, in the order printed.
+	// Empty, the flags are listed as the flag set declares them.
+	Options []OptionGroup
 	// Sections are the blocks printed after the options, in order.
 	Sections []Section
 	// SeeAlso names related pages as "name(section)", plus any URLs.
 	SeeAlso []string
 }
 
+// OptionGroup is one titled block of the option list.
+type OptionGroup struct {
+	// Title heads the block: "Checking a model", "Deprecated".
+	Title   string
+	Options []Option
+}
+
+// Option is one entry of the option list: a flag with its alternative spellings.
+type Option struct {
+	// Name is the flag as declared, without its dash.
+	Name string
+	// Aliases are the other spellings the flag set declares for the same
+	// setting, listed with the name rather than as entries of their own.
+	Aliases []string
+	// Arg is the argument's placeholder, "<name>", or "[=<name>]" when optional;
+	// empty for a boolean flag.
+	Arg string
+}
+
 // Section is one titled block of the help: worked examples, prose, a labelled
 // list, or a combination, rendered in that order.
 type Section struct {
@@ -36,6 +65,9 @@ type Section struct {
 	Items []Item
 	// Paragraphs is the prose closing the block.
 	Paragraphs []string
+	// BeforeOptions prints the block ahead of the option list in the terminal
+	// help, for the examples a reader wants before any flag.
+	BeforeOptions bool
 	// ManOnly keeps the block out of the terminal help, for reference material
 	// that belongs in a page a reader consults rather than in a flag summary.
 	ManOnly bool
@@ -63,6 +95,12 @@ func Entry(label, text string) Item {
 	return Item{Label: label, Text: text}
 }
 
+// Opt is an option list entry for the flag name, with the argument placeholder
+// arg ("" for a boolean flag) and any alternative spellings.
+func Opt(name, arg string, aliases ...string) Option {
+	return Option{Name: name, Arg: arg, Aliases: aliases}
+}
+
 // Section is the manual section the page belongs in, 1 where none is stated.
 func (d Doc) Section() int {
 	if d.ManSection == 0 {
@@ -70,3 +108,59 @@ func (d Doc) Section() int {
 	}
 	return d.ManSection
 }
+
+// CheckOptions reports a flag the groups leave out or name twice, or an option
+// the flag set does not declare, so a flag cannot go undocumented.
+func (d Doc) CheckOptions(fs *flag.FlagSet) error {
+	if len(d.Options) == 0 {
+		return nil
+	}
+	seen := map[string]bool{}
+	for _, g := range d.Options {
+		for _, o := range g.Options {
+			for _, name := range append([]string{o.Name}, o.Aliases...) {
+				if fs.Lookup(name) == nil {
+					return fmt.Errorf("option -%s is documented but not declared", name)
+				}
+				if seen[name] {
+					return fmt.Errorf("option -%s is documented twice", name)
+				}
+				seen[name] = true
+			}
+		}
+	}
+	var err error
+	fs.VisitAll(func(f *flag.Flag) {
+		if err == nil && !seen[f.Name] {
+			err = fmt.Errorf("flag -%s is declared but in no option group", f.Name)
+		}
+	})
+	return err
+}
+
+// names lists the option's spellings, shorthand first: -e, -eval.
+func (o Option) names() []string {
+	names := append([]string{o.Name}, o.Aliases...)
+	sort.SliceStable(names, func(i, j int) bool { return len(names[i]) < len(names[j]) })
+	return names
+}
+
+// spelling is the option as the terminal help writes it: "-e, -eval <expr>",
+// "-satisfy[=<name>]".
+func (o Option) spelling() string {
+	text := "-" + strings.Join(o.names(), ", -")
+	switch {
+	case o.Arg == "":
+	case strings.HasPrefix(o.Arg, "["):
+		text += o.Arg
+	default:
+		text += " " + o.Arg
+	}
+	return text
+}
+
+// help is the flag's usage string with its backquoted placeholder unquoted.
+func help(f *flag.Flag) string {
+	_, text := flag.UnquoteUsage(f)
+	return text
+}
diff --git a/man/man1/sysml.1 b/man/man1/sysml.1
index 78dbbebca6..5d0b163cd9 100644
--- a/man/man1/sysml.1
+++ b/man/man1/sysml.1
@@ -12,375 +12,322 @@ others whichever order they were named in. With no expression or check to
 carry out it opens an interactive prompt; otherwise it does what was asked and
 exits on the verdict, which is what lets a run gate a build.
 .SH OPTIONS
+.SS General
 .TP
-.BI \-action " value"
-Run this action to completion, as \-action "Drive rover1" to run it on an
-object; under \-schedule explore each run performs it on an object of its own,
-named as a definition or usage to create, a path into one such as
-mission.rover, or, named alone, the run's one \-instantiate object performing
-it (repeatable)
+.BR \-h ", " \-help
+Show this help and exit
 .TP
-.BI \-advance " value"
-Simulated time units to run the \-action and \-state behaviors for, on one
-shared clock (default: a state machine takes only its initial transition; an
-action runs to completion)
+.BR \-v ", " \-version
+Show the version and exit
 .TP
-.BI \-analysis " value"
-Run this analysis or verification case and report its outputs and the verdict
-of its objective, as \-analysis "Pkg::Case(3.0) Pkg::part" with arguments for
-its inputs and an object as its subject; a verification case also reports the
-verdict its body produced (repeatable)
+.B \-man
+Write this command's manual page, in roff, to stdout and exit
+.SS Evaluating
 .TP
-.BI \-calc " value"
-Invoke this calculation and report what it computed, as \-calc "Fall(3, 4)"
+.BR \-e ", " \-eval " \fIexpr\fP"
+Evaluate this expression, against the model when one is loaded, and exit
 (repeatable)
 .TP
-.BI \-check\-assume " value"
-With \-engine smt or \-engine all: assume this constraint or requirement over
-the initial state of the action, as \-check\-assume Plant::EnvelopeLimits; a
-set no initial state satisfies is reported not covered, never proved
-(repeatable)
+.BR \-query " \fItext\fP"
+Evaluate this OSLC Query text against the model and exit
+.SS Checking a model
 .TP
-.BI \-check\-depth " value"
-With \-engine check, \-engine smt or \-engine all: the most moves one schedule
-may make before the search backtracks, or the moves the smt engine unrolls the
-action to, named as the depth bound hit (default 10000 for check, 40 for smt)
-.TP
-.BI \-check\-diverge " value"
-With \-engine check, \-engine smt or \-engine all: report this feature
-sensitive when schedules leave it with different final values \(em check
-searching the schedules, smt asking the solver for two that end it apart \(em
-as \-check\-diverge x, \-check\-diverge step.out for a performed node's output
-or \-check\-diverge this.level for the performing object's (not covered under
-smt), a name nothing holds refused; default every attribute of the action and
-of its performing object, the action's own when it has none (repeatable)
-.TP
-.BI \-check\-input " value"
-With \-engine smt or \-engine all: leave this feature of the action free in
-its declared domain although the model binds it, as \-check\-input inletTemp;
-a name that is not a feature the action reads is refused. Without it, every
-input the model leaves unbound is free and every bound one is pinned
+.BR \-validate "[=\fIobject\fP]"
+Report the model's diagnostics and exit, nonzero on an error;
+\-validate=<object> checks instead every assertion about that object
 (repeatable)
 .TP
-.BI \-check\-property " value"
-With \-engine check or \-engine all: evaluate this constraint or requirement
-at every stable state of the action, on the performing object when there is
-one, and report a schedule at which it is false (repeatable)
-.TP
-.BI \-check\-states " value"
-With \-engine check or \-engine all: the most distinct states the search may
-visit, named as the states bound hit; the same figure \-engine all gives an
-exploration as its runs (default 1000000)
-.TP
-.BI \-check\-timeout " value"
-With \-engine check, \-engine smt or \-engine all: the time the check's plan
-may run for, as 30s or 2m, and the time each of the smt engine's solver
-queries may take in place of OPENSYSML_SMT_TIMEOUT; a search it stops is
-reported incomplete with the states and depth reached, not as a verdict
-.TP
-.BI \-check\-unroll " value"
-With \-engine smt or \-engine all: the most iterations of one loop the smt
-engine unrolls before it stops, named as the unroll bound hit (default 4)
-.TP
-.BI \-check\-witness " string"
-With \-engine check, \-engine smt or \-engine all: write a witness file to
-this directory for each violation and each divergent value \(em the inputs the
-solver chose, the schedule's choices, a blank line, then the run's trace \(em
-which \-schedule replay:<file> and %replay follow
-.TP
-.BI \-compile " string"
-Compile this calc def to a native executable named by \-o, as \-compile
-Pkg::Fib
+.B \-strict
+Judge the model as conforming SysML v2: notation no pinned production admits
+is an error, not a warning
 .TP
-.BI \-constraint " value"
+.BR \-constraint " \fIname\fP"
 Evaluate this constraint and exit (repeatable)
 .TP
-.BI \-convert " string"
-Convert the model to this format instead of running it: sysml, kerml, ttl,
-turtle or rdf (RDF is experimental)
-.TP
-.BI \-cpuprofile " string"
-Write a CPU profile of the run to this file, for go tool pprof
+.BR \-requirement " \fIname\fP"
+Evaluate this requirement, and every verification case verifying it, and exit
+(repeatable)
 .TP
-.B \-debug
-Report every diagnostic over the whole session buffer, with the pass that
-produced it
+.BR \-satisfy "[=\fIname\fP]"
+Evaluate every satisfaction assertion, or with \-satisfy=<name> those the
+named element states, and exit (repeatable)
 .TP
-.BI \-diagram\-form " string"
-Form the graph\-shaped diagrams of \-render\-document and \-render\-documents
-are written in: mermaid (default), dot or plantuml; a table\-kind view is a
-table either way
+.BR \-calc " \fIcall\fP"
+Invoke this calculation and report its result, as \-calc "Fall(3, 4)"
+(repeatable)
 .TP
-.BI \-doc\-form " string"
-Form \-render\-document and \-render\-documents write: markdown (default),
-html or pdf, which drives an external converter
+.BR \-analysis " \fIcall\fP"
+Run this analysis or verification case and report its outputs and verdict, as
+\-analysis "Pkg::Case(3.0) Pkg::part" (repeatable)
 .TP
-.B \-doc\-number\-sections
-Number the section headings hierarchically (\-doc\-form html or pdf)
+.BR \-run\-query " \fIquery\fP"
+Execute this document query and report its rows, as \-run\-query "Heavy
+root=telescope" (repeatable)
 .TP
-.B \-doc\-title\-page
-Put the document title on a page of its own (\-doc\-form html or pdf)
+.BR \-instantiate " \fIname\fP"
+Create an object of this definition or usage before the checks, so a verdict
+is about it (repeatable)
 .TP
-.B \-doc\-toc
-Write a table of contents ahead of the content (\-doc\-form html or pdf)
-.TP
-.BI \-e " value"
-Evaluate expression and exit (shorthand)
-.TP
-.BI \-engine " value"
-Analysis engine every check is put to: auto (default) picks the strongest
-engine covering the question, all puts it to every covering engine in name
-order and composes their answers, or an engine by name (run, explore, check,
-smt, sweep, solve, tool:<name> from OPENSYSML_TOOLS, or an external engine
-from OPENSYSML_ENGINES), whose refusal is then the answer; \-engine explore is
-\-schedule explore, \-engine check searches every schedule of each \-action
-for a violation, deadlock, failure or divergence, and \-engine smt decides
-each \-check\-property over every schedule and every value of the action's
-free inputs through an SMT solver
+.B \-json
+Report checks as one JSON document rather than as lines
+.SS Running behaviors
 .TP
-.B \-engines
-List the analysis engines this build knows \(em name, kind (built\-in, tool,
-engine, policy, sampler), protocol, authority, the questions each answers and
-whether its process is found \(em with the manifest entry and resolved command
-of each external one, spawning nothing, and exit
+.BR \-action " \fIname\fP"
+Run this action to completion, as \-action "Drive rover1" to run it on an
+object (repeatable)
 .TP
-.BI \-eval " value"
-Evaluate expression and exit (can be specified multiple times)
+.BR \-state " \fIname\fP"
+Run this state machine, as \-state "Mission rover1" to run it on an object
+(repeatable)
 .TP
-.BI \-from " string"
-Input format for \-convert: sysml, kerml, ttl, turtle, rdf, or xmi/uml/mdzip
-for a SysML v1 model to migrate (experimental; default: from the input's
-extension)
+.BR \-advance " \fItime\fP"
+Simulated time units to run the \-action and \-state behaviors for, on one
+shared clock; without it a state machine takes only its initial transition
 .TP
-.B \-h
-Show this help (shorthand)
+.BR \-schedule " \fIpolicy\fP"
+Policy every run resolves its choice points under: declared, reverse
+(default), seed:<n>, explore[:runs=N,depth=D] or replay:<file>
 .TP
-.B \-help
-Show this help and exit
+.BR \-seed " \fIn\fP"
+Seed the model's own draws \(em weighted decisions, random functions \(em and
+those of \-samples and \-runs; the same seed draws the same run or table
 .TP
-.BI \-html\-css " value"
-Style the HTML with this stylesheet: a file is inlined, a URL is linked
-(repeatable, applied in order after the default sheet)
+.BR \-runs " \fIn\fP"
+Run the \-action this many times, each run seeded from \-seed, and table the
+\-observe features; needs \-seed
 .TP
-.B \-html\-default\-css
-Write the default document stylesheet and exit, as a starting point for your
-own
+.BR \-observe " \fIfeature\fP"
+Report this feature of the \-runs action, or clock for the time it completed
+at; default every feature it holds and the clock (repeatable)
 .TP
-.B \-html\-fragment
-Write the document element alone, without the page shell or a stylesheet, to
-embed in a page of your own
+.BR \-sweep " \fIrange\fP"
+Run the \-analysis or \-calc once per value of this range, as \-sweep
+"n=1..8:2"; several ranges run their cartesian product (repeatable)
 .TP
-.BI \-html\-math " string"
-Have the HTML page load MathJax to typeset its formulas: cdn loads a pinned
-release from jsDelivr, a URL loads the script it names (default: formulas stay
-LaTeX source)
+.BR \-samples " \fIn\fP"
+Draw this many values uniformly from each \-sweep range instead of stepping
+through it; needs \-seed
 .TP
-.BI \-html\-mermaid " string"
-Have the HTML page load Mermaid to draw its diagrams: cdn loads a pinned
-release from jsDelivr, a URL loads the script it names (default: diagrams stay
-Mermaid source)
+.BR \-jobs " \fIn\fP"
+Runs of one check that may go concurrently, each on a worker of its own;
+default OPENSYSML_JOBS, else the number of CPUs
+.SS Analysis engines
 .TP
-.B \-html\-no\-default\-css
-Leave the default stylesheet out, so only \-html\-css sheets style the
-document
+.B \-engines
+List the analysis engines this build knows and their status, spawning nothing,
+and exit
 .TP
-.BI \-html\-theme " string"
-Style the HTML page with a bundled theme layered over the default stylesheet:
-default, modern, print or report (default: the default stylesheet alone)
+.B \-probe
+With \-engines, also start each external engine once and report the outcome as
+its status
 .TP
-.BI \-instantiate " value"
-Create an object of this definition or usage before the checks, so a verdict
-is about it; under \-schedule explore, \-engine check, smt or all, each run
-creates an object of it of its own before the behaviors start, one per
-\-instantiate, which a \-state or \-action named alone attaches to and a path
-such as mission.vehicle walks into (repeatable)
+.BR \-engine " \fIname\fP"
+Analysis engine every check is put to: auto (default), all, or one by name
+\(em run, explore, check, smt, sweep, solve, tool:<name> or an external engine
+.SS Checking every schedule (\-engine check, smt or all)
 .TP
-.BI \-jobs " value"
-Runs of one check that may go concurrently \(em the linearizations of an
-exploration, the engines \-engine all consults \(em each on a worker of its
-own over the shared model; the result is the same at any count. Default
-OPENSYSML_JOBS, else the number of CPUs
+.BR \-check\-property " \fIname\fP"
+Evaluate this constraint or requirement at every stable state of the action
+and report a schedule at which it is false (repeatable)
 .TP
-.B \-json
-Report checks as one JSON document rather than as lines
+.BR \-check\-diverge " \fIfeature\fP"
+Report this feature sensitive when schedules leave it with different final
+values, as x, step.out or this.level; default every attribute (repeatable)
 .TP
-.B \-man
-Write this command's manual page, in roff, to stdout and exit
+.BR \-check\-input " \fIfeature\fP"
+Under smt, leave this feature of the action free in its declared domain
+although the model binds it (repeatable)
 .TP
-.BI \-memprofile " string"
-Write a heap profile of the run to this file, for go tool pprof
+.BR \-check\-assume " \fIname\fP"
+Under smt, assume this constraint or requirement over the initial state of the
+action (repeatable)
 .TP
-.B \-memstats
-Report on stderr what the run cost: wall time, memory allocated, memory taken
-from the OS
+.BR \-check\-witness " \fIdir\fP"
+Write a witness file for each violation and each divergent value to this
+directory, for \-schedule replay:<file> and %replay to follow
 .TP
-.BI \-migration\-report " string"
-With \-convert from xmi: write the element\-by\-element migration report to
-this file (JSON when it ends in .json, text otherwise)
+.BR \-check\-depth " \fIn\fP"
+The most moves one schedule may make before the search backtracks, or the
+moves smt unrolls the action to (default 10000 for check, 40 for smt)
 .TP
-.BI \-o " string"
-Write conversion output to this file (shorthand)
+.BR \-check\-states " \fIn\fP"
+Under check, the most distinct states the search may visit (default 1000000)
 .TP
-.BI \-observe " clock"
-Report this feature of the \-runs action, or clock for the time it completed
-at; default every feature it holds and the clock (repeatable)
+.BR \-check\-unroll " \fIn\fP"
+Under smt, the most iterations of one loop the solver unrolls before it stops
+(default 4)
 .TP
-.BI \-output " string"
-Write conversion output to this file (default: stdout)
+.BR \-check\-timeout " \fIduration\fP"
+The time the check's plan may run for, as 30s or 2m, and the time each smt
+solver query may take in place of OPENSYSML_SMT_TIMEOUT
+.SS Converting and migrating
 .TP
-.BI \-pdf\-engine " string"
-Converter \-doc\-form pdf drives: weasyprint (default), pandoc or prince
+.BR \-convert " \fIformat\fP"
+Convert the model to this format instead of running it: sysml, kerml, ttl,
+turtle or rdf (RDF is experimental)
 .TP
-.B \-pdf\-number\-sections
-Number the section headings hierarchically (\-doc\-form pdf)
+.BR \-from " \fIformat\fP"
+Input format for \-convert: sysml, kerml, ttl, turtle, rdf, or xmi, uml or
+mdzip for a SysML v1 model to migrate (experimental); default the input's
+extension
 .TP
-.B \-pdf\-title\-page
-Put the document title on a page of its own (\-doc\-form pdf)
+.BR \-o ", " \-output " \fIfile\fP"
+Write what \-convert, \-compile, \-render or \-render\-document produces to
+this file instead of stdout
 .TP
-.B \-pdf\-toc
-Write a table of contents ahead of the content (\-doc\-form pdf)
+.BR \-migration\-report " \fIfile\fP"
+With \-convert from xmi, write the element\-by\-element migration report to
+this file: JSON when it ends in .json, text otherwise
+.SS Compiling natively
 .TP
-.B \-probe
-With \-engines, also start each external engine once, check its describe
-against its manifest entry field by field and report the outcome as its status
+.BR \-compile " \fIcalc\fP"
+Compile this calc def to a native executable named by \-o, as \-compile
+Pkg::Fib
 .TP
-.BI \-query " string"
-Evaluate OSLC Query text against the model instead of running the REPL
+.BR \-target " \fIbackend\fP"
+Backend \-compile generates code for: c or go. The default is c.
 .TP
-.B \-quiet
-Report errors only, suppressing warnings
+.B \-source
+With \-compile, write the generated source to \-o instead of building it
+.SS Rendering views
 .TP
-.BI \-render " string"
-Render this view of the model (every file named, loaded as one) instead of
-running it, in the form its render member states
+.BR \-render " \fIview\fP"
+Render this view of the model instead of running it, in the form its render
+member states
 .TP
-.BI \-render\-all " string"
+.BR \-render\-all " \fIdir\fP"
 Render every declared view into this directory
 .TP
-.BI \-render\-document " string"
+.BR \-render\-form " \fIform\fP"
+Form \-render or \-render\-all writes: text, mermaid, markdown, dot or
+plantuml; default from the destination for \-render, each kind's machine form
+for \-render\-all
+.TP
+.BR \-render\-palette " \fIpalette\fP"
+Palette the dot or plantuml form fills nodes from, by keyword family:
+okabe\-ito, tol\-bright, tol\-muted, tol\-light, brewer\-set2, brewer\-dark2,
+viridis or cividis; default black and white
+.SS Rendering documents
+.TP
+.BR \-render\-document " \fIname\fP"
 Compile this document definition, run its queries and write the rendered
-Markdown
+document
 .TP
-.BI \-render\-documents " string"
-Render every document definition as linked Markdown into this directory
+.BR \-render\-documents " \fIdir\fP"
+Render every document definition, linked to one another, into this directory
 .TP
-.BI \-render\-form " string"
-Form \-render or \-render\-all writes: text, mermaid, markdown, dot or
-plantuml (default: destination\-dependent for \-render, each kind's machine
-form for \-render\-all)
+.BR \-doc\-form " \fIform\fP"
+Form the documents are written in: markdown (default), html or pdf, which
+drives an external converter
 .TP
-.BI \-render\-palette " string"
-Palette the DOT or PlantUML form of \-render or \-render\-all fills nodes
-from, by keyword family: okabe\-ito, tol\-bright, tol\-muted, tol\-light,
-brewer\-set2, brewer\-dark2, viridis or cividis (default: black and white)
+.BR \-diagram\-form " \fIform\fP"
+Form the documents' graph\-shaped diagrams are written in: mermaid (default),
+dot or plantuml; a table\-kind view is a table either way
 .TP
-.BI \-requirement " value"
-Evaluate this requirement and exit, reporting beside its verdict the verdict
-of every verification case verifying it (repeatable)
+.B \-doc\-title\-page
+Put the document title on a page of its own (html or pdf)
 .TP
-.BI \-run\-query " value"
-Execute this document query and report its rows, as \-run\-query
-"HeavySubsystems root=telescope" (repeatable)
+.B \-doc\-toc
+Write a table of contents ahead of the content (html or pdf)
 .TP
-.BI \-runs " value"
-Run the \-action this many times, each run's modeled randomness (weighted
-decisions, random functions) seeded from \-seed, and report the table of the
-\-observe features with each one's distribution; needs \-seed
+.B \-doc\-number\-sections
+Number the section headings hierarchically (html or pdf)
 .TP
-.BI \-samples " value"
-Draw this many values uniformly from each \-sweep range instead of stepping
-through them, Integers or reals as the parameter is typed; needs \-seed
+.BR \-pdf\-engine " \fIconverter\fP"
+Converter \-doc\-form pdf drives: weasyprint (default), pandoc or prince
+.SS Styling HTML documents
 .TP
-.B \-satisfy
-Evaluate every satisfaction assertion, or with \-satisfy=<name> those the
-named element states, reporting beside each verdict the verdict of every
-verification case verifying the requirement (repeatable). The default is [].
+.BR \-html\-theme " \fItheme\fP"
+Style the page with a bundled theme layered over the default stylesheet:
+default, modern, print or report
 .TP
-.BI \-schedule " value"
-Scheduling policy every run resolves its choice points under (concurrent
-tokens, overlapping guards, competing transitions): declared, reverse
-(default), seed:<n> for a reproducible pseudo\-random order,
-explore[:runs=N,depth=D] to run every linearization within the budget and
-table the distinct outcomes, or replay:<file> to follow a witness file's
-choice lines move for move, then reverse
+.BR \-html\-css " \fIfile|url\fP"
+Style the page with this stylesheet too: a file is inlined, a URL is linked
+(repeatable, applied in order after the default sheet)
 .TP
-.BI \-seed " value"
-Seed the model's own draws \(em Probability\-weighted decisions,
-RandomFunctions \(em come from in every run made, whatever \-schedule, and the
-seed \-samples or \-runs draws from; the same seed draws the same run or table
+.B \-html\-no\-default\-css
+Leave the default stylesheet out, so only \-html\-css sheets style the
+document
 .TP
-.B \-source
-With \-compile, write the generated source to \-o instead of building it
+.B \-html\-fragment
+Write the document element alone, without the page shell or a stylesheet, to
+embed in a page of your own
 .TP
-.BI \-state " value"
-Run this state machine, as \-state "Mission rover1" to run it on an object;
-under \-schedule explore each run creates the object of its own, named as a
-definition or usage to create or a path such as mission.rover into one \(em
-the declaration is created once per run, so machines on sibling parts share it
-and its connectors \(em or, named alone, the run's one \-instantiate object
-exhibiting it (repeatable)
+.B \-html\-default\-css
+Write the default document stylesheet, or with \-html\-theme that theme's
+whole sheet, and exit
 .TP
-.B \-strict
-Judge the model as conforming SysML v2: notation no pinned production admits
-is an error, not a warning
+.BR \-html\-mermaid " cdn|\fIurl\fP"
+Have the page load Mermaid to draw its diagrams: cdn loads a pinned release
+from jsDelivr, a URL the script it names
 .TP
-.BI \-sweep " value"
-Run the named \-analysis or \-calc once per value of this range, as \-sweep
-"speed=0.0 [SI::'m/s']..10.0 [SI::'m/s']:2.0 [SI::'m/s']"; the values are
-produced in the parameter's declared type; several ranges run their cartesian
-product (repeatable)
+.BR \-html\-math " cdn|\fIurl\fP"
+Have the page load MathJax to typeset its formulas: cdn loads a pinned release
+from jsDelivr, a URL the script it names
+.SS Syncing against a repository
 .TP
-.BI \-sync\-annotate " string"
-Write the model to this file with each minted id declared as an @ElementId
-annotation (needs \-sync\-mint\-ids)
+.BR \-sync\-diff " \fIrepo\fP"
+Show the change set between the model and this repository \(em a graph file
+(.ttl) or a SysML v2 API endpoint URL \(em and exit; never writes
 .TP
-.BI \-sync\-apply " string"
+.BR \-sync\-apply " \fIurl\fP"
 Apply the change set to the model's project branch at this SysML v2 API
-endpoint URL, then record the commit in the sync state (token from
-FLEXO_INTEROP_TOKEN)
+endpoint URL, then record the commit in the sync state
 .TP
-.BI \-sync\-base " string"
+.BR \-sync\-base " \fIfile\fP"
 Repository graph at the last\-seen commit; with it, repository changes since
 then surface as conflicts
 .TP
+.BR \-sync\-state " \fIfile\fP"
+Sync state file recording project, branch and last\-seen commit; default
+<model>.sync.json beside the model
+.TP
 .B \-sync\-confirm\-deletes
 Confirm repository\-side deletes; without it the diff reports them but
 applying is refused
 .TP
-.BI \-sync\-diff " string"
-Show the change set between the model and this repository \(em a graph file
-(.ttl) or a SysML v2 API endpoint URL \(em keyed by effective element id,
-instead of running it; never writes
-.TP
 .B \-sync\-mint\-ids
 Mint a UUID for each unannotated element being created, so the repository can
 address it stably
 .TP
-.BI \-sync\-state " string"
-Sync state file recording project, branch and last\-seen commit (default:
-<model>.sync.json beside the model)
+.BR \-sync\-annotate " \fIfile\fP"
+Write the model to this file with each minted id declared as an @ElementId
+annotation (needs \-sync\-mint\-ids)
+.SS Diagnostics and profiling
 .TP
-.BI \-target " string"
-Backend \-compile generates code for: c (default) or go. The default is c.
+.B \-debug
+Report every diagnostic over the whole session buffer, with the pass that
+produced it
 .TP
-.BI \-to " value"
-Replaced by \-convert, which names the output format
+.B \-quiet
+Report errors only, suppressing warnings
 .TP
 .B \-trace
 Report each execution step: expression evaluation, calc invocation, action
 tokens, state transitions
 .TP
-.B \-v
-Show version (shorthand)
+.BR \-cpuprofile " \fIfile\fP"
+Write a CPU profile of the run to this file, for go tool pprof
+.TP
+.BR \-memprofile " \fIfile\fP"
+Write a heap profile of the run to this file, for go tool pprof
+.TP
+.B \-memstats
+Report on stderr what the run cost: wall time, memory allocated, memory taken
+from the OS
+.SS Deprecated
+.TP
+.BR \-to " \fIformat\fP"
+Replaced by \-convert, which names the output format
+.TP
+.B \-pdf\-title\-page
+Former name of \-doc\-title\-page, which also shapes HTML
 .TP
-.B \-validate
-Analyse the model and report its diagnostics, exiting nonzero on an error;
-with \-validate=<object> check instead every assertion about an object
-\-instantiate created and the objects it holds, an object named, #<id>, or a
-path such as car.engine (repeatable). The default is [].
+.B \-pdf\-toc
+Former name of \-doc\-toc, which also shapes HTML
 .TP
-.B \-version
-Show version information
+.B \-pdf\-number\-sections
+Former name of \-doc\-number\-sections, which also shapes HTML
 .SH EXAMPLES
 .RS 2
 .nf
@@ -434,7 +381,38 @@ sysml \-satisfy \-json model.sysml
 .fi
 .RE
 .PP
-Each check flag may be repeated.
+Each check flag may be repeated. \-validate=<object> checks every assertion
+about an object \-instantiate created and the objects it holds: an object
+named, #<id>, or a path such as car.engine. \-requirement and \-satisfy report
+beside each verdict the verdict of every verification case verifying the
+requirement. \-analysis takes arguments for the case's inputs and an object as
+its subject, as \-analysis "Pkg::Case(3.0) Pkg::part"; a verification case
+also reports the verdict its body produced.
+.SH RUNNING ACTIONS AND STATE MACHINES
+\-action runs an action to completion and \-state a state machine, both on one
+shared clock that \-advance runs for the given simulated time units; without
+\-advance a state machine takes only its initial transition. Either names a
+definition or usage, or one followed by the object to perform it on, as
+\-action "Drive rover1".
+.PP
+\-schedule is the policy every run resolves its choice points under \(em
+concurrent tokens, overlapping guards, competing transitions: declared,
+reverse (the default), seed:<n> for a reproducible pseudo\-random order,
+explore[:runs=N,depth=D] to run every linearization within the budget and
+table the distinct outcomes, or replay:<file> to follow a witness file's
+choice lines move for move, then reverse.
+.PP
+Under \-schedule explore, \-engine check, smt or all, each run creates objects
+of its own before the behaviors start: one per \-instantiate, which a \-state
+or \-action named alone attaches to, and one per \-action or \-state naming a
+definition or usage to create or a path into one such as mission.rover. The
+declaration is created once per run, so machines on sibling parts share it and
+its connectors.
+.PP
+\-jobs is how many runs of one check may go concurrently \(em the
+linearizations of an exploration, the engines \-engine all consults \(em each
+on a worker of its own over the shared model; the result is the same at any
+count.
 .SH ANALYSIS ENGINES
 .RS 2
 .nf
@@ -469,6 +447,59 @@ evidence \(em observed (one run), witnessed (a replayed execution), bounded
 the strength and is named. Under \-json each check carries the plan and one
 results[] entry per engine that answered, with its engine, claim, strength,
 bounds and witness.
+.PP
+\-engines lists each engine's name, kind (built\-in, tool, engine, policy,
+sampler), protocol, authority, the questions it answers and whether its
+process is found, with the manifest entry and resolved command of each
+external one; \-probe also starts each external engine once and checks its
+describe against its manifest entry field by field. An engine is named run,
+explore, check, smt, sweep, solve, tool:<name> from OPENSYSML_TOOLS, or as an
+external engine from OPENSYSML_ENGINES. \-engine explore is \-schedule
+explore; \-engine check searches every schedule of each \-action for a
+violation, deadlock, failure or divergence; \-engine smt decides each
+\-check\-property over every schedule and every value of the action's free
+inputs through an SMT solver.
+.SH CHECKING EVERY SCHEDULE
+.RS 2
+.nf
+# Search every schedule for Safe
+sysml \-engine check \-action Go \-check\-property Safe m.sysml
+# Is speed schedule\-dependent?
+sysml \-engine check \-action Go \-check\-diverge speed m.sysml
+sysml \-engine smt \-action Go \-check\-input t \-check\-property Safe \e
+    m.sysml
+# A witness file per finding
+sysml \-engine check \-action Go \-check\-witness out m.sysml
+.fi
+.RE
+.PP
+\-check\-property evaluates a constraint or requirement at every stable state
+of the action, on the performing object when there is one, and reports a
+schedule at which it is false. \-check\-diverge reports a feature sensitive
+when schedules leave it with different final values \(em check searching the
+schedules, smt asking the solver for two that end it apart \(em named as x,
+step.out for a performed node's output or this.level for the performing
+object's (not covered under smt); a name nothing holds is refused, and without
+it every attribute of the action and of its performing object is checked, the
+action's own when it has none.
+.PP
+Under smt every input the model leaves unbound is free and every bound one is
+pinned; \-check\-input leaves a bound feature free in its declared domain, and
+a name that is not a feature the action reads is refused. \-check\-assume
+assumes a constraint or requirement over the initial state; a set no initial
+state satisfies is reported not covered, never proved.
+.PP
+\-check\-witness writes a file for each violation and each divergent value
+\(em the inputs the solver chose, the schedule's choices, a blank line, then
+the run's trace \(em which \-schedule replay:<file> and %replay follow. A
+bound is named when it is hit: \-check\-depth is the most moves one schedule
+may make before the search backtracks, or the moves smt unrolls the action to;
+\-check\-states the most distinct states the search may visit, the same figure
+\-engine all gives an exploration as its runs; \-check\-unroll the most
+iterations of one loop smt unrolls; \-check\-timeout the time the plan may run
+for and the time each solver query may take in place of OPENSYSML_SMT_TIMEOUT
+\(em a search it stops is reported incomplete with the states and depth
+reached, not as a verdict.
 .SH SWEEPING AND SAMPLING A PARAMETER
 .RS 2
 .nf
@@ -556,8 +587,10 @@ sysml in.txt \-convert ttl \-from sysml
 .RE
 .PP
 The input format is taken from the file extension (.sysml, .kerml, .ttl)
-unless \-from names it. Converting to the format it is already in rewrites the
-input: notation is reformatted, Turtle is normalized.
+unless \-from names it: sysml, kerml, ttl, turtle, rdf, or xmi, uml or mdzip
+for a SysML v1 model to migrate, whose element\-by\-element report
+\-migration\-report writes out. Converting to the format it is already in
+rewrites the input: notation is reformatted, Turtle is normalized.
 .PP
 RDF conversion is experimental: the mapping covers model structure and the
 behavior its bodies state, refuses what it cannot write back, and its
@@ -639,15 +672,17 @@ The rendering is the one the view's render member states, and a containment
 tree where it states none. It is tool\-defined output: SysML v2 specifies the
 notation, not how a tool draws it. Notices \(em an empty view, an element the
 rendering cannot represent \(em go on stderr. Every file named is loaded as
-one model, so a view may expose elements a sibling file declares. A
-graph\-shaped rendering is written as a Mermaid diagram by default, as
-Graphviz DOT with \-render\-form dot and as PlantUML with \-render\-form
-plantuml, which also writes a sequence rendering; neither Graphviz nor
-PlantUML is needed to write them. Both are drawn in the black\-and\-white
-style of the SysML v2 Pilot visualizer; \-render\-palette fills their nodes by
-keyword family from a colourblind\-safe palette (okabe\-ito, tol\-bright,
-tol\-muted, tol\-light, brewer\-set2, brewer\-dark2, viridis or cividis),
-keeping black text legible on every fill.
+one model, so a view may expose elements a sibling file declares.
+\-render\-form names the form written \(em text, mermaid, markdown, dot or
+plantuml; by default \-render takes it from the destination and \-render\-all
+writes each kind's machine form. A graph\-shaped rendering is written as a
+Mermaid diagram by default, as Graphviz DOT with \-render\-form dot and as
+PlantUML with \-render\-form plantuml, which also writes a sequence rendering;
+neither Graphviz nor PlantUML is needed to write them. Both are drawn in the
+black\-and\-white style of the SysML v2 Pilot visualizer; \-render\-palette
+fills their nodes by keyword family from a colourblind\-safe palette
+(okabe\-ito, tol\-bright, tol\-muted, tol\-light, brewer\-set2, brewer\-dark2,
+viridis or cividis), keeping black text legible on every fill.
 .SH RENDERING A DOCUMENT
 .RS 2
 .nf