Vertep

The author

Volodymyr Pavlyshyn

I write software for memory: how agents and people keep what they know, in graphs that can be queried, dated, verified and trusted. Engineering since 2002. Vertep is where I take the same idea to behaviour: a program whose every step is allowed by a chart and written down.

What I work on

My focus is memory for agents and humans: knowledge graphs, retrieval, temporal and verifiable data, and agent identity and trust. I have twice been a founding engineer: at Affinidi, on self-sovereign identity, and at Mykin, on a privacy-first personal AI with on-device memory. Since 2026 I work as an independent researcher and open-source author.

I work by five verbs: do, validate, iterate, learn, teach. Vertep follows them closely: the chart is the validation, the journal is the iteration, and the Lean model is the lesson I could not skip.

Where Vertep fits

Vertep started from a question the books keep asking: where does a language model belong in a program? My answer is at a choice point, picking among moves a chart offers, with each answer journaled. The proofs that keep the Rust runtime honest are written in Lean 4, and the larger body of Lean work lives on Lean 4 Knowledge, a site about graph engineering, logic and certified reasoning. It carries the open-source projects lean-elpi, LeanRDF, typedb-lean and ladybug-lean, and a neuro-symbolic series of three books: The Little Elpier, Logic for Agents and Bulletproof Knowledge.

Read next: The goat does not choose the play, and how the Lean proofs and the Rust runtime are tied together.

Career

I studied system engineering at Lviv Polytechnic National University (bachelor 2006, master 2008, both with honours). I speak Ukrainian, English, German, Polish and Russian. The full record is on the CV page.

Books and research

I have published eighteen books, mostly on Leanpub, with one more in progress. They cover agent memory, knowledge graphs, temporal graphs, metagraphs, world models, edge AI, graph databases and engineering practice. Among them: AI Agents Memory Empowered by Knowledge Graphs, Metagraph for AI Agents, Temporal Aware AI Memory, Dependent Types & Logic for AI Agent Ready Knowledge Graphs and Rusty Graphs. The whole list is at pavlyshyn.me/books. Independent papers, including Metagraph Encodings over Identified Triples and Layered Bitemporal Graphs, are listed at pavlyshyn.me/papers.

Find me elsewhere

Legal notices for this site: Impressum · Datenschutz · AGB.