The mini book

1Graphs that remember

A labeled property graph stores things as nodes and the ways they relate as relationships. Both carry a label (a type) and properties (typed fields). A relationship has a direction and joins exactly two nodes, so the connection itself can be described, queried and timestamped like anything else.

Compared with RDF triples, a property graph keeps the facts about an entity together with it and lets relationships carry their own data, which is why it suits application memory: one hop answers "who works at ACME since when".

Read more: The Property Graph Model and An Introduction to Knowledge Graphs.

2LadybugDB: a graph database inside your program

LadybugDB is an embedded property graph database built on the Kùzu engine. There is no server: you open a file (or :memory:) and you have a database that persists when the process ends. It speaks Cypher, enforces a typed schema, runs ACID transactions, and has extensions for vector search, full-text search, graph algorithms and relational sources. It is MIT licensed.

Embedded matters for agents and edge devices: the memory lives next to the code that uses it, works offline, and never leaves the machine. ladybug-lean talks to LadybugDB through its C API, which it loads at runtime, and copies every result into Lean values, so nothing in Lean ever points into native memory.

MATCH (p:Person)-[w:WorksAt]->(c:Company)
WHERE w.since >= 2020
RETURN p.name, c.name

Read more: Getting Started with LadybugDB, Why an Embedded Graph Database Matters for AI Memory and Cypher: The Graph Query Language.

3The schema is the ontology

An ontology says what kinds of things exist and how they may relate. In most systems it lives apart from the database and drifts. In LadybugDB the CREATE NODE TABLE and CREATE REL TABLE statements are the ontology, and the database enforces them when you write: a WorksAt declared from Person to Company cannot join two companies.

CREATE NODE TABLE Person(id INT64, name STRING, age INT64, PRIMARY KEY(id));
CREATE NODE TABLE Company(name STRING, PRIMARY KEY(name));
CREATE REL TABLE WorksAt(FROM Person TO Company, since INT64);

Read more: Typed Graphs and Ontologies, including polymorphic relations, and Subgraphs: Partitioning Knowledge.

4The ontology in the type checker

The database checks the ontology when you write. A query that reads a property that does not exist, compares a string with a number, or walks a relationship backwards is still accepted by your program; it fails, or quietly returns nothing, when it runs. ladybug-lean moves the ontology into Lean's type checker, so those mistakes are found when you compile.

The tables are Lean structures, and the schema is generated from them, not written twice:

structure Person where
  id   : Int64
  name : String
  age  : Option Int64

node_table Person
-- Person.Var  : the query variable; p.name : Expr String, p.age : Expr (Option Int64)
-- ddl Person  = "CREATE NODE TABLE IF NOT EXISTS Person(id INT64, name STRING, age INT64, PRIMARY KEY(id))"

Relationship patterns are checked by instance search: out p WorksAt (node Company) type-checks only because rel_table WorksAt (from := Person) (to := Company) said so. verifySchema closes the loop at runtime, reporting any difference between your declarations and the tables in a database file.

5Unknown is a value

Cypher has three truth values: true, false and unknown, which is what you get when you compare with NULL. NULL > 30 is unknown, unknown OR true is true, and WHERE keeps only true rows. Most query libraries pretend this away, and NULLs then surface as surprises when rows are decoded.

ladybug-lean puts it in the types. A nullable property is an Expr (Option τ); a comparison is an Expr (Option Bool), with none as unknown; OPTIONAL MATCH makes every property it binds nullable; and the row type of a query tells you exactly which columns can be NULL.

def withEmployer : Query (String × Option String) := query do
  let p ← match_ (node Person)
  let (_, c) ← optMatch (out p WorksAt (node Company))
  return_ (p.name, c.name)            -- c.name : Expr (Option String)

6Queries are values

A query is an ordinary Lean value: a small AST of clauses whose typed wrappers carry the result type. You can write it two ways, a monadic builder or Cypher text in cypher%, and both produce the same AST, so they print and run identically.

def viaBuilder : Query (String × String) := query do
  let p ← match_ (node Person)
  let (_, c) ← match_ (out p WorksAt (node Company))
  return_ (p.name, c.name)

def viaCypher := cypher% MATCH (p:Person)-[:WorksAt]->(c:Company) RETURN p.name, c.name

#guard viaBuilder.print == viaCypher.print

Because a query is data, it is printed to Cypher text by one function, and every Lean value in it becomes a parameter ($p0, $p1, …). A string such as "x'}) DETACH DELETE n //" is data, never part of the query, so injection is impossible by construction. The same AST is what the in-memory backend interprets.

7What "checked" means here

It is worth being precise. ladybug-lean does not prove theorems about Cypher's semantics. What it gives you is layers of checking, each mechanical:

-- pinned in a source file, checked on every build, no database needed
#guard (do applySchema schema; Repo.insert (Person.mk 1 "Ann" none);
           Repo.findAll Person : MemM _).run'.toOption.map (·.size) == some 1

8Memory for agents

An agent's memory is more than a vector store. It needs what was observed (memories with text and embeddings), about whom (entities and how they relate), and when (a timeline). A property graph holds all three, and LadybugDB answers questions that cross them in one query: the memories most similar to a thought that also mention someone the agent knows.

-- the five memories closest to a thought, if they mention Ann
let hits ← runQueryM do
  let (mem, dist) ← vectorSearch Memory "memory_vec" thought 20
  where_ (← exists_ do
    let (_, e) ← match_ (out mem Mentions (node Entity))
    where_ (e.name ==. lit "Ann"))
  orderBy dist
  limit 5
  return_ (mem.text, dist)

The example project builds a small version of this memory: entities, memories with embeddings, mentions, a timeline, and recall by similarity, by entity and by path.

Read more: From Triples to Metagraphs, Semantic Spacetime, Vector Indexes, Designing Agentic Memory and Ladybug Memory: A Working AI Memory System.