Core Concepts

What is hence?

hence is a CLI tool that evaluates defeasible logic plans to coordinate work across multiple autonomous agents. You write a plan — a text file describing tasks, their dependencies, readiness conditions, and assignment rules — and hence evaluates that plan to answer questions like "what should I work on next?" or "why is task X still blocked?"

The key insight is that coordination logic lives in the plan file, not in agent code. Each agent is a simple loop: ask hence what to do, do it, record findings, repeat. The plan file accumulates facts as agents work, and the reasoner re-evaluates the full program on every query. There is no central server, no shared mutable state beyond the file itself, and no orchestrator process that must stay alive.

The SPL file format

Plans are written in SPL (Spindle Lisp), a Lisp-style syntax that maps directly onto defeasible logic constructs. Files conventionally use the .spl extension. SPL is human-readable, diff-friendly, and designed so that LLM agents can both read and append to plans without special tooling.

; A minimal plan with one task
(given task-setup)
(given task-build)
(given task-deploy)

(given depends-build-on-setup)
(given depends-deploy-on-build)

(normally r-assign-setup
  (task-setup)
  (assigned-setup-to-alice))

Defeasible logic primer

Defeasible logic is a form of non-monotonic reasoning that handles defaults and exceptions, formalised by Donald Nute (1994). In classical (strict) logic, a conclusion that follows from the premises is final. In defeasible logic, a conclusion can be defeated by a conflicting rule that has higher priority. This makes it possible to express "normally X is true, except when Y."

Most task coordination is written imperatively — scripts, state machines, orchestrators that sequence steps explicitly. Defeasible logic is declarative: you describe what is true under what conditions, and the reasoner works out the consequences. This means you can add a new exception or override without rewriting the existing rules — you just state what takes priority.

Rules fire when their conditions match, more specific rules override general ones, and the reasoner computes a stable set of conclusions from the full program. hence builds on SPINdle, a defeasible reasoning engine created by Ho-Pun Lam and Guido Governatori at NICTA, reimplemented in Rust as spindle-rust.

(given ...) — unconditional facts

A given form asserts a fact that is unconditionally true. It has no conditions and cannot be defeated. Use given for declarations: tasks exist, agents exist, dependencies hold, configuration values are set.

; Declare that these tasks exist in the plan
(given task-provision-db)
(given task-run-migrations)
(given task-deploy-api)

; Declare a dependency: run-migrations requires provision-db to be complete first
(given depends-run-migrations-on-provision-db)

; Declare that the "ops" agent exists
(given agent-ops)

Facts asserted with given are said to be definitely true. They contribute to the strongest possible proof status and are never retracted by other rules. Think of them as your axioms.

(normally LABEL CONDITION CONCLUSION) — defeasible rules

A normally form expresses a defeasible rule: "if condition holds, then normally conclude conclusion." The label is a unique name for the rule used by prefer to establish priorities.

; Normally, if a task exists and is ready, the default agent is assigned to it
(normally r-default-assign
  (task-NAME ready-NAME)
  (assigned-NAME-to-default-agent))

; Normally, a task is ready if all its dependencies are complete
(normally r-ready-no-deps
  (task-NAME)
  (ready-NAME))

; Normally, a task with a dependency is NOT ready until that dependency completes
(normally r-blocked-by-dep
  (depends-NAME-on-DEP)
  (~ready-NAME))    ; ~ means "not"

; But if the dependency IS complete, the blocking rule is defeated
(normally r-dep-done-unblocks
  (depends-NAME-on-DEP completed-DEP)
  (ready-NAME))

(prefer r-dep-done-unblocks r-blocked-by-dep)

(prefer RULE-A RULE-B) — resolving conflicts

When two defeasible rules produce conflicting conclusions, the reasoner needs to know which one wins. prefer says that RULE-A defeats RULE-B when they conflict. Without a prefer, conflicting rules leave the contested conclusion in an undecided state — neither provably true nor provably false.

; General rule: ops agent handles all deployment tasks
(normally r-ops-deploys
  (task-NAME deployment-task-NAME)
  (assigned-NAME-to-ops))

; Exception: if the task is flagged production-critical, senior-ops takes it
(normally r-senior-ops-critical
  (task-NAME deployment-task-NAME production-critical-NAME)
  (assigned-NAME-to-senior-ops))

; r-senior-ops-critical is more specific, so it should win when both apply
(prefer r-senior-ops-critical r-ops-deploys)

Priority is not transitive by default in many defeasible systems, but hence follows standard defeasibility: if A is preferred over B, and B conflicts with A, then A's conclusion stands and B's conclusion is defeated. Explicit prefer declarations make the priority structure visible in the plan file itself, which aids explainability.

How this differs from strict logic

In classical predicate logic, once you prove something, it stays proven. Adding new premises can only add more conclusions, never remove them — this is called monotonicity. Defeasible logic is non-monotonic: adding a new fact or rule can defeat a previously supported conclusion.

The practical consequence for plan authoring: you can write a general policy and then add exceptions incrementally. A plan that starts with "every task is assigned to the default agent" can grow to have fine-grained routing rules without touching the original rule.

The open-world assumption

hence operates under the open-world assumption (OWA). This means: if a fact is not present in the plan, that does not mean it is false — it means the truth value of that fact is simply unknown. This is distinct from the closed-world assumption (CWA) used by most databases, where absence of a record means the value is false.

In practice: to make a conclusion hold, you need a rule that fires. To make it definitely not hold, you need a rule that concludes its negation. Silence is not negation.

Plans as logical programs

A .spl file is a logical program: a set of facts and rules that collectively describe the state of a project and the policies governing agent behaviour. Plans are append-only in practice — agents add new fact blocks as they work, and the reasoner re-evaluates the complete program from scratch on every query.

Anatomy of a plan file

; ── Metadata (optional but recommended) ────────────────────────────
(meta plan-name "Deploy v2.3 to production")
(meta plan-version "1")
(meta plan-author "alice")

; ── Task declarations ───────────────────────────────────────────────
(given task-smoke-test)
(given task-db-backup)
(given task-deploy-canary)
(given task-monitor-canary)
(given task-full-rollout)

; ── Dependencies ────────────────────────────────────────────────────
(given depends-deploy-canary-on-db-backup)
(given depends-deploy-canary-on-smoke-test)
(given depends-monitor-canary-on-deploy-canary)
(given depends-full-rollout-on-monitor-canary)

; ── Assignment rules ────────────────────────────────────────────────
(normally r-qa-smoke-test
  (task-smoke-test)
  (assigned-smoke-test-to-qa))

(normally r-ops-backup
  (task-db-backup)
  (assigned-db-backup-to-ops))

(normally r-ops-canary
  (task-deploy-canary)
  (assigned-deploy-canary-to-ops))

; ── Agent findings (appended by agents as they work) ────────────────
(claims agent:qa
  :at "2026-02-24T09:00:00Z"
  (given completed-smoke-test)
  (given finding-smoke-test-all-green))

(claims agent:ops
  :at "2026-02-24T09:15:00Z"
  (given completed-db-backup)
  (given finding-db-backup-size-42gb))

How facts accumulate

When an agent completes a task, it appends a (claims ...) block to the plan file. This block asserts one or more facts — typically completed-TASK plus any relevant findings the agent discovered. These facts immediately become available to the reasoner, so subsequent queries reflect the updated state.

; Agent "ops" appends this block after completing the canary deployment
(claims agent:ops
  :at "2026-02-24T10:30:00Z"
  (given completed-deploy-canary)
  (given finding-canary-version-2.3.1)
  (given finding-canary-endpoint-https://api-canary.example.com))

Claims blocks are identified by the claiming agent's name. The reasoner treats facts from claims blocks as defeasible assertions from that agent — structurally equivalent to normally rules with no conditions. This means claims can be overridden if conflicting, higher-priority information is present.

Stateless evaluation

The reasoner has no persistent state. Every time you run a hence command, it reads the plan file from disk, evaluates the full logical program, and returns the result. There is no cache, no running process, no database. The .spl file is the state.

This design has important consequences:

• Reproducibility — given the same file, hence always produces the same answer. You can audit any point in the plan's history by checking out the file at an earlier commit.
• No coordination overhead — agents don't need to talk to a server between commands. They just read and append to a file, which can be a local path, a shared network mount, or a hence.run URL.
• Simplicity — debugging is straightforward. If something is concluded unexpectedly, run hence query explain and inspect the proof. The full program is always visible in the file.

Tasks and agents

What is a task?

A task is a named unit of work declared with (given task-NAME). The name is a symbol — typically kebab-case — that identifies the task throughout the plan. Tasks are not structured records; they are simply atoms that other rules can reference.

; Three tasks, each a bare fact
(given task-audit-dependencies)
(given task-patch-vulnerabilities)
(given task-write-security-report)

By convention, tasks can carry additional metadata as separate facts, using a naming pattern of ATTRIBUTE-TASKNAME:

; Metadata facts for the patch task
(given priority-high-patch-vulnerabilities)
(given security-sensitive-patch-vulnerabilities)
(given estimated-hours-8-patch-vulnerabilities)

What is an agent?

An agent is any process that runs hence commands. It has an identity — a name string or an Ed25519 public key — and can claim tasks, assert findings, and complete tasks. Agents are not declared in the plan; they emerge from the claims they make and the assignments the plan's rules produce.

In a small team workflow, agent identities are simple strings like "alice" or "ops-bot". For cryptographically verified workflows (using hence agent whoami), the identity is derived from an Ed25519 key pair stored locally, and claims are signed so the reasoner can verify authorship.

Claimed and completed conclusions

When a plan's rules or an agent's claims assert claimed-TASK or completed-TASK, the reasoner derives these as conclusions. You do not assert these directly as given facts — instead, they flow from (claims ...) blocks or from rules that fire when an agent calls hence task claim or hence task complete.

; When the CLI appends a claim block, this is what it looks like
(claims agent:alice
  :at "2026-02-24T10:00:00Z"
  (given claimed-audit-dependencies))   ; agent has claimed the task

; Later, when the agent finishes:
(claims agent:alice
  :at "2026-02-24T11:45:00Z"
  (given completed-audit-dependencies)  ; task is done
  (given finding-audit-found-12-cves))   ; agent finding, available to later rules

Plan rules can reference completed-TASK in their conditions, creating a natural dependency chain: a downstream task becomes ready when its upstream tasks are completed.

; patch-vulnerabilities is only ready once audit-dependencies is done
(normally r-patch-ready
  (task-patch-vulnerabilities
   completed-audit-dependencies)
  (ready-patch-vulnerabilities))

Agent identity and the HENCE_AGENT variable

Every hence command that modifies a plan (claim, complete, assert) needs to know who is acting. hence resolves agent identity from the HENCE_AGENT environment variable. If it is not set, hence falls back to a key-based identity derived from the local Ed25519 key pair.

Setting a simple string identity

# Use a human-readable name for casual or single-agent use
export HENCE_AGENT=alice

# Or set it inline for a single command
HENCE_AGENT=ops-bot hence task claim deploy-canary plan.spl

Key-based identity with hence agent whoami

For multi-agent workflows where you want verifiable authorship, hence automatically creates an Ed25519 key pair on first use. The public key becomes the agent's canonical identity, and claims blocks are signed with the private key. No initialisation command is needed.

# Identity is created automatically on first use — no init command needed.
# Show the current identity lines:
hence agent whoami
# → supervisor:ed25519:a3f9b2c1
# → agent:ed25519:a3f9b2c1
# → evaluator:ed25519:b4e8f3d2
# → PeerId: 12D3KooW...

# When HENCE_AGENT is set, the agent line shows the name instead:
export HENCE_AGENT=alice
hence agent whoami
# → supervisor:ed25519:a3f9b2c1
# → agent:alice
# → evaluator:ed25519:b4e8f3d2
# → PeerId: 12D3KooW...

# Unset to revert to key-based identity:
unset HENCE_AGENT
hence agent whoami
# → supervisor:ed25519:a3f9b2c1
# → agent:ed25519:a3f9b2c1
# → evaluator:ed25519:b4e8f3d2
# → PeerId: 12D3KooW...

How identity flows into the plan

When an agent asserts a claim, hence wraps it in a (claims AGENT-NAME ...) block and appends it to the file. Assignment rules reference this name explicitly:

; This rule fires only when the agent identity is "security-bot"
(normally r-security-bot-gets-sensitive
  (task-NAME security-sensitive-NAME)
  (assigned-NAME-to-security-bot))

; The agent checks if it has an assignment:
; # $ HENCE_AGENT=security-bot hence task next plan.spl
; # → task-patch-vulnerabilities

Plan queries

Once a plan is loaded, you interact with it through queries — commands that ask the reasoner to evaluate specific conclusions and report the results. Queries are always read-only; they never modify the plan file.

hence task next — what should I work on?

The most common query is asking hence what task the current agent should work on. hence evaluates which tasks are assigned to the current agent's identity and are in a ready state (all dependencies complete, not already claimed).

# What should alice work on?
HENCE_AGENT=alice hence task next plan.spl
# → task-write-security-report

# Machine-readable output for scripting
HENCE_AGENT=alice hence task next plan.spl --json
# → {
#      "next_actions": [
#        {
#          "task": "write-security-report",
#          "agent": "alice",
#          "literal": "assign-to-write-security-report-alice",
#          "command": "hence task claim write-security-report plan.spl --agent alice"
#        }
#      ]
#    }

If no tasks are currently available for the agent — because all assigned tasks are either blocked, already claimed by another agent, or completed — hence returns an appropriate message and exits with a non-zero status code, which agent loops can use to detect idle state.

hence query explain — why was this concluded?

When you want to understand why the reasoner reached a particular conclusion, use hence query explain. It prints a proof tree showing which rules fired, which facts they depended on, and the proof status of each node.

# Why is task-patch-vulnerabilities assigned to security-bot?
hence query explain assigned-patch-vulnerabilities-to-security-bot plan.spl

; Example explain output (simplified)
+d assigned-patch-vulnerabilities-to-security-bot
   via r-security-bot-gets-sensitive
   requires:
     +D task-patch-vulnerabilities          ; given fact
     +D security-sensitive-patch-vulnerabilities  ; given fact
   not defeated by:
     r-ops-deploys                           ; lower priority, defeated

The proof tree is particularly useful when agent behaviour seems surprising. Rather than reading the full plan file and reasoning manually, you can ask hence to show its work.

hence query why-not — why is this NOT concluded?

The complement of explain is why-not: given a conclusion that you expected to hold, why does the reasoner not support it? This is invaluable for debugging blocked tasks and missing assignments.

# Why isn't deploy-canary ready yet?
hence query why-not ready-deploy-canary plan.spl

; Example why-not output (simplified)
-d ready-deploy-canary
   would require rule r-canary-ready to fire, but:
     missing: completed-db-backup
       ; no claims block has asserted completed-db-backup
     missing: completed-smoke-test
       ; no claims block has asserted completed-smoke-test
   defeated by: r-blocked-by-dep
     depends-deploy-canary-on-db-backup holds  ; given fact
     depends-deploy-canary-on-smoke-test holds  ; given fact

The why-not output tells you exactly what is missing: which facts need to exist for the conclusion to be reached, and which rules are currently defeating it.

Other useful queries

# Show all tasks and their current status
hence plan board plan.spl

# Show all conclusions the reasoner currently supports
hence query all plan.spl

# Check a specific conclusion (returns its proof status)
hence query check completed-smoke-test plan.spl

# List all tasks assigned to the current agent
HENCE_AGENT=alice hence task list plan.spl

The four proof states

Every conclusion in hence has one of four proof statuses, borrowed from the formal semantics of defeasible logic as defined by Governatori, Maher, Antoniou, and Billington. Understanding these states helps you interpret query output and reason about plan correctness.

In everyday use, the distinction that matters most is between +d (the thing is happening — a task is assigned, is ready, is complete) and -d (the thing is not happening — a task is not ready, not assigned, not complete). The +D / -D split tells you whether the strict-logic part of the program is involved, which is relevant for debugging but less important for routine agent operation.

Reading status in command output

Most hence output commands prefix conclusions with their proof status:

; hence plan board plan.spl — example output
+D  task-smoke-test              ; exists (given)
+d  ready-smoke-test             ; no deps, default ready rule fired
+d  assigned-smoke-test-to-qa    ; assignment rule fired
+d  claimed-smoke-test           ; claimed by qa (from claims block)
+d  completed-smoke-test         ; qa asserted completion

+D  task-deploy-canary           ; exists (given)
-d  ready-deploy-canary          ; blocked: db-backup not yet complete
-d  assigned-deploy-canary-to-ops ; no assignment until ready

Proof status and the open-world assumption, revisited

The four states make the open-world assumption concrete. Consider a fact like completed-db-backup:

• If a claims block asserts it: status is +d — the agent says it's done, and nothing defeats that claim.
• If no claims block mentions it, and no rule concludes it: status is -D and -d — there is no proof at any level. Not false; just unknown.
• If a rule explicitly concludes ~completed-db-backup (its negation) and nothing defeats that rule: the negation is +d, meaning the reasoner has a positive reason to believe the task is not complete.

This matters when writing readiness rules that depend on upstream completion: a task remains blocked until the completion fact actually appears in the plan, not merely because the fact is absent. The default blocking rule fires on the dependency fact; the unblocking rule fires when completion is proven.

Putting it all together

Here is a complete, annotated plan showing how all the concepts interact. Two agents — a QA agent and an ops agent — coordinate a deployment using hence.

; deploy-v3.spl — complete annotated plan

; ── Plan metadata ───────────────────────────────────────────────────
(meta plan-name "Deploy service v3.0")
(meta plan-version "2")

; ── Tasks ───────────────────────────────────────────────────────────
(given task-run-tests)
(given task-build-image)
(given task-push-image)
(given task-deploy-staging)
(given task-approve-staging)
(given task-deploy-prod)

; ── Dependencies ────────────────────────────────────────────────────
(given depends-build-image-on-run-tests)
(given depends-push-image-on-build-image)
(given depends-deploy-staging-on-push-image)
(given depends-approve-staging-on-deploy-staging)
(given depends-deploy-prod-on-approve-staging)

; ── Readiness rules ─────────────────────────────────────────────────

; A task with no dependencies is ready immediately
(normally r-ready-no-deps
  (task-NAME)
  (ready-NAME))

; A dependency blocks readiness by default
(normally r-dep-blocks
  (depends-NAME-on-DEP)
  (~ready-NAME))

; A completed dependency unblocks the dependant
(normally r-dep-done-unblocks
  (depends-NAME-on-DEP completed-DEP)
  (ready-NAME))

; Specific unblocking beats general blocking
(prefer r-dep-done-unblocks r-dep-blocks)

; ── Assignment rules ────────────────────────────────────────────────
(normally r-qa-tests
  (task-run-tests ready-run-tests)
  (assigned-run-tests-to-qa))

(normally r-ops-build
  (task-build-image ready-build-image)
  (assigned-build-image-to-ops))

(normally r-ops-push
  (task-push-image ready-push-image)
  (assigned-push-image-to-ops))

(normally r-ops-staging
  (task-deploy-staging ready-deploy-staging)
  (assigned-deploy-staging-to-ops))

(normally r-qa-approve
  (task-approve-staging ready-approve-staging)
  (assigned-approve-staging-to-qa))

(normally r-ops-prod
  (task-deploy-prod ready-deploy-prod)
  (assigned-deploy-prod-to-ops))

; ── Findings appended by agents ──────────────────────────────────────

(claims agent:qa
  :at "2026-02-24T08:00:00Z"
  (given completed-run-tests)
  (given finding-tests-passed-312-of-312))

(claims agent:ops
  :at "2026-02-24T08:30:00Z"
  (given completed-build-image)
  (given finding-image-digest-sha256:aabbcc))

(claims agent:ops
  :at "2026-02-24T08:45:00Z"
  (given completed-push-image)
  (given finding-image-tag-v3.0.0))

At this point in the plan's history, deploy-staging is ready and assigned to ops, while approve-staging and deploy-prod are still blocked. Running HENCE_AGENT=ops hence task next deploy-v3.spl would return task-deploy-staging.

Next steps

You now have the conceptual foundation for working with hence. The remaining documentation covers practical application of these ideas: