elephant · agents talking in logical sentences

Shared state with a memory for commitments.

Elephant gives people and agents a shared logical theory of facts, rules, and signed promises. Conclusions explain themselves. Commitments become fulfilled or violated from the evidence. The whole history syncs peer-to-peer, end-to-end encrypted.

Install elephant → See a promise kept

v0.1.8 · 21 September 2026 Defeasible logic · signed speech acts CRDT state · MLS encryption · peer-to-peer sync Apache-2.0 · experimental

commitment / s-ba25bccbverified

promised outcome

legal-signed

promisedprovenfulfilled

debtoragent:840a1d78…

deadline2036-01-01T00:00Z

signed statementderived state · not a mutable field

New in v0.1.8

Reason about quantities, time, and trust.

Spindle v0.4 brings arithmetic, aggregation, temporal reasoning, and trust diminishment into Elephant's signed theories. Shared lookup functions and named aggregators travel with the encrypted theory, so peers can use the same extensions.

Calculate from evidence

Sum purchases, count observations, or derive minimum and maximum values. Arithmetic and integer or symbol aggregation let rules reason over the data in your theory.

Inspect typed conclusions

reason --v2 --json preserves argument types, all four proof tags, modality, negation, and temporal bounds. capabilities --json lists the reasoning interfaces and supported fragments.

See how trust changes

reason --trust and status --trust expose source identities, diminished trust degrees, threshold results, and the defeaters responsible.

Share reasoning extensions

extensions set and extensions show manage signed lookup functions and named aggregators replicated through encrypted theory sync.

Explore missing evidence

require verifies candidate fact sets; abduce exposes raw, unverified candidates. These searches are bounded. Hypothetical facts enter before grounding and aggregation, so new bindings and totals are considered.

Discover available work

next -t release --json, introduced in v0.1.7, finds documented, ready tasks with readiness provenance and no outstanding completion promise. Inspect the evidence, then promise the outcome.

Release v0.1.8 → Read the reasoning guide

The problem

Our software makes commitments. Its databases only remember fields.

Agents approve releases, accept work, report evidence, and promise outcomes. Most systems reduce those acts to mutable rows and application code. When the world changes, the explanation for a decision—and who undertook what—disappears.

Ordinary coordination state

Statuses are assigned by application code, so “fulfilled” means a field was set—not that the promised outcome is actually proven.

Rules hide in services where people and agents cannot query why a gate is closed or what evidence would open it.

Shared words drift silently. One agent writes build-ok; another waits forever for ci-green.

What elephant records

Promises are signed objects with a goal, author, and deadline. Their state is a conclusion about the theory, not an editable label.

Rules live beside facts in one logical corpus. Ask why-not, require, or explain and get an inspectable answer.

Vocabulary is visible as part of the theory. Orphaned names and missing predicates surface before they become coordination failures.

A release gate, end to end

Ask what is missing. Make a promise. Prove it was kept.

These commands follow the worked example in Elephant's release. Pick a step to see how one shared theory moves from evidence to an explained decision.

elephant · release theory

$ elephant id create --name alice
created identity
did:crdt:840a1d78223afbfc6d6eda0540a17cfbdb00af2b694e3b857244b73898a5a4d1
agent:alice

$ elephant theory create release
created theory release
id  0bcddfc507ebe6f3adf11ea72d0d269ee9680071511349f5027cb2141ad4c239

# One theory: facts, rules, vocabulary, promises, and provenance.
# Every authored statement carries its signer.

$ elephant assert 'qa-signed' -t release
assert  s-8d4c68355d956faa

$ elephant assert \
  '(normally r-ready
     (and qa-signed legal-signed docs-ready)
     release-ready)' -t release
assert  s-84346ab76b76f98e

$ elephant status -t release
 -D  docs-ready
 -D  legal-signed
 +D  qa-signed
 -D  release-ready

$ elephant why-not release-ready -t release
rule r-ready: Missing premises: legal-signed, docs-ready

$ elephant require release-ready -t release
provable if all added:
  docs-ready  legal-signed

# "why-not" explains the failure.
# "require" runs backwards to find the minimal sufficient facts.
# No one has to reverse-engineer the gate from application code.

$ elephant promise 'legal-signed' \
  --by 2036-01-01T00:00:00Z -t release
commit  s-ba25bccb08018723

$ elephant commitments -t release
outstanding  s-ba25bccb08018723
  agent:840a1d78… → legal-signed
  by 2036-01-01T00:00:00Z

# Outstanding is derived: the commitment exists, its goal is
# not yet proven, it was not revoked, and its deadline remains ahead.

$ elephant assert 'legal-signed' -t release
$ elephant assert 'docs-ready' -t release

$ elephant status -t release
 +D  docs-ready
 +D  legal-signed
 +D  qa-signed
 +d  release-ready

$ elephant commitments -t release
fulfilled  s-ba25bccb08018723
  agent:840a1d78… → legal-signed
  by 2036-01-01T00:00:00Z

# +d means release-ready was derived defeasibly.
# Fulfilment follows from proof of the promised outcome.

What changed after hence

Reasoning is only useful when the state, the promises, and the words hold together.

01 · Shared state

A theory that travels.

Elephant replaces local coordination files with CRDT-backed theories that peers can join and sync directly. History is encrypted before it leaves the machine.

One Loro document per theory
End-to-end encryption with MLS
Peer discovery over pkarr / Mainline DHT
QUIC transport through iroh
Assertions can be retracted cleanly

02 · Commitment semantics

A promise has consequences.

A promise is part of the signed corpus. Elephant determines whether it is outstanding, fulfilled, violated, or revoked from the theory and an explicit evaluation time.

Signed author and promised content
Explicit deadline
Fulfilment derived from proof
Violations remain attributable
No hidden system-clock dependency

03 · Live vocabulary

The theory defines its words.

Predicate families—such as ci-green/1—can carry descriptions, argument types, kinds, and expected asserters. Diagnostics reveal vocabulary drift without forbidding new language.

Named, parameterised predicates
Signed definitions sync with the theory
Orphans: asserted but unused
Holes: expected but never proven
Advisory warnings, never quarantine

Commitment lifecycle

No one sets a promise to “done.” The theory concludes what happened.

Elephant evaluates the same signed history at a supplied point in time. That keeps reasoning deterministic and makes past or future states inspectable.

signed

An agent authors a goal and deadline.

→

outstanding

The goal is not proven; time remains.

→

fulfilled

The promised sentence is now provable.

violated

The deadline passed without proof.

Fulfilment is monotone in the corpus.

Once evidence proves the goal, simply advancing evaluation time cannot make the promise un-fulfil itself.

Violation is an accountable conclusion.

The unproven goal, expired deadline, and signing agent remain together in the record. An elephant never forgets.

How it works

A sealed corpus around a pure reasoning core.

Elephant verifies and opens signed statements, derives the closure of the corpus at a chosen time, and closes results back into the shared theory. Networking and cryptography stay outside the reasoner's pure core.

┌────────────── elephant ────────────────────┐ │ CLI (clap) daemon (loopback API) │ │ │ │ │ │ ▼ ▼ │ │ ┌───────────────────────────────────┐ │ │ │ theory store — one LoroDoc/theory │ │ │ │ sealed append-only corpus (MLS) │ │ │ └───────────────┬───────────────────┘ │ │ │ verify → open → close │ │ ┌───────────────▼───────────────────┐ │ │ │ PURE CORE closure(corpus,trust,t)│ │ │ │ envelope · tombstone · commitments│ │ │ └──┬────────┬────────┬────────┬─────┘ │ └─────┼────────┼────────┼────────┼───────────┘ ┌────▼──┐ ┌───▼────┐ ┌─▼──────┐ ┌▼───────┐ │cbcl-rs│ │spindle-│ │did-crdt│ │ openmls│ │dialect│ │rust SPL│ │identity│ │ MLS │ └───────┘ └────────┘ └────────┘ └────────┘ transport: iroh QUIC + pkarr/Mainline-DHT join: SPAKE2

Defeasible, not brittle

Strict rules, normal rules, exceptions, and priorities let a theory absorb new or contradictory information without collapsing.

Every conclusion has provenance

explain shows the facts and rules behind a result; why-not shows which premises are absent.

Identity is part of the statement

did:crdt identities sign assertions, definitions, and promises, preserving authorship as theories sync.

Time is an input

The reasoner receives evaluation time as a parameter. Re-run history at any moment without an implicit call to the wall clock.

Vocabulary stays open

Definitions guide shared meaning, while new predicates remain legal. Elephant diagnoses mismatch rather than appointing a schema police.

The terminal is only one client

The CLI talks to a loopback daemon; the theory store and pure core provide the substrate for other interfaces.

Joining a theory

Share a phrase. Never share the key.

Alice creates a one-time invitation and communicates the short phrase out of band. SPAKE2 proves both peers know it without transmitting it. After confirmation, Bob joins the MLS group and receives the encrypted history.

The phrase is entered on the TTY, never command history or process arguments.
Rendezvous uses a derived pkarr record on the BitTorrent Mainline DHT.
A wrong guess fails opaquely and burns the one-time invitation.
No key material crosses the wire.

Alice · invite

$ elephant theory invite release

7842-walnut-harbor

↓ out of band ↓

Bob · join

$ elephant theory join --alias release
Enter invite code at the prompt.

result

joined · history verified · MLS epoch current

Questions

Frequently asked questions.

Is elephant a database?

It stores and syncs state, but the useful abstraction is a logical theory. You add signed facts, rules, predicate definitions, retractions, and promises; Elephant derives conclusions over that corpus and can explain how it reached them.

How is elephant different from hence?

Hence applies defeasible reasoning to multi-agent task coordination. Elephant is its more general successor: theories sync peer-to-peer on CRDTs, commitments follow promise semantics, and predicate vocabulary can be defined at runtime for any domain.

Does a promise make its goal true?

No. A promise records an agent's commitment to make a sentence provable. It remains outstanding until evidence establishes that goal; it becomes violated if the supplied evaluation time passes the deadline first.

What happens when agents use different names for the same thing?

elephant vocab identifies orphans—predicates asserted but never consumed—and holes—predicates rules expect but nobody proves. Definitions add documentation and expected asserters. The diagnostics are advisory: Elephant warns about vocabulary drift without rejecting new words.

Is there a central server?

Theories sync directly between peers over iroh QUIC. Peer discovery uses pkarr and the Mainline DHT; a local daemon provides the loopback API. Shared history is protected with Message Layer Security. For continuous updates, run the daemon on each peer with ELEPHANT_SYNC_INTERVAL=30; an unset or zero interval disables continuous sync.

Is it production-ready?

Elephant is early, experimental software. It is available to install and inspect today, but adopters should evaluate it accordingly. The source is open under Apache-2.0.