delhi is an epistemic model checker. It represents what each agent knows and believes, keeps it straight through announcements, sensing and actions that some agents witness and others miss — and lets you ask what happens when someone's picture of another person goes stale.
Rust, MIT/Apache-2.0. A single self-contained binary — no runtime dependencies.
Most systems that reason about the world track facts. The interesting failures live one level up, in what agents think about each other.
Sally puts her marble in the basket and leaves. Anne moves it to the box. Sally comes back — where will she look?
The answer is the basket, and getting it right means holding two incompatible pictures at once: where the marble is, and where Sally thinks it is. A fact table cannot do that. It is also the canonical test for whether a child can represent someone else's mind, which is not a coincidence.
The conjunction below is the whole task: !basket is the world,
B[sally] basket is Sally, and neither is negotiable.
$ delhi eval sally_anne.delhi \ -a "sally_leaves()" "anne_moves()" "sally_returns()" \ -f "B[sally] basket & !basket" true
Declare agents, what is true, what is believed, and who observes what. delhi builds the model and checks it against every line you wrote.
Ask one formula, or enumerate every formula of a shape that holds —
B[alice] _ & !_ finds what an agent believes that is false.
A REPL, a browser UI with a live model graph, Graphviz output, benchmarks, and a Python wrapper for ML stacks.
Three commands to a second-order false belief.
A prebuilt binary, or from crates.io. --force is also how you update.
cargo install delhi
Alice lies about the coin, Bob distracts her, Carol peeks. Alice never sees the peek.
$ delhi eval coin_lie.delhi -a "announce_not_heads()" "distract_a()" "peek_c()" \ -f "B[alice] B[carol] !h & K[carol] h" true # alice is wrong about carol, not about the coin
A browser UI over your own folder of .delhi files — editor, live state,
model graph, console.
delhi gui
The book opens with four short chapters that assume nothing beyond and, or and not — what possible worlds are, why knowledge and belief need different machinery, what higher-order attitudes buy you, and what happens to all of it when the world changes.