diff --git a/Makefile b/Makefile
index 77cf63c2..ad909e53 100644
--- a/Makefile
+++ b/Makefile
@@ -1,24 +1,16 @@
-default: Makefile.coq
-	$(MAKE) -f Makefile.coq
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
 
-quick: Makefile.coq
-	$(MAKE) -f Makefile.coq quick
-
-install: Makefile.coq
-	$(MAKE) -f Makefile.coq install
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
-
-clean: Makefile.coq
-	$(MAKE) -f Makefile.coq cleanall
-	rm -f Makefile.coq Makefile.coq.conf
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-lint:
-	@echo "Possible use of hypothesis names:"
-	find . -name '*.v' -exec grep -Hn 'H[0-9][0-9]*' {} \;
+force _CoqProject Makefile: ;
 
-distclean: clean
-	rm -f _CoqProject
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
 
-.PHONY: default quick clean lint distclean install
+.PHONY: all clean force
diff --git a/_CoqProject b/_CoqProject
index 5bb4eec4..91d40f5d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,48 +1,45 @@
--Q core Verdi
--Q lib Verdi
--Q systems Verdi
--Q extraction Verdi
+-Q theories Verdi
 
-core/NameOverlay.v
-core/DynamicNetLemmas.v
-core/Net.v
-core/HandlerMonad.v
-core/Verdi.v
-core/StateMachineHandlerMonad.v
-core/InverseTraceRelations.v
-core/SingleSimulations.v
-core/PartialMapSimulations.v
-core/TotalMapExecutionSimulations.v
-core/VerdiHints.v
-core/DupDropReordering.v
-core/PartialMapExecutionSimulations.v
-core/GhostSimulations.v
-core/StatePacketPacketDecomposition.v
-core/TraceRelations.v
-core/LabeledNet.v
-core/TotalMapSimulations.v
-core/PartialExtendedMapSimulations.v
+theories/Core/NameOverlay.v
+theories/Core/DynamicNetLemmas.v
+theories/Core/Net.v
+theories/Core/HandlerMonad.v
+theories/Core/Verdi.v
+theories/Core/StateMachineHandlerMonad.v
+theories/Core/InverseTraceRelations.v
+theories/Core/SingleSimulations.v
+theories/Core/PartialMapSimulations.v
+theories/Core/TotalMapExecutionSimulations.v
+theories/Core/VerdiHints.v
+theories/Core/DupDropReordering.v
+theories/Core/PartialMapExecutionSimulations.v
+theories/Core/GhostSimulations.v
+theories/Core/StatePacketPacketDecomposition.v
+theories/Core/TraceRelations.v
+theories/Core/LabeledNet.v
+theories/Core/TotalMapSimulations.v
+theories/Core/PartialExtendedMapSimulations.v
 
-lib/Ssrexport.v
-lib/FMapVeryWeak.v
+theories/Lib/Ssrexport.v
+theories/Lib/FMapVeryWeak.v
 
-systems/Counter.v
-systems/SerializedMsgParams.v
-systems/PrimaryBackup.v
-systems/SerializedMsgParamsCorrect.v
-systems/LockServSeqNum.v
-systems/VarDPrimaryBackup.v
-systems/VarD.v
-systems/SeqNum.v
-systems/LiveLockServ.v
-systems/SeqNumCorrect.v
-systems/LockServ.v
-systems/Log.v
-systems/LogCorrect.v
+theories/Systems/Counter.v
+theories/Systems/SerializedMsgParams.v
+theories/Systems/PrimaryBackup.v
+theories/Systems/SerializedMsgParamsCorrect.v
+theories/Systems/LockServSeqNum.v
+theories/Systems/VarDPrimaryBackup.v
+theories/Systems/VarD.v
+theories/Systems/SeqNum.v
+theories/Systems/LiveLockServ.v
+theories/Systems/SeqNumCorrect.v
+theories/Systems/LockServ.v
+theories/Systems/Log.v
+theories/Systems/LogCorrect.v
 
-extraction/ExtrOcamlFinInt.v
-extraction/ExtrOcamlNatIntExt.v
-extraction/ExtrOcamlDiskOp.v
-extraction/ExtrOcamlBasicExt.v
-extraction/ExtrOcamlBool.v
-extraction/ExtrOcamlList.v
+theories/Extraction/ExtrOcamlFinInt.v
+theories/Extraction/ExtrOcamlNatIntExt.v
+theories/Extraction/ExtrOcamlDiskOp.v
+theories/Extraction/ExtrOcamlBasicExt.v
+theories/Extraction/ExtrOcamlBool.v
+theories/Extraction/ExtrOcamlList.v
diff --git a/dune-project b/dune-project
new file mode 100644
index 00000000..1182f1f2
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.5)
+(using coq 0.6)
+(name verdi)
diff --git a/script/checkpaths.sh b/script/checkpaths.sh
deleted file mode 100755
index b6e5e2f1..00000000
--- a/script/checkpaths.sh
+++ /dev/null
@@ -1,39 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-if ! [ -f _CoqProject ]; then
-    exit 0
-fi
-
-if [ "${TRAVIS}x" != "x" ]; then
-    exit 0
-fi
-
-
-grep '\.v' _CoqProject | sort > build.files
-find . -name '*.v' | sed 's!^\./!!' | sort > files
-
-comm -23 files build.files > files.missing.from.build
-comm -13 files build.files > nonexistant.build.files
-
-EXIT_CODE=0
-
-if [ -s files.missing.from.build ]
-then
-    echo 'The following files are present but missing from Makefile.coq.'
-    echo 'Perhaps you have added a new file and should rerun ./configure?'
-    cat files.missing.from.build
-    EXIT_CODE=1
-fi
-
-if [ -s nonexistant.build.files ]
-then
-    echo 'The following files are present in Makefile.coq but to not exist.'
-    echo 'Perhaps you have deleted a file and should rerun ./configure?'
-    cat nonexistant.build.files
-    EXIT_CODE=1
-fi
-
-rm -f files build.files files.missing.from.build nonexistant.build.files
-exit $EXIT_CODE
diff --git a/script/coqproject.sh b/script/coqproject.sh
deleted file mode 100755
index 0b834bb6..00000000
--- a/script/coqproject.sh
+++ /dev/null
@@ -1,89 +0,0 @@
-#!/usr/bin/env bash
-
-### coqproject.sh
-### Creates a _CoqProject file, including external dependencies.
-
-### See the README.md file for a description.
-
-## Implementation
-
-if [ -z ${DIRS+x} ]; then DIRS=(.); fi
-
-COQPROJECT_TMP=_CoqProject.tmp
-
-rm -f $COQPROJECT_TMP
-touch $COQPROJECT_TMP
-
-function dep_dirs_lines(){
-  dep_dirs_var="$2"_DIRS
-  local -a 'dep_dirs=("${'"$dep_dirs_var"'[@]}")'
-  if [ "x${dep_dirs[0]}" = "x" ]; then dep_dirs=(.); fi
-  for dep_dir in "${dep_dirs[@]}"; do
-      namespace_var=NAMESPACE_"$2"_"$dep_dir"
-      namespace_var=${namespace_var//\//_}
-      namespace_var=${namespace_var//-/_}
-      namespace_var=${namespace_var//./_}
-      namespace=${!namespace_var:=$2}
-      if [ $dep_dir = "." ]; then
-        LINE="-Q $1 $namespace"
-      else
-        LINE="-Q $1/$dep_dir $namespace"
-      fi
-      echo $LINE >> $COQPROJECT_TMP
-  done
-}
-for dep in ${DEPS[@]}; do
-    path_var="$dep"_PATH
-    if [ ! "x${!path_var}" = "x" ]; then
-	path=${!path_var}
-	if [ ! -d "$path" ]; then
-            echo "$dep not found at $path."
-            exit 1
-	fi
-
-	pushd "$path" > /dev/null
-	path=$(pwd)
-	popd > /dev/null
-	echo "$dep found at $path"
-
-	dep_dirs_lines $path $dep
-    fi
-done
-
-COQTOP="coqtop $(cat $COQPROJECT_TMP)"
-function check_canary(){
-    echo "Require Import $@." | $COQTOP 2>&1 | grep -i error 1> /dev/null 2>&1 
-}
-i=0
-len="${#CANARIES[@]}"
-while [ $i -lt $len ]; do
-    if check_canary ${CANARIES[$i]}; then
-        echo "Error: ${CANARIES[$((i + 1))]}"
-        exit 1
-    fi
-    let "i+=2"
-done
-
-for dir in ${DIRS[@]}; do
-    namespace_var=NAMESPACE_"$dir"
-    namespace_var=${namespace_var//\//_}
-    namespace_var=${namespace_var//-/_}
-    namespace_var=${namespace_var//./_}
-    namespace=${!namespace_var:="''"}
-    LINE="-Q $dir $namespace"
-    echo $LINE >> $COQPROJECT_TMP
-done
-
-for dir in ${DIRS[@]}; do
-    echo >> $COQPROJECT_TMP
-    find $dir -iname '*.v' -not -name '*\#*'  >> $COQPROJECT_TMP
-done
-
-for extra in ${EXTRA[@]}; do
-    if ! grep --quiet "^$extra\$" $COQPROJECT_TMP; then
-        echo >> $COQPROJECT_TMP
-        echo $extra >> $COQPROJECT_TMP
-    fi
-done
-
-mv $COQPROJECT_TMP _CoqProject
diff --git a/core/DupDropReordering.v b/theories/Core/DupDropReordering.v
similarity index 100%
rename from core/DupDropReordering.v
rename to theories/Core/DupDropReordering.v
diff --git a/core/DynamicNetLemmas.v b/theories/Core/DynamicNetLemmas.v
similarity index 100%
rename from core/DynamicNetLemmas.v
rename to theories/Core/DynamicNetLemmas.v
diff --git a/core/GhostSimulations.v b/theories/Core/GhostSimulations.v
similarity index 100%
rename from core/GhostSimulations.v
rename to theories/Core/GhostSimulations.v
diff --git a/core/HandlerMonad.v b/theories/Core/HandlerMonad.v
similarity index 100%
rename from core/HandlerMonad.v
rename to theories/Core/HandlerMonad.v
diff --git a/core/InverseTraceRelations.v b/theories/Core/InverseTraceRelations.v
similarity index 100%
rename from core/InverseTraceRelations.v
rename to theories/Core/InverseTraceRelations.v
diff --git a/core/LabeledNet.v b/theories/Core/LabeledNet.v
similarity index 100%
rename from core/LabeledNet.v
rename to theories/Core/LabeledNet.v
diff --git a/core/NameOverlay.v b/theories/Core/NameOverlay.v
similarity index 100%
rename from core/NameOverlay.v
rename to theories/Core/NameOverlay.v
diff --git a/core/Net.v b/theories/Core/Net.v
similarity index 100%
rename from core/Net.v
rename to theories/Core/Net.v
diff --git a/core/PartialExtendedMapSimulations.v b/theories/Core/PartialExtendedMapSimulations.v
similarity index 100%
rename from core/PartialExtendedMapSimulations.v
rename to theories/Core/PartialExtendedMapSimulations.v
diff --git a/core/PartialMapExecutionSimulations.v b/theories/Core/PartialMapExecutionSimulations.v
similarity index 100%
rename from core/PartialMapExecutionSimulations.v
rename to theories/Core/PartialMapExecutionSimulations.v
diff --git a/core/PartialMapSimulations.v b/theories/Core/PartialMapSimulations.v
similarity index 100%
rename from core/PartialMapSimulations.v
rename to theories/Core/PartialMapSimulations.v
diff --git a/core/SingleSimulations.v b/theories/Core/SingleSimulations.v
similarity index 100%
rename from core/SingleSimulations.v
rename to theories/Core/SingleSimulations.v
diff --git a/core/StateMachineHandlerMonad.v b/theories/Core/StateMachineHandlerMonad.v
similarity index 100%
rename from core/StateMachineHandlerMonad.v
rename to theories/Core/StateMachineHandlerMonad.v
diff --git a/core/StatePacketPacketDecomposition.v b/theories/Core/StatePacketPacketDecomposition.v
similarity index 100%
rename from core/StatePacketPacketDecomposition.v
rename to theories/Core/StatePacketPacketDecomposition.v
diff --git a/core/TotalMapExecutionSimulations.v b/theories/Core/TotalMapExecutionSimulations.v
similarity index 100%
rename from core/TotalMapExecutionSimulations.v
rename to theories/Core/TotalMapExecutionSimulations.v
diff --git a/core/TotalMapSimulations.v b/theories/Core/TotalMapSimulations.v
similarity index 100%
rename from core/TotalMapSimulations.v
rename to theories/Core/TotalMapSimulations.v
diff --git a/core/TraceRelations.v b/theories/Core/TraceRelations.v
similarity index 100%
rename from core/TraceRelations.v
rename to theories/Core/TraceRelations.v
diff --git a/core/Verdi.v b/theories/Core/Verdi.v
similarity index 100%
rename from core/Verdi.v
rename to theories/Core/Verdi.v
diff --git a/core/VerdiHints.v b/theories/Core/VerdiHints.v
similarity index 100%
rename from core/VerdiHints.v
rename to theories/Core/VerdiHints.v
diff --git a/extraction/ExtrOcamlBasicExt.v b/theories/Extraction/ExtrOcamlBasicExt.v
similarity index 100%
rename from extraction/ExtrOcamlBasicExt.v
rename to theories/Extraction/ExtrOcamlBasicExt.v
diff --git a/extraction/ExtrOcamlBool.v b/theories/Extraction/ExtrOcamlBool.v
similarity index 100%
rename from extraction/ExtrOcamlBool.v
rename to theories/Extraction/ExtrOcamlBool.v
diff --git a/extraction/ExtrOcamlDiskOp.v b/theories/Extraction/ExtrOcamlDiskOp.v
similarity index 100%
rename from extraction/ExtrOcamlDiskOp.v
rename to theories/Extraction/ExtrOcamlDiskOp.v
diff --git a/extraction/ExtrOcamlFinInt.v b/theories/Extraction/ExtrOcamlFinInt.v
similarity index 100%
rename from extraction/ExtrOcamlFinInt.v
rename to theories/Extraction/ExtrOcamlFinInt.v
diff --git a/extraction/ExtrOcamlList.v b/theories/Extraction/ExtrOcamlList.v
similarity index 100%
rename from extraction/ExtrOcamlList.v
rename to theories/Extraction/ExtrOcamlList.v
diff --git a/extraction/ExtrOcamlNatIntExt.v b/theories/Extraction/ExtrOcamlNatIntExt.v
similarity index 100%
rename from extraction/ExtrOcamlNatIntExt.v
rename to theories/Extraction/ExtrOcamlNatIntExt.v
diff --git a/lib/FMapVeryWeak.v b/theories/Lib/FMapVeryWeak.v
similarity index 100%
rename from lib/FMapVeryWeak.v
rename to theories/Lib/FMapVeryWeak.v
diff --git a/lib/Ssrexport.v b/theories/Lib/Ssrexport.v
similarity index 100%
rename from lib/Ssrexport.v
rename to theories/Lib/Ssrexport.v
diff --git a/systems/Counter.v b/theories/Systems/Counter.v
similarity index 100%
rename from systems/Counter.v
rename to theories/Systems/Counter.v
diff --git a/systems/LiveLockServ.v b/theories/Systems/LiveLockServ.v
similarity index 100%
rename from systems/LiveLockServ.v
rename to theories/Systems/LiveLockServ.v
diff --git a/systems/LockServ.v b/theories/Systems/LockServ.v
similarity index 100%
rename from systems/LockServ.v
rename to theories/Systems/LockServ.v
diff --git a/systems/LockServSeqNum.v b/theories/Systems/LockServSeqNum.v
similarity index 100%
rename from systems/LockServSeqNum.v
rename to theories/Systems/LockServSeqNum.v
diff --git a/systems/Log.v b/theories/Systems/Log.v
similarity index 100%
rename from systems/Log.v
rename to theories/Systems/Log.v
diff --git a/systems/LogCorrect.v b/theories/Systems/LogCorrect.v
similarity index 100%
rename from systems/LogCorrect.v
rename to theories/Systems/LogCorrect.v
diff --git a/systems/PrimaryBackup.v b/theories/Systems/PrimaryBackup.v
similarity index 100%
rename from systems/PrimaryBackup.v
rename to theories/Systems/PrimaryBackup.v
diff --git a/systems/SeqNum.v b/theories/Systems/SeqNum.v
similarity index 100%
rename from systems/SeqNum.v
rename to theories/Systems/SeqNum.v
diff --git a/systems/SeqNumCorrect.v b/theories/Systems/SeqNumCorrect.v
similarity index 100%
rename from systems/SeqNumCorrect.v
rename to theories/Systems/SeqNumCorrect.v
diff --git a/systems/SerializedMsgParams.v b/theories/Systems/SerializedMsgParams.v
similarity index 100%
rename from systems/SerializedMsgParams.v
rename to theories/Systems/SerializedMsgParams.v
diff --git a/systems/SerializedMsgParamsCorrect.v b/theories/Systems/SerializedMsgParamsCorrect.v
similarity index 100%
rename from systems/SerializedMsgParamsCorrect.v
rename to theories/Systems/SerializedMsgParamsCorrect.v
diff --git a/systems/VarD.v b/theories/Systems/VarD.v
similarity index 100%
rename from systems/VarD.v
rename to theories/Systems/VarD.v
diff --git a/systems/VarDPrimaryBackup.v b/theories/Systems/VarDPrimaryBackup.v
similarity index 100%
rename from systems/VarDPrimaryBackup.v
rename to theories/Systems/VarDPrimaryBackup.v
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 00000000..0ad1482b
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name Verdi)
+ (package coq-verdi)
+ (synopsis "Framework for verification of implementations of distributed systems in Coq"))
+
+(include_subdirs qualified)