AlgoStar

This repository contains verified implementations of algorithms and data structures in Pulse, a separation-logic language embedded in F*.

All the code has been produced by agents driven by prompts and feedback on specifications from humans.

AutoCLRS

This is an agent-generated implementation of algorithms and data structures from Cormen, Leiserson, Rivest, and Stein's Introduction to Algorithms (CLRS) textbook, available from MIT press.

Prerequisites

• OCaml (>= 4.14) with opam
• Z3 (>= 4.8.5) — install via opam: opam install z3 or your system package manager
• GNU Make, Git

Getting Started

1. Clone the repository with submodules

git clone --recurse-submodules git@github.com:FStarLang/AutoCLRS.git
cd AutoCLRS

If you already cloned without --recurse-submodules:

git submodule update --init --recursive

2. Build F* and Pulse

./setup.sh

This builds F* and Pulse from the pinned submodule versions. It takes 10–20 minutes on first run. You can also build them individually:

./setup.sh fstar   # build only F*
./setup.sh pulse   # build only Pulse (requires F* already built)

3. Verify all chapters

make        # verify all chapters
make -j8    # parallel build (recommended)
make clean  # clean build artifacts

Each chapter can also be verified independently:

cd autoclrs/ch02-getting-started && make

Repository Structure

Documentation

Detailed per-algorithm documentation (specification reviews, correctness properties, complexity results, and known gaps) is available in:

• Per-algorithm reviews: autoclrs/<chapter>/<Module>.Review.md files
• Chapter READMEs: autoclrs/<chapter>/README.md