Elephant 3000 — programs that keep their promises

21 July 2026 - Hugo O’Connor

An elephant, rendered as an abstract diagram of signed speech acts and commitments

A few months ago we released hence and have used it daily to help keep agents on track for long-running tasks using defeasible logic via spindle-rust as a coordination substrate.

Elephant 3000 is the successor to hence that adds some notable improvements in state management, commitment semantics, and vocabulary.

In 1989 John McCarthy imagined a programming language of the future called Elephant 2000.

McCarthy proposed that;

Program I/O should be meaningful speech acts (questions, answers, offers, acceptances..)
Speech acts should be logical sentences
Programs may assume obligations on behalf of their owners
Programs may have accomplishment specifications
The program is a single list of logical sentences

We couldn’t find any implementation of Elephant 2000, and so we’ve re-imagined it incoporating a swagger of great technologies.

What we learned from hence

hence gave LLM agents defeasible reasoning to plan and coordinate over long-running tasks, grounding their actions in a logical theory that could accomodate new, contradictory information as it arose.

But six months of daily use surfaced three areas to improve;

State management Hence ran on local files (or a server based coordinator), Elephant now runs on CRDTs and syncs theories peer-to-peer using a SPAKE2 pairing phrase. Theories are end-to-end encrypted using the Message Layer Security standard. Agents can now also retract assertions, rather than bloating the theory with logical retractions.
Commitment sematics Whereas hence applied a custom vocabulary for claiming tasks and application logic for leases, Elephant implements commitment / promise semantics as proposed in Elephant 2000. Agents can promise to accomplish some action in the world, committing the logical sentence to be added to the shared theory on condition of fulfilment.
Vocabulary Hence had an opinionated vocabulary focussed on task management, we’ve added named predicates to Spindle, such that an elephant theory can work in any domain of application with custom predicate vocabulary defined and shared by agent’s at runtime (and some basic built-in vocabulary).

This is early, experimental software, but you can install it today;

curl https://files.anuna.io/elephant/install.sh | sh

Walkthrough

Elephant is composed of some key libraries we maintain such as cbcl-rs, spindle-rust and did-crdt.

       ┌────────────── 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

Joining is the part I like most. Alice invites, Bob joins, and no key material crosses the wire:

# Alice
$ elephant theory invite release
  Share this one-time code:  7842-walnut-harbor

Alice communicates this phrase out of band to Bob;

# Bob (code entered on the TTY, never argv/logs)
$ elephant theory join 7842-walnut-harbor --alias release

This derives a pkarr rendezvous record on the BitTorrent Mainline DHT and the two words are a SPAKE2 password that is never transmitted and is burnt after a single wrong guess. After key confirmation Alice adds Bob to the theory’s MLS group and he pulls the whole encrypted history. A wrong code fails opaquely and leaves no partial state.

Propositional content is still SPL, the same Spindle Lisp hence used: (given …) facts, (always …) strict rules, (normally …) defeasible rules, (except …) defeaters, (prefer …) superiority. If you wrote plans before, you can read theories now.

A worked example: the release gate

Alice opens a theory about a release, states a gate rule, discovers what’s missing, and someone makes a promise. Every command below is real; the output is copied from a run of scripts/demo.sh in the repository.

Alice creates a cryptographic identity (using our did:crdt method) and a theory, then asserts one fact and one rule:

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

$ elephant theory create release
created theory release
id  0bcddfc507ebe6f3adf11ea72d0d269ee9680071511349f5027cb2141ad4c239

$ 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

Now ask the theory whether the gate is open. Note that you ask; there is no column to read.

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

Blocked. Why?

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

And run backwards — abduction — for the minimal set of facts that would open it:

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

Someone now promises to get legal sign-off, with a deadline:

$ 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

The promise is an object in the theory, signed by the agent who made it, with a deadline attached. It is outstanding — not because anyone set a field to “outstanding”, but because it arose, was not revoked, its goal is not yet proven, and its deadline has not passed.

The remaining facts land, and the gate opens:

$ 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

release-ready is +d: defeasibly provable, derived rather than declared. Ask for the derivation and you get one, with provenance:

$ elephant explain release-ready -t release
Explanation for +d release-ready
This was proven using defeasible rules and was not defeated by any conflicting rule.

Derivation:
  1. "release-ready" was derived defeasibly
     Using defeasible rule: r-ready
     Prerequisites:
       1. "qa-signed" was established as a fact
          Using fact: f1
       1. "legal-signed" was established as a fact
          Using fact: f3
       1. "docs-ready" was established as a fact
          Using fact: f4

The case of a broken promise

Evaluation time is a parameter to the reasoner rather than a call to the system clock, you can ask what the commitments look like at any moment — including after a deadline:

$ elephant promise 'docs-ready' --by 2026-08-01T00:00:00Z -t release
commit  s-19937580d5cc394b

$ elephant commitments -t release
outstanding  s-19937580d5cc394b  agent:fd66075e… → docs-ready by 2026-08-01T00:00:00Z

$ elephant commitments -t release --at 2026-09-01T00:00:00Z
violated     s-19937580d5cc394b  agent:fd66075e… → docs-ready by 2026-08-01T00:00:00Z
(1 violated — an elephant never forgets)

Nobody wrote that violation down. It is a conclusion about history: a commitment that exists, whose goal is unproven, whose deadline is behind us. The agent that made it is named in the record, and the record is signed.

That is Elephant 2000’s specification-by-promise-keeping, running in a terminal. And the state machine is monotone in the corpus rather than in wall-clock time — a fulfilled promise cannot un-fulfil itself simply because time passed.

Agreeing on the meaning of words

Sharing a theory only helps if the parties mean the same things by the same names. A CI bot asserting build-ok-m1 past a rule that listens for ci-green-m1 is a silent coordination failure: no error, no warning, just a conclusion that never fires. hence could not help here, because its vocabulary was frozen and packed arguments into flat atom names — there was no unit of meaning smaller than the whole atom to document or agree on.

So we added predicates to spindle. A parameterised literal (ci-green m1) belongs to a predicate family ci-green/1 — a functor and an arity — and the family, not the ground literal, is the thing worth documenting and agreeing on. That separation is what makes vocabulary a first-class object rather than a naming convention.

You can now define a predicate, and the definition is itself a signed statement that syncs like any other:

$ elephant define ci-green/1 --arg task:symbol \
    --desc "CI pipeline green for task ?t" --kind evidence --asserter role:ci -t release

$ elephant assert '(normally r-verified (and (ci-green ?t) (review-approved ?t)) (verified ?t))' -t release

Now watch the failure happen. The reviewer does their part, but the CI bot asserts the wrong name:

$ elephant assert '(given (review-approved m1))' -t release
$ elephant assert '(given (build-ok m1))' -t release
assert  s-5530f4425c85f0cd

Both asserts succeed. Nothing is wrong, exactly. But verified never concludes:

$ elephant status -t release
 +D  build-ok m1
 +D  review-approved m1

In hence, that is where the debugging session begins. In elephant, you ask the theory about its own vocabulary:

$ elephant vocab -t release
orphan  predicate  build-ok/1         fact       
hole    predicate  ci-green/1         body       — CI pipeline green for task ?t
active  predicate  review-approved/1  fact,body  
active  predicate  verified/1         head       — evidence a task's work is verified …  [built-in]

build-ok/1 is an orphan: asserted by somebody, listened for by nobody. ci-green/1 is a hole: rules are waiting on it and nothing proves it. An orphan and a hole of the same arity, appearing at the same moment, is a naming mismatch nearly every time — and the hole carries its own documentation, so the CI bot’s author can read what the rule actually wanted.

Vocabulary is derived from the corpus, never a pinned schema — the theory is its own ontology, where rules are the signature and meta is the documentation. And it is advisory, never enforcement: nobody is forbidden from coining a word, a near-miss produces a warning rather than a rejected assert, and nothing is ever quarantined for being newly named. The spec’s metaphor is a working group’s glossary kept inside the minute-book itself — every word in use is listed, every listed word carries its definition and its author.

McCarthy saw that once programs start talking to people and to each other, correctness has to include keeping your promises. He was imagining airline reservations. We now have millions of programs making commitments on our behalf, at a speed nobody can reliably audit.

An elephant, however, never forgets.

–

elephant is open source under Apache-2.0. spindle-rust is open source under LGPL-3.0. McCarthy, J. Elephant 2000: A Programming Language Based on Speech Acts, Stanford, 1989.