diff --git a/README.md b/README.md
index 7d962dd..a947ccd 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,33 @@
-# coq-hyperproperty-lib
-A hyperproperty library written in Coq.
+# Coq Hyperproperty Library
+
+This repo contains a hyperproperty library written in Coq.
+
+As of 2023-12-12, work on this library is still ongoing, and we expect
+significant changes to the interface to occur.
+
+## Library Layout
+
+This library consists of core hyperproperty definitions and proofs
+(`Hyperproperties.v`), two example hyperproperties and proofs
+(`GuaranteedService.v` and `ObservationalDeterminism.v`), and an example system
+(`CrashSystem.v`).
+
+## Build Instructions
+
+This code was built with Coq version 8.17.1. To build this library, clone the
+repo and run:
+
+```
+make
+```
+
+This should verify all proofs in all files.
+
+## Known Issues
+
+A small number of lemmas outside of the `Hyperproperties.v` file are not yet
+completed. Note that all proofs inside the `Hyperproperties.v` file are
+complete.
+
+This library currently uses classical logic and assumes the excluded middle for
+some proofs. Future work aims to remove this dependency.