Separation-logic proofs of heap-manipulating programs require careful accounting of objects and pointers in memory. On paper, these proofs are often accompanied by heap-memory diagrams that help authors and readers track the evolution of the program’s abstract state. However, users of interactive theorem provers must instead work with plain-text notations that obscure object relationships.

In Sepviz, we imitate an intuitive diagrammatic notation commonly used in research and educational materials about separation logic, support animation across proof steps, and make it easy to port to new frameworks.

Alectryon (named after the Greek god of chicken) is a collection of tools for writing technical documents that mix Rocq code and prose, in a style sometimes called literate programming.

Rocq proofs are hard to understand in isolation: unlike pen-and-paper proofs, proof scripts only record the steps to take (induct on x, apply a theorem, …), not the states (goals) that these steps lead to. As a result, plain proof scripts are essentially incomprehensible without the assistance of an interactive interface like VSCode or Proof General.

The most common approach these days for sharing proofs with readers without forcing them to run Rocq is to manually copy Rocq's output into source code comments — a tedious, error-prone, and brittle process. Any text that accompanies the proof is also embedded in comments, making for a painful editing experience.

Alectryon does better: it automatically captures Rocq's output and interleaves it with proof scripts to produce interactive webpages, and it lets you toggle between prose- and code-oriented perspectives on the same document so that you can use your favorite text editing mode for writing prose and your favorite Rocq IDE for writing proofs.