Workflows

Workflow A: start from tests/logs

1. Add test and log traces:

   speclogician ch trace test-add --art-id T1 --name "test positive" --given "{ x = 1 }" --when "{ amount = 2 }" --then "{ x = 3 }"
   speclogician ch trace log-add --art-id L1 --filename "prod.log" --given "{ x = 0 }" --contents "OrderAccepted"

2. Add a minimal domain model (state/action types)
3. Add predicates to describe observed properties
4. Add scenarios that match observed behavior
5. Use diffs to measure progress: check scenarios_valid_pct and components_valid_pct

Workflow B: start from requirements/docs

1. Add doc artifacts:

   speclogician ch data doc-add --art-id D1 --text "Orders must be rejected if qty > 10000"

2. Add predicates and transitions that encode key rules
3. Add scenarios to cover each requirement clause
4. Link artifacts to the formal components they support:

   speclogician ch data link --art-id D1 --comp-name qty_too_big

5. Track linked_artifacts_pct in the diff to measure coverage

Workflow C: start from code (agentic)

1. Use CodeLogician/ImandraX to extract formal structure from code
2. Add source code references:

   speclogician ch data src-add --art-id S1 --src-code "def check(order): ..." --language python

3. Use batch operations for efficiency:

   speclogician ch batch --json < changes.json

4. Validate batches cheaply before committing:

   speclogician ch batch --dry-run --json < changes.json

5. Iterate: inspect with view state --compact, diagnose with reach properties, refine

The refinement loop

In all workflows, after every batch of changes:

speclogician view state --compact     # current state overview
speclogician view diff --json         # what changed + progress metrics
speclogician reach properties         # safety + liveness check (SAFE? LIVE?)
speclogician reach unreachable        # dead scenarios
speclogician reach frontier           # scenarios with no successors

If a change made things worse, undo it:

speclogician undo --json

Use safety and liveness to drive refinement:

The backbone is always the same: incremental typed changes + global verification after every step + measurable progress metrics