diff --git a/Makefile b/Makefile
index 76087f6..ddf5861 100644
--- a/Makefile
+++ b/Makefile
@@ -31,8 +31,8 @@ proofalytics-aux: Makefile.coq
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
 
-raft/RaftState.v: raft/RaftState.v.rec
-	$(PYTHON) script/extract_record_notation.py raft/RaftState.v.rec raft_data > raft/RaftState.v
+theories/Raft/RaftState.v: theories/Raft/RaftState.v.rec
+	$(PYTHON) script/extract_record_notation.py theories/Raft/RaftState.v.rec raft_data > theories/Raft/RaftState.v
 
 clean: Makefile.coq
 	$(MAKE) -f Makefile.coq cleanall
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 9c77009..58fd4fd 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -1,21 +1,21 @@
 include Makefile.ml-files
 
-script/assumptions.vo script/assumptions.glob script/assumptions.v.d: script/assumptions.v raft-proofs/EndToEndLinearizability.vo
+script/assumptions.vo script/assumptions.glob script/assumptions.v.d: script/assumptions.v theories/RaftProofs/EndToEndLinearizability.vo
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) script/assumptions.v
 
-$(VARDML): extraction/vard/coq/ExtractVarDRaft.v systems/VarDRaft.vo
+$(VARDML): extraction/vard/coq/ExtractVarDRaft.v theories/Systems/VarDRaft.vo
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard/coq/ExtractVarDRaft.v
 
-$(VARDSERML): extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v systems/VarDRaftSerialized.vo
+$(VARDSERML): extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v theories/Systems/VarDRaftSerialized.vo
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v
 
-$(VARDLOGML): extraction/vard-log/coq/ExtractVarDRaftLog.v systems/VarDRaftLog.vo
+$(VARDLOGML): extraction/vard-log/coq/ExtractVarDRaftLog.v theories/Systems/VarDRaftLog.vo
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-log/coq/ExtractVarDRaftLog.v
 
-$(VARDSERLOGML): extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v systems/VarDRaftSerializedLog.vo
+$(VARDSERLOGML): extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v theories/Systems/VarDRaftSerializedLog.vo
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v
 
-$(VARDDEBUGML): extraction/vard-debug/coq/ExtractVarDRaftDebug.v systems/VarDRaft.vo
+$(VARDDEBUGML): extraction/vard-debug/coq/ExtractVarDRaftDebug.v theories/Systems/VarDRaft.vo
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-debug/coq/ExtractVarDRaftDebug.v
 
 clean::
diff --git a/README.md b/README.md
index 8130d04..9a6c85b 100644
--- a/README.md
+++ b/README.md
@@ -75,9 +75,9 @@ compiled without checking any proofs.
 
 ## Files
 
-The `raft` and `raft-proofs` subdirectories contain the implementation and
-verification of Raft. For each proof interface file in `raft`, there is a 
-corresponding proof file in `raft-proofs`. The files in the `raft` 
+The `Raft` and `RaftProofs` subdirectories of `theories` contain the implementation
+and verification of Raft. For each proof interface file in `Raft`, there is a
+corresponding proof file in `RaftProofs`. The files in the `Raft`
 subdirectory include:
 
 - `Raft.v`: an implementation of Raft in Verdi
@@ -87,16 +87,16 @@ subdirectory include:
 - `CommonTheorems.v`: several useful theorems about functions used by
   the Raft implementation
 - `OneLeaderPerTermInterface`: a statement of Raft's *election
-  safety* property. See also the corresponding proof file in `raft-proofs`.
+  safety* property. See also the corresponding proof file in `RaftProofs`.
     - `CandidatesVoteForSelvesInterface.v`, `VotesCorrectInterface.v`, and
       `CroniesCorrectInterface.v`: statements of properties used by the proof
       `OneLeaderPerTermProof.v`
 - `LogMatchingInterface.v`: a statement of Raft's *log matching*
-    property. See also `LogMatchingProof.v` in `raft-proofs`
+    property. See also `LogMatchingProof.v` in `RaftProofs`
     - `LeaderSublogInterface.v`, `SortedInterface.v`, and `UniqueIndicesInterface.v`: statements
       of properties used by `LogMatchingProof.v`
 
-The file `EndToEndLinearizability.v` in `raft-proofs` uses the proofs of
+The file `EndToEndLinearizability.v` in `RaftProofs` uses the proofs of
 all proof interfaces to show Raft's *linearizability* property.
 
 ## The `vard` Key-Value Store
diff --git a/_CoqProject b/_CoqProject
index d3d17be..d975c0d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,224 +1,218 @@
--Q raft VerdiRaft
--Q raft-proofs VerdiRaft
--Q systems VerdiRaft
+-Q theories VerdiRaft
 -Q extraction/vard/coq VerdiRaft
 -Q extraction/vard-serialized/coq VerdiRaft
 -Q extraction/vard-log/coq VerdiRaft
 -Q extraction/vard-serialized-log/coq VerdiRaft
 -Q extraction/vard-debug/coq VerdiRaft
 
-raft/CommonTheorems.v
-raft/AppliedImpliesInputInterface.v
-raft/VotesVotesWithLogCorrespondInterface.v
-raft/InLogInAllEntriesInterface.v
-raft/AllEntriesCandidateEntriesInterface.v
-raft/SpecLemmas.v
-raft/StateMachineSafetyPrimeInterface.v
-raft/VotedForTermSanityInterface.v
-raft/CroniesCorrectInterface.v
-raft/AppliedEntriesMonotonicInterface.v
-raft/RaftLinearizableProofs.v
-raft/TransitiveCommitInterface.v
-raft/VotedForMoreUpToDateInterface.v
-raft/LeaderLogsTermSanityInterface.v
-raft/LastAppliedLeCommitIndexInterface.v
-raft/RefinementSpecLemmas.v
-raft/AllEntriesLeaderLogsInterface.v
-raft/LeaderLogsCandidateEntriesInterface.v
-raft/RaftMsgRefinementInterface.v
-raft/VotesWithLogSortedInterface.v
-raft/StateMachineSafetyInterface.v
-raft/AllEntriesLeaderSublogInterface.v
-raft/DecompositionWithPostState.v
-raft/GhostLogCorrectInterface.v
-raft/LeaderLogsPreservedInterface.v
-raft/LogsLeaderLogsInterface.v
-raft/PrevLogLeaderSublogInterface.v
-raft/AppendEntriesRequestReplyCorrespondenceInterface.v
-raft/LeaderLogsSortedInterface.v
-raft/MatchIndexSanityInterface.v
-raft/LeadersHaveLeaderLogsInterface.v
-raft/LeaderCompletenessInterface.v
-raft/VotesWithLogTermSanityInterface.v
-raft/Linearizability.v
-raft/AppendEntriesLeaderInterface.v
-raft/CandidateTermGtLogInterface.v
-raft/GhostLogAllEntriesInterface.v
-raft/OneLeaderPerTermInterface.v
-raft/MatchIndexAllEntriesInterface.v
-raft/CausalOrderPreservedInterface.v
-raft/CroniesTermInterface.v
-raft/UniqueIndicesInterface.v
-raft/CurrentTermGtZeroInterface.v
-raft/LeaderSublogInterface.v
-raft/LogMatchingInterface.v
-raft/InputBeforeOutputInterface.v
-raft/CandidatesVoteForSelvesInterface.v
-raft/RequestVoteReplyMoreUpToDateInterface.v
-raft/StateMachineCorrectInterface.v
-raft/CandidateEntriesInterface.v
-raft/LastAppliedCommitIndexMatchingInterface.v
-raft/RaftState.v
-raft/NextIndexSafetyInterface.v
-raft/NoAppendEntriesToSelfInterface.v
-raft/LogAllEntriesInterface.v
-raft/RefinementCommonTheorems.v
-raft/LeadersHaveLeaderLogsStrongInterface.v
-raft/NoAppendEntriesToLeaderInterface.v
-raft/OneLeaderLogPerTermInterface.v
-raft/TermsAndIndicesFromOneInterface.v
-raft/AllEntriesLogMatchingInterface.v
-raft/RequestVoteTermSanityInterface.v
-raft/GhostLogsLogPropertiesInterface.v
-raft/RequestVoteReplyTermSanityInterface.v
-raft/MatchIndexLeaderInterface.v
-raft/OutputImpliesAppliedInterface.v
-raft/GhostLogLogMatchingInterface.v
-raft/EveryEntryWasCreatedHostLogInterface.v
-raft/AppendEntriesReplySublogInterface.v
-raft/AppendEntriesRequestsCameFromLeadersInterface.v
-raft/CommonDefinitions.v
-raft/PrefixWithinTermInterface.v
-raft/AppendEntriesRequestTermSanityInterface.v
-raft/AllEntriesLeaderLogsTermInterface.v
-raft/SortedInterface.v
-raft/VotesLeCurrentTermInterface.v
-raft/Raft.v
-raft/OutputGreatestIdInterface.v
-raft/CommitRecordedCommittedInterface.v
-raft/VotesCorrectInterface.v
-raft/VotesReceivedMoreUpToDateInterface.v
-raft/AllEntriesIndicesGt0Interface.v
-raft/LeaderLogsVotesWithLogInterface.v
-raft/NoAppendEntriesRepliesToSelfInterface.v
-raft/AppendEntriesRequestLeaderLogsInterface.v
-raft/LeaderLogsLogPropertiesInterface.v
-raft/LeaderLogsSublogInterface.v
-raft/LeaderLogsContiguousInterface.v
-raft/TermSanityInterface.v
-raft/TermsAndIndicesFromOneLogInterface.v
-raft/PrevLogCandidateEntriesTermInterface.v
-raft/StateTraceInvariant.v
-raft/AllEntriesTermSanityInterface.v
-raft/RefinedLogMatchingLemmasInterface.v
-raft/AllEntriesLogInterface.v
-raft/AllEntriesVotesWithLogInterface.v
-raft/LeaderLogsLogMatchingInterface.v
-raft/MaxIndexSanityInterface.v
-raft/RequestVoteMaxIndexMaxTermInterface.v
-raft/OutputCorrectInterface.v
-raft/RaftRefinementInterface.v
-raft/TraceUtil.v
-raft/EveryEntryWasCreatedInterface.v
-raft/RefinementCommonDefinitions.v
+theories/Raft/CommonTheorems.v
+theories/Raft/AppliedImpliesInputInterface.v
+theories/Raft/VotesVotesWithLogCorrespondInterface.v
+theories/Raft/InLogInAllEntriesInterface.v
+theories/Raft/AllEntriesCandidateEntriesInterface.v
+theories/Raft/SpecLemmas.v
+theories/Raft/StateMachineSafetyPrimeInterface.v
+theories/Raft/VotedForTermSanityInterface.v
+theories/Raft/CroniesCorrectInterface.v
+theories/Raft/AppliedEntriesMonotonicInterface.v
+theories/Raft/RaftLinearizableProofs.v
+theories/Raft/TransitiveCommitInterface.v
+theories/Raft/VotedForMoreUpToDateInterface.v
+theories/Raft/LeaderLogsTermSanityInterface.v
+theories/Raft/LastAppliedLeCommitIndexInterface.v
+theories/Raft/RefinementSpecLemmas.v
+theories/Raft/AllEntriesLeaderLogsInterface.v
+theories/Raft/LeaderLogsCandidateEntriesInterface.v
+theories/Raft/RaftMsgRefinementInterface.v
+theories/Raft/VotesWithLogSortedInterface.v
+theories/Raft/StateMachineSafetyInterface.v
+theories/Raft/AllEntriesLeaderSublogInterface.v
+theories/Raft/DecompositionWithPostState.v
+theories/Raft/GhostLogCorrectInterface.v
+theories/Raft/LeaderLogsPreservedInterface.v
+theories/Raft/LogsLeaderLogsInterface.v
+theories/Raft/PrevLogLeaderSublogInterface.v
+theories/Raft/AppendEntriesRequestReplyCorrespondenceInterface.v
+theories/Raft/LeaderLogsSortedInterface.v
+theories/Raft/MatchIndexSanityInterface.v
+theories/Raft/LeadersHaveLeaderLogsInterface.v
+theories/Raft/LeaderCompletenessInterface.v
+theories/Raft/VotesWithLogTermSanityInterface.v
+theories/Raft/Linearizability.v
+theories/Raft/AppendEntriesLeaderInterface.v
+theories/Raft/CandidateTermGtLogInterface.v
+theories/Raft/GhostLogAllEntriesInterface.v
+theories/Raft/OneLeaderPerTermInterface.v
+theories/Raft/MatchIndexAllEntriesInterface.v
+theories/Raft/CausalOrderPreservedInterface.v
+theories/Raft/CroniesTermInterface.v
+theories/Raft/UniqueIndicesInterface.v
+theories/Raft/CurrentTermGtZeroInterface.v
+theories/Raft/LeaderSublogInterface.v
+theories/Raft/LogMatchingInterface.v
+theories/Raft/InputBeforeOutputInterface.v
+theories/Raft/CandidatesVoteForSelvesInterface.v
+theories/Raft/RequestVoteReplyMoreUpToDateInterface.v
+theories/Raft/StateMachineCorrectInterface.v
+theories/Raft/CandidateEntriesInterface.v
+theories/Raft/LastAppliedCommitIndexMatchingInterface.v
+theories/Raft/RaftState.v
+theories/Raft/NextIndexSafetyInterface.v
+theories/Raft/NoAppendEntriesToSelfInterface.v
+theories/Raft/LogAllEntriesInterface.v
+theories/Raft/RefinementCommonTheorems.v
+theories/Raft/LeadersHaveLeaderLogsStrongInterface.v
+theories/Raft/NoAppendEntriesToLeaderInterface.v
+theories/Raft/OneLeaderLogPerTermInterface.v
+theories/Raft/TermsAndIndicesFromOneInterface.v
+theories/Raft/AllEntriesLogMatchingInterface.v
+theories/Raft/RequestVoteTermSanityInterface.v
+theories/Raft/GhostLogsLogPropertiesInterface.v
+theories/Raft/RequestVoteReplyTermSanityInterface.v
+theories/Raft/MatchIndexLeaderInterface.v
+theories/Raft/OutputImpliesAppliedInterface.v
+theories/Raft/GhostLogLogMatchingInterface.v
+theories/Raft/EveryEntryWasCreatedHostLogInterface.v
+theories/Raft/AppendEntriesReplySublogInterface.v
+theories/Raft/AppendEntriesRequestsCameFromLeadersInterface.v
+theories/Raft/CommonDefinitions.v
+theories/Raft/PrefixWithinTermInterface.v
+theories/Raft/AppendEntriesRequestTermSanityInterface.v
+theories/Raft/AllEntriesLeaderLogsTermInterface.v
+theories/Raft/SortedInterface.v
+theories/Raft/VotesLeCurrentTermInterface.v
+theories/Raft/Raft.v
+theories/Raft/OutputGreatestIdInterface.v
+theories/Raft/CommitRecordedCommittedInterface.v
+theories/Raft/VotesCorrectInterface.v
+theories/Raft/VotesReceivedMoreUpToDateInterface.v
+theories/Raft/AllEntriesIndicesGt0Interface.v
+theories/Raft/LeaderLogsVotesWithLogInterface.v
+theories/Raft/NoAppendEntriesRepliesToSelfInterface.v
+theories/Raft/AppendEntriesRequestLeaderLogsInterface.v
+theories/Raft/LeaderLogsLogPropertiesInterface.v
+theories/Raft/LeaderLogsSublogInterface.v
+theories/Raft/LeaderLogsContiguousInterface.v
+theories/Raft/TermSanityInterface.v
+theories/Raft/TermsAndIndicesFromOneLogInterface.v
+theories/Raft/PrevLogCandidateEntriesTermInterface.v
+theories/Raft/StateTraceInvariant.v
+theories/Raft/AllEntriesTermSanityInterface.v
+theories/Raft/RefinedLogMatchingLemmasInterface.v
+theories/Raft/AllEntriesLogInterface.v
+theories/Raft/AllEntriesVotesWithLogInterface.v
+theories/Raft/LeaderLogsLogMatchingInterface.v
+theories/Raft/MaxIndexSanityInterface.v
+theories/Raft/RequestVoteMaxIndexMaxTermInterface.v
+theories/Raft/OutputCorrectInterface.v
+theories/Raft/RaftRefinementInterface.v
+theories/Raft/TraceUtil.v
+theories/Raft/EveryEntryWasCreatedInterface.v
+theories/Raft/RefinementCommonDefinitions.v
 
-raft-proofs/StateMachineSafetyProof.v
-raft-proofs/NoAppendEntriesToLeaderProof.v
-raft-proofs/GhostLogsLogPropertiesProof.v
-raft-proofs/TermSanityProof.v
-raft-proofs/MatchIndexSanityProof.v
-raft-proofs/OneLeaderPerTermProof.v
-raft-proofs/CroniesCorrectProof.v
-raft-proofs/LogMatchingProof.v
-raft-proofs/SortedProof.v
-raft-proofs/RequestVoteReplyMoreUpToDateProof.v
-raft-proofs/EveryEntryWasCreatedProof.v
-raft-proofs/TransitiveCommitProof.v
-raft-proofs/AllEntriesLeaderLogsProof.v
-raft-proofs/TermsAndIndicesFromOneLogProof.v
-raft-proofs/EveryEntryWasCreatedHostLogProof.v
-raft-proofs/VotedForTermSanityProof.v
-raft-proofs/OutputCorrectProof.v
-raft-proofs/OutputImpliesAppliedProof.v
-raft-proofs/LeaderLogsSublogProof.v
-raft-proofs/AllEntriesLogProof.v
-raft-proofs/RequestVoteTermSanityProof.v
-raft-proofs/GhostLogAllEntriesProof.v
-raft-proofs/AppliedImpliesInputProof.v
-raft-proofs/LeaderLogsVotesWithLogProof.v
-raft-proofs/LeaderLogsTermSanityProof.v
-raft-proofs/LastAppliedCommitIndexMatchingProof.v
-raft-proofs/AllEntriesLogMatchingProof.v
-raft-proofs/VotesReceivedMoreUpToDateProof.v
-raft-proofs/CandidateEntriesProof.v
-raft-proofs/CroniesTermProof.v
-raft-proofs/VotesWithLogTermSanityProof.v
-raft-proofs/CandidateTermGtLogProof.v
-raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v
-raft-proofs/AppendEntriesReplySublogProof.v
-raft-proofs/MatchIndexLeaderProof.v
-raft-proofs/AppendEntriesRequestTermSanityProof.v
-raft-proofs/StateMachineSafetyPrimeProof.v
-raft-proofs/LogsLeaderLogsProof.v
-raft-proofs/AllEntriesLeaderLogsTermProof.v
-raft-proofs/OutputGreatestIdProof.v
-raft-proofs/AppendEntriesRequestLeaderLogsProof.v
-raft-proofs/PrefixWithinTermProof.v
-raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v
-raft-proofs/OneLeaderLogPerTermProof.v
-raft-proofs/RefinedLogMatchingLemmasProof.v
-raft-proofs/CurrentTermGtZeroProof.v
-raft-proofs/LeaderLogsSortedProof.v
-raft-proofs/AppendEntriesLeaderProof.v
-raft-proofs/MatchIndexAllEntriesProof.v
-raft-proofs/NoAppendEntriesToSelfProof.v
-raft-proofs/InputBeforeOutputProof.v
-raft-proofs/LeaderLogsContiguousProof.v
-raft-proofs/VotesWithLogSortedProof.v
-raft-proofs/UniqueIndicesProof.v
-raft-proofs/AppliedEntriesMonotonicProof.v
-raft-proofs/TermsAndIndicesFromOneProof.v
-raft-proofs/LeadersHaveLeaderLogsProof.v
-raft-proofs/AllEntriesVotesWithLogProof.v
-raft-proofs/LeadersHaveLeaderLogsStrongProof.v
-raft-proofs/LastAppliedLeCommitIndexProof.v
-raft-proofs/CausalOrderPreservedProof.v
-raft-proofs/StateMachineCorrectProof.v
-raft-proofs/RequestVoteReplyTermSanityProof.v
-raft-proofs/RaftRefinementProof.v
-raft-proofs/VotesVotesWithLogCorrespondProof.v
-raft-proofs/LogAllEntriesProof.v
-raft-proofs/VotedForMoreUpToDateProof.v
-raft-proofs/AllEntriesTermSanityProof.v
-raft-proofs/NextIndexSafetyProof.v
-raft-proofs/LeaderLogsLogMatchingProof.v
-raft-proofs/GhostLogLogMatchingProof.v
-raft-proofs/AllEntriesCandidateEntriesProof.v
-raft-proofs/PrevLogCandidateEntriesTermProof.v
-raft-proofs/AllEntriesLeaderSublogProof.v
-raft-proofs/AllEntriesIndicesGt0Proof.v
-raft-proofs/GhostLogCorrectProof.v
-raft-proofs/VotesCorrectProof.v
-raft-proofs/LeaderLogsPreservedProof.v
-raft-proofs/RaftMsgRefinementProof.v
-raft-proofs/EndToEndLinearizability.v
-raft-proofs/NoAppendEntriesRepliesToSelfProof.v
-raft-proofs/LeaderCompletenessProof.v
-raft-proofs/CandidatesVoteForSelvesProof.v
-raft-proofs/InLogInAllEntriesProof.v
-raft-proofs/RequestVoteMaxIndexMaxTermProof.v
-raft-proofs/LeaderLogsCandidateEntriesProof.v
-raft-proofs/LeaderLogsLogPropertiesProof.v
-raft-proofs/LeaderSublogProof.v
-raft-proofs/PrevLogLeaderSublogProof.v
-raft-proofs/VotesLeCurrentTermProof.v
+theories/RaftProofs/StateMachineSafetyProof.v
+theories/RaftProofs/NoAppendEntriesToLeaderProof.v
+theories/RaftProofs/GhostLogsLogPropertiesProof.v
+theories/RaftProofs/TermSanityProof.v
+theories/RaftProofs/MatchIndexSanityProof.v
+theories/RaftProofs/OneLeaderPerTermProof.v
+theories/RaftProofs/CroniesCorrectProof.v
+theories/RaftProofs/LogMatchingProof.v
+theories/RaftProofs/SortedProof.v
+theories/RaftProofs/RequestVoteReplyMoreUpToDateProof.v
+theories/RaftProofs/EveryEntryWasCreatedProof.v
+theories/RaftProofs/TransitiveCommitProof.v
+theories/RaftProofs/AllEntriesLeaderLogsProof.v
+theories/RaftProofs/TermsAndIndicesFromOneLogProof.v
+theories/RaftProofs/EveryEntryWasCreatedHostLogProof.v
+theories/RaftProofs/VotedForTermSanityProof.v
+theories/RaftProofs/OutputCorrectProof.v
+theories/RaftProofs/OutputImpliesAppliedProof.v
+theories/RaftProofs/LeaderLogsSublogProof.v
+theories/RaftProofs/AllEntriesLogProof.v
+theories/RaftProofs/RequestVoteTermSanityProof.v
+theories/RaftProofs/GhostLogAllEntriesProof.v
+theories/RaftProofs/AppliedImpliesInputProof.v
+theories/RaftProofs/LeaderLogsVotesWithLogProof.v
+theories/RaftProofs/LeaderLogsTermSanityProof.v
+theories/RaftProofs/LastAppliedCommitIndexMatchingProof.v
+theories/RaftProofs/AllEntriesLogMatchingProof.v
+theories/RaftProofs/VotesReceivedMoreUpToDateProof.v
+theories/RaftProofs/CandidateEntriesProof.v
+theories/RaftProofs/CroniesTermProof.v
+theories/RaftProofs/VotesWithLogTermSanityProof.v
+theories/RaftProofs/CandidateTermGtLogProof.v
+theories/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.v
+theories/RaftProofs/AppendEntriesReplySublogProof.v
+theories/RaftProofs/MatchIndexLeaderProof.v
+theories/RaftProofs/AppendEntriesRequestTermSanityProof.v
+theories/RaftProofs/StateMachineSafetyPrimeProof.v
+theories/RaftProofs/LogsLeaderLogsProof.v
+theories/RaftProofs/AllEntriesLeaderLogsTermProof.v
+theories/RaftProofs/OutputGreatestIdProof.v
+theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v
+theories/RaftProofs/PrefixWithinTermProof.v
+theories/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.v
+theories/RaftProofs/OneLeaderLogPerTermProof.v
+theories/RaftProofs/RefinedLogMatchingLemmasProof.v
+theories/RaftProofs/CurrentTermGtZeroProof.v
+theories/RaftProofs/LeaderLogsSortedProof.v
+theories/RaftProofs/AppendEntriesLeaderProof.v
+theories/RaftProofs/MatchIndexAllEntriesProof.v
+theories/RaftProofs/NoAppendEntriesToSelfProof.v
+theories/RaftProofs/InputBeforeOutputProof.v
+theories/RaftProofs/LeaderLogsContiguousProof.v
+theories/RaftProofs/VotesWithLogSortedProof.v
+theories/RaftProofs/UniqueIndicesProof.v
+theories/RaftProofs/AppliedEntriesMonotonicProof.v
+theories/RaftProofs/TermsAndIndicesFromOneProof.v
+theories/RaftProofs/LeadersHaveLeaderLogsProof.v
+theories/RaftProofs/AllEntriesVotesWithLogProof.v
+theories/RaftProofs/LeadersHaveLeaderLogsStrongProof.v
+theories/RaftProofs/LastAppliedLeCommitIndexProof.v
+theories/RaftProofs/CausalOrderPreservedProof.v
+theories/RaftProofs/StateMachineCorrectProof.v
+theories/RaftProofs/RequestVoteReplyTermSanityProof.v
+theories/RaftProofs/RaftRefinementProof.v
+theories/RaftProofs/VotesVotesWithLogCorrespondProof.v
+theories/RaftProofs/LogAllEntriesProof.v
+theories/RaftProofs/VotedForMoreUpToDateProof.v
+theories/RaftProofs/AllEntriesTermSanityProof.v
+theories/RaftProofs/NextIndexSafetyProof.v
+theories/RaftProofs/LeaderLogsLogMatchingProof.v
+theories/RaftProofs/GhostLogLogMatchingProof.v
+theories/RaftProofs/AllEntriesCandidateEntriesProof.v
+theories/RaftProofs/PrevLogCandidateEntriesTermProof.v
+theories/RaftProofs/AllEntriesLeaderSublogProof.v
+theories/RaftProofs/AllEntriesIndicesGt0Proof.v
+theories/RaftProofs/GhostLogCorrectProof.v
+theories/RaftProofs/VotesCorrectProof.v
+theories/RaftProofs/LeaderLogsPreservedProof.v
+theories/RaftProofs/RaftMsgRefinementProof.v
+theories/RaftProofs/EndToEndLinearizability.v
+theories/RaftProofs/NoAppendEntriesRepliesToSelfProof.v
+theories/RaftProofs/LeaderCompletenessProof.v
+theories/RaftProofs/CandidatesVoteForSelvesProof.v
+theories/RaftProofs/InLogInAllEntriesProof.v
+theories/RaftProofs/RequestVoteMaxIndexMaxTermProof.v
+theories/RaftProofs/LeaderLogsCandidateEntriesProof.v
+theories/RaftProofs/LeaderLogsLogPropertiesProof.v
+theories/RaftProofs/LeaderSublogProof.v
+theories/RaftProofs/PrevLogLeaderSublogProof.v
+theories/RaftProofs/VotesLeCurrentTermProof.v
 
-systems/VarDRaftSerializedLogCorrect.v
-systems/VarDRaftCorrect.v
-systems/VarDRaftSerializedCorrect.v
-systems/VarDRaftSerializedLog.v
-systems/VarDRaftLogCorrect.v
-systems/VarDRaftSerialized.v
-systems/VarDRaftSerializers.v
-systems/VarDRaftLog.v
-systems/VarDRaft.v
+theories/Systems/VarDRaftSerializedLogCorrect.v
+theories/Systems/VarDRaftCorrect.v
+theories/Systems/VarDRaftSerializedCorrect.v
+theories/Systems/VarDRaftSerializedLog.v
+theories/Systems/VarDRaftLogCorrect.v
+theories/Systems/VarDRaftSerialized.v
+theories/Systems/VarDRaftSerializers.v
+theories/Systems/VarDRaftLog.v
+theories/Systems/VarDRaft.v
 
 extraction/vard/coq/ExtractVarDRaft.v
-
 extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v
-
 extraction/vard-log/coq/ExtractVarDRaftLog.v
-
 extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v
-
 extraction/vard-debug/coq/ExtractVarDRaftDebug.v
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..50906a2
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.5)
+(using coq 0.6)
+(name verdi-raft)
diff --git a/meta.yml b/meta.yml
index 5641255..fc365fc 100644
--- a/meta.yml
+++ b/meta.yml
@@ -131,9 +131,9 @@ build: |-
 documentation: |-
   ## Files
 
-  The `raft` and `raft-proofs` subdirectories contain the implementation and
-  verification of Raft. For each proof interface file in `raft`, there is a 
-  corresponding proof file in `raft-proofs`. The files in the `raft` 
+  The `Raft` and `RaftProofs` subdirectories of `theories` contain the implementation
+  and verification of Raft. For each proof interface file in `Raft`, there is a
+  corresponding proof file in `RaftProofs`. The files in the `Raft`
   subdirectory include:
   
   - `Raft.v`: an implementation of Raft in Verdi
@@ -143,16 +143,16 @@ documentation: |-
   - `CommonTheorems.v`: several useful theorems about functions used by
     the Raft implementation
   - `OneLeaderPerTermInterface`: a statement of Raft's *election
-    safety* property. See also the corresponding proof file in `raft-proofs`.
+    safety* property. See also the corresponding proof file in `RaftProofs`.
       - `CandidatesVoteForSelvesInterface.v`, `VotesCorrectInterface.v`, and
         `CroniesCorrectInterface.v`: statements of properties used by the proof
         `OneLeaderPerTermProof.v`
   - `LogMatchingInterface.v`: a statement of Raft's *log matching*
-      property. See also `LogMatchingProof.v` in `raft-proofs`
+      property. See also `LogMatchingProof.v` in `RaftProofs`
       - `LeaderSublogInterface.v`, `SortedInterface.v`, and `UniqueIndicesInterface.v`: statements
         of properties used by `LogMatchingProof.v`
   
-  The file `EndToEndLinearizability.v` in `raft-proofs` uses the proofs of
+  The file `EndToEndLinearizability.v` in `RaftProofs` uses the proofs of
   all proof interfaces to show Raft's *linearizability* property.
 
   ## The `vard` Key-Value Store
diff --git a/raft/AllEntriesCandidateEntriesInterface.v b/theories/Raft/AllEntriesCandidateEntriesInterface.v
similarity index 100%
rename from raft/AllEntriesCandidateEntriesInterface.v
rename to theories/Raft/AllEntriesCandidateEntriesInterface.v
diff --git a/raft/AllEntriesIndicesGt0Interface.v b/theories/Raft/AllEntriesIndicesGt0Interface.v
similarity index 100%
rename from raft/AllEntriesIndicesGt0Interface.v
rename to theories/Raft/AllEntriesIndicesGt0Interface.v
diff --git a/raft/AllEntriesLeaderLogsInterface.v b/theories/Raft/AllEntriesLeaderLogsInterface.v
similarity index 100%
rename from raft/AllEntriesLeaderLogsInterface.v
rename to theories/Raft/AllEntriesLeaderLogsInterface.v
diff --git a/raft/AllEntriesLeaderLogsTermInterface.v b/theories/Raft/AllEntriesLeaderLogsTermInterface.v
similarity index 100%
rename from raft/AllEntriesLeaderLogsTermInterface.v
rename to theories/Raft/AllEntriesLeaderLogsTermInterface.v
diff --git a/raft/AllEntriesLeaderSublogInterface.v b/theories/Raft/AllEntriesLeaderSublogInterface.v
similarity index 100%
rename from raft/AllEntriesLeaderSublogInterface.v
rename to theories/Raft/AllEntriesLeaderSublogInterface.v
diff --git a/raft/AllEntriesLogInterface.v b/theories/Raft/AllEntriesLogInterface.v
similarity index 100%
rename from raft/AllEntriesLogInterface.v
rename to theories/Raft/AllEntriesLogInterface.v
diff --git a/raft/AllEntriesLogMatchingInterface.v b/theories/Raft/AllEntriesLogMatchingInterface.v
similarity index 100%
rename from raft/AllEntriesLogMatchingInterface.v
rename to theories/Raft/AllEntriesLogMatchingInterface.v
diff --git a/raft/AllEntriesTermSanityInterface.v b/theories/Raft/AllEntriesTermSanityInterface.v
similarity index 100%
rename from raft/AllEntriesTermSanityInterface.v
rename to theories/Raft/AllEntriesTermSanityInterface.v
diff --git a/raft/AllEntriesVotesWithLogInterface.v b/theories/Raft/AllEntriesVotesWithLogInterface.v
similarity index 100%
rename from raft/AllEntriesVotesWithLogInterface.v
rename to theories/Raft/AllEntriesVotesWithLogInterface.v
diff --git a/raft/AppendEntriesLeaderInterface.v b/theories/Raft/AppendEntriesLeaderInterface.v
similarity index 100%
rename from raft/AppendEntriesLeaderInterface.v
rename to theories/Raft/AppendEntriesLeaderInterface.v
diff --git a/raft/AppendEntriesReplySublogInterface.v b/theories/Raft/AppendEntriesReplySublogInterface.v
similarity index 100%
rename from raft/AppendEntriesReplySublogInterface.v
rename to theories/Raft/AppendEntriesReplySublogInterface.v
diff --git a/raft/AppendEntriesRequestLeaderLogsInterface.v b/theories/Raft/AppendEntriesRequestLeaderLogsInterface.v
similarity index 100%
rename from raft/AppendEntriesRequestLeaderLogsInterface.v
rename to theories/Raft/AppendEntriesRequestLeaderLogsInterface.v
diff --git a/raft/AppendEntriesRequestReplyCorrespondenceInterface.v b/theories/Raft/AppendEntriesRequestReplyCorrespondenceInterface.v
similarity index 100%
rename from raft/AppendEntriesRequestReplyCorrespondenceInterface.v
rename to theories/Raft/AppendEntriesRequestReplyCorrespondenceInterface.v
diff --git a/raft/AppendEntriesRequestTermSanityInterface.v b/theories/Raft/AppendEntriesRequestTermSanityInterface.v
similarity index 100%
rename from raft/AppendEntriesRequestTermSanityInterface.v
rename to theories/Raft/AppendEntriesRequestTermSanityInterface.v
diff --git a/raft/AppendEntriesRequestsCameFromLeadersInterface.v b/theories/Raft/AppendEntriesRequestsCameFromLeadersInterface.v
similarity index 100%
rename from raft/AppendEntriesRequestsCameFromLeadersInterface.v
rename to theories/Raft/AppendEntriesRequestsCameFromLeadersInterface.v
diff --git a/raft/AppliedEntriesMonotonicInterface.v b/theories/Raft/AppliedEntriesMonotonicInterface.v
similarity index 100%
rename from raft/AppliedEntriesMonotonicInterface.v
rename to theories/Raft/AppliedEntriesMonotonicInterface.v
diff --git a/raft/AppliedImpliesInputInterface.v b/theories/Raft/AppliedImpliesInputInterface.v
similarity index 100%
rename from raft/AppliedImpliesInputInterface.v
rename to theories/Raft/AppliedImpliesInputInterface.v
diff --git a/raft/CandidateEntriesInterface.v b/theories/Raft/CandidateEntriesInterface.v
similarity index 100%
rename from raft/CandidateEntriesInterface.v
rename to theories/Raft/CandidateEntriesInterface.v
diff --git a/raft/CandidateTermGtLogInterface.v b/theories/Raft/CandidateTermGtLogInterface.v
similarity index 100%
rename from raft/CandidateTermGtLogInterface.v
rename to theories/Raft/CandidateTermGtLogInterface.v
diff --git a/raft/CandidatesVoteForSelvesInterface.v b/theories/Raft/CandidatesVoteForSelvesInterface.v
similarity index 100%
rename from raft/CandidatesVoteForSelvesInterface.v
rename to theories/Raft/CandidatesVoteForSelvesInterface.v
diff --git a/raft/CausalOrderPreservedInterface.v b/theories/Raft/CausalOrderPreservedInterface.v
similarity index 100%
rename from raft/CausalOrderPreservedInterface.v
rename to theories/Raft/CausalOrderPreservedInterface.v
diff --git a/raft/CommitRecordedCommittedInterface.v b/theories/Raft/CommitRecordedCommittedInterface.v
similarity index 100%
rename from raft/CommitRecordedCommittedInterface.v
rename to theories/Raft/CommitRecordedCommittedInterface.v
diff --git a/raft/CommonDefinitions.v b/theories/Raft/CommonDefinitions.v
similarity index 100%
rename from raft/CommonDefinitions.v
rename to theories/Raft/CommonDefinitions.v
diff --git a/raft/CommonTheorems.v b/theories/Raft/CommonTheorems.v
similarity index 100%
rename from raft/CommonTheorems.v
rename to theories/Raft/CommonTheorems.v
diff --git a/raft/CroniesCorrectInterface.v b/theories/Raft/CroniesCorrectInterface.v
similarity index 100%
rename from raft/CroniesCorrectInterface.v
rename to theories/Raft/CroniesCorrectInterface.v
diff --git a/raft/CroniesTermInterface.v b/theories/Raft/CroniesTermInterface.v
similarity index 100%
rename from raft/CroniesTermInterface.v
rename to theories/Raft/CroniesTermInterface.v
diff --git a/raft/CurrentTermGtZeroInterface.v b/theories/Raft/CurrentTermGtZeroInterface.v
similarity index 100%
rename from raft/CurrentTermGtZeroInterface.v
rename to theories/Raft/CurrentTermGtZeroInterface.v
diff --git a/raft/DecompositionWithPostState.v b/theories/Raft/DecompositionWithPostState.v
similarity index 100%
rename from raft/DecompositionWithPostState.v
rename to theories/Raft/DecompositionWithPostState.v
diff --git a/raft/EveryEntryWasCreatedHostLogInterface.v b/theories/Raft/EveryEntryWasCreatedHostLogInterface.v
similarity index 100%
rename from raft/EveryEntryWasCreatedHostLogInterface.v
rename to theories/Raft/EveryEntryWasCreatedHostLogInterface.v
diff --git a/raft/EveryEntryWasCreatedInterface.v b/theories/Raft/EveryEntryWasCreatedInterface.v
similarity index 100%
rename from raft/EveryEntryWasCreatedInterface.v
rename to theories/Raft/EveryEntryWasCreatedInterface.v
diff --git a/raft/GhostLogAllEntriesInterface.v b/theories/Raft/GhostLogAllEntriesInterface.v
similarity index 100%
rename from raft/GhostLogAllEntriesInterface.v
rename to theories/Raft/GhostLogAllEntriesInterface.v
diff --git a/raft/GhostLogCorrectInterface.v b/theories/Raft/GhostLogCorrectInterface.v
similarity index 100%
rename from raft/GhostLogCorrectInterface.v
rename to theories/Raft/GhostLogCorrectInterface.v
diff --git a/raft/GhostLogLogMatchingInterface.v b/theories/Raft/GhostLogLogMatchingInterface.v
similarity index 100%
rename from raft/GhostLogLogMatchingInterface.v
rename to theories/Raft/GhostLogLogMatchingInterface.v
diff --git a/raft/GhostLogsLogPropertiesInterface.v b/theories/Raft/GhostLogsLogPropertiesInterface.v
similarity index 100%
rename from raft/GhostLogsLogPropertiesInterface.v
rename to theories/Raft/GhostLogsLogPropertiesInterface.v
diff --git a/raft/InLogInAllEntriesInterface.v b/theories/Raft/InLogInAllEntriesInterface.v
similarity index 100%
rename from raft/InLogInAllEntriesInterface.v
rename to theories/Raft/InLogInAllEntriesInterface.v
diff --git a/raft/InputBeforeOutputInterface.v b/theories/Raft/InputBeforeOutputInterface.v
similarity index 100%
rename from raft/InputBeforeOutputInterface.v
rename to theories/Raft/InputBeforeOutputInterface.v
diff --git a/raft/LastAppliedCommitIndexMatchingInterface.v b/theories/Raft/LastAppliedCommitIndexMatchingInterface.v
similarity index 100%
rename from raft/LastAppliedCommitIndexMatchingInterface.v
rename to theories/Raft/LastAppliedCommitIndexMatchingInterface.v
diff --git a/raft/LastAppliedLeCommitIndexInterface.v b/theories/Raft/LastAppliedLeCommitIndexInterface.v
similarity index 100%
rename from raft/LastAppliedLeCommitIndexInterface.v
rename to theories/Raft/LastAppliedLeCommitIndexInterface.v
diff --git a/raft/LeaderCompletenessInterface.v b/theories/Raft/LeaderCompletenessInterface.v
similarity index 100%
rename from raft/LeaderCompletenessInterface.v
rename to theories/Raft/LeaderCompletenessInterface.v
diff --git a/raft/LeaderLogsCandidateEntriesInterface.v b/theories/Raft/LeaderLogsCandidateEntriesInterface.v
similarity index 100%
rename from raft/LeaderLogsCandidateEntriesInterface.v
rename to theories/Raft/LeaderLogsCandidateEntriesInterface.v
diff --git a/raft/LeaderLogsContiguousInterface.v b/theories/Raft/LeaderLogsContiguousInterface.v
similarity index 100%
rename from raft/LeaderLogsContiguousInterface.v
rename to theories/Raft/LeaderLogsContiguousInterface.v
diff --git a/raft/LeaderLogsLogMatchingInterface.v b/theories/Raft/LeaderLogsLogMatchingInterface.v
similarity index 100%
rename from raft/LeaderLogsLogMatchingInterface.v
rename to theories/Raft/LeaderLogsLogMatchingInterface.v
diff --git a/raft/LeaderLogsLogPropertiesInterface.v b/theories/Raft/LeaderLogsLogPropertiesInterface.v
similarity index 100%
rename from raft/LeaderLogsLogPropertiesInterface.v
rename to theories/Raft/LeaderLogsLogPropertiesInterface.v
diff --git a/raft/LeaderLogsPreservedInterface.v b/theories/Raft/LeaderLogsPreservedInterface.v
similarity index 100%
rename from raft/LeaderLogsPreservedInterface.v
rename to theories/Raft/LeaderLogsPreservedInterface.v
diff --git a/raft/LeaderLogsSortedInterface.v b/theories/Raft/LeaderLogsSortedInterface.v
similarity index 100%
rename from raft/LeaderLogsSortedInterface.v
rename to theories/Raft/LeaderLogsSortedInterface.v
diff --git a/raft/LeaderLogsSublogInterface.v b/theories/Raft/LeaderLogsSublogInterface.v
similarity index 100%
rename from raft/LeaderLogsSublogInterface.v
rename to theories/Raft/LeaderLogsSublogInterface.v
diff --git a/raft/LeaderLogsTermSanityInterface.v b/theories/Raft/LeaderLogsTermSanityInterface.v
similarity index 100%
rename from raft/LeaderLogsTermSanityInterface.v
rename to theories/Raft/LeaderLogsTermSanityInterface.v
diff --git a/raft/LeaderLogsVotesWithLogInterface.v b/theories/Raft/LeaderLogsVotesWithLogInterface.v
similarity index 100%
rename from raft/LeaderLogsVotesWithLogInterface.v
rename to theories/Raft/LeaderLogsVotesWithLogInterface.v
diff --git a/raft/LeaderSublogInterface.v b/theories/Raft/LeaderSublogInterface.v
similarity index 100%
rename from raft/LeaderSublogInterface.v
rename to theories/Raft/LeaderSublogInterface.v
diff --git a/raft/LeadersHaveLeaderLogsInterface.v b/theories/Raft/LeadersHaveLeaderLogsInterface.v
similarity index 100%
rename from raft/LeadersHaveLeaderLogsInterface.v
rename to theories/Raft/LeadersHaveLeaderLogsInterface.v
diff --git a/raft/LeadersHaveLeaderLogsStrongInterface.v b/theories/Raft/LeadersHaveLeaderLogsStrongInterface.v
similarity index 100%
rename from raft/LeadersHaveLeaderLogsStrongInterface.v
rename to theories/Raft/LeadersHaveLeaderLogsStrongInterface.v
diff --git a/raft/Linearizability.v b/theories/Raft/Linearizability.v
similarity index 100%
rename from raft/Linearizability.v
rename to theories/Raft/Linearizability.v
diff --git a/raft/LogAllEntriesInterface.v b/theories/Raft/LogAllEntriesInterface.v
similarity index 100%
rename from raft/LogAllEntriesInterface.v
rename to theories/Raft/LogAllEntriesInterface.v
diff --git a/raft/LogMatchingInterface.v b/theories/Raft/LogMatchingInterface.v
similarity index 100%
rename from raft/LogMatchingInterface.v
rename to theories/Raft/LogMatchingInterface.v
diff --git a/raft/LogsLeaderLogsInterface.v b/theories/Raft/LogsLeaderLogsInterface.v
similarity index 100%
rename from raft/LogsLeaderLogsInterface.v
rename to theories/Raft/LogsLeaderLogsInterface.v
diff --git a/raft/MatchIndexAllEntriesInterface.v b/theories/Raft/MatchIndexAllEntriesInterface.v
similarity index 100%
rename from raft/MatchIndexAllEntriesInterface.v
rename to theories/Raft/MatchIndexAllEntriesInterface.v
diff --git a/raft/MatchIndexLeaderInterface.v b/theories/Raft/MatchIndexLeaderInterface.v
similarity index 100%
rename from raft/MatchIndexLeaderInterface.v
rename to theories/Raft/MatchIndexLeaderInterface.v
diff --git a/raft/MatchIndexSanityInterface.v b/theories/Raft/MatchIndexSanityInterface.v
similarity index 100%
rename from raft/MatchIndexSanityInterface.v
rename to theories/Raft/MatchIndexSanityInterface.v
diff --git a/raft/MaxIndexSanityInterface.v b/theories/Raft/MaxIndexSanityInterface.v
similarity index 100%
rename from raft/MaxIndexSanityInterface.v
rename to theories/Raft/MaxIndexSanityInterface.v
diff --git a/raft/NextIndexSafetyInterface.v b/theories/Raft/NextIndexSafetyInterface.v
similarity index 100%
rename from raft/NextIndexSafetyInterface.v
rename to theories/Raft/NextIndexSafetyInterface.v
diff --git a/raft/NoAppendEntriesRepliesToSelfInterface.v b/theories/Raft/NoAppendEntriesRepliesToSelfInterface.v
similarity index 100%
rename from raft/NoAppendEntriesRepliesToSelfInterface.v
rename to theories/Raft/NoAppendEntriesRepliesToSelfInterface.v
diff --git a/raft/NoAppendEntriesToLeaderInterface.v b/theories/Raft/NoAppendEntriesToLeaderInterface.v
similarity index 100%
rename from raft/NoAppendEntriesToLeaderInterface.v
rename to theories/Raft/NoAppendEntriesToLeaderInterface.v
diff --git a/raft/NoAppendEntriesToSelfInterface.v b/theories/Raft/NoAppendEntriesToSelfInterface.v
similarity index 100%
rename from raft/NoAppendEntriesToSelfInterface.v
rename to theories/Raft/NoAppendEntriesToSelfInterface.v
diff --git a/raft/OneLeaderLogPerTermInterface.v b/theories/Raft/OneLeaderLogPerTermInterface.v
similarity index 100%
rename from raft/OneLeaderLogPerTermInterface.v
rename to theories/Raft/OneLeaderLogPerTermInterface.v
diff --git a/raft/OneLeaderPerTermInterface.v b/theories/Raft/OneLeaderPerTermInterface.v
similarity index 100%
rename from raft/OneLeaderPerTermInterface.v
rename to theories/Raft/OneLeaderPerTermInterface.v
diff --git a/raft/OutputCorrectInterface.v b/theories/Raft/OutputCorrectInterface.v
similarity index 100%
rename from raft/OutputCorrectInterface.v
rename to theories/Raft/OutputCorrectInterface.v
diff --git a/raft/OutputGreatestIdInterface.v b/theories/Raft/OutputGreatestIdInterface.v
similarity index 100%
rename from raft/OutputGreatestIdInterface.v
rename to theories/Raft/OutputGreatestIdInterface.v
diff --git a/raft/OutputImpliesAppliedInterface.v b/theories/Raft/OutputImpliesAppliedInterface.v
similarity index 100%
rename from raft/OutputImpliesAppliedInterface.v
rename to theories/Raft/OutputImpliesAppliedInterface.v
diff --git a/raft/PrefixWithinTermInterface.v b/theories/Raft/PrefixWithinTermInterface.v
similarity index 100%
rename from raft/PrefixWithinTermInterface.v
rename to theories/Raft/PrefixWithinTermInterface.v
diff --git a/raft/PrevLogCandidateEntriesTermInterface.v b/theories/Raft/PrevLogCandidateEntriesTermInterface.v
similarity index 100%
rename from raft/PrevLogCandidateEntriesTermInterface.v
rename to theories/Raft/PrevLogCandidateEntriesTermInterface.v
diff --git a/raft/PrevLogLeaderSublogInterface.v b/theories/Raft/PrevLogLeaderSublogInterface.v
similarity index 100%
rename from raft/PrevLogLeaderSublogInterface.v
rename to theories/Raft/PrevLogLeaderSublogInterface.v
diff --git a/raft/Raft.v b/theories/Raft/Raft.v
similarity index 100%
rename from raft/Raft.v
rename to theories/Raft/Raft.v
diff --git a/raft/RaftLinearizableProofs.v b/theories/Raft/RaftLinearizableProofs.v
similarity index 100%
rename from raft/RaftLinearizableProofs.v
rename to theories/Raft/RaftLinearizableProofs.v
diff --git a/raft/RaftMsgRefinementInterface.v b/theories/Raft/RaftMsgRefinementInterface.v
similarity index 100%
rename from raft/RaftMsgRefinementInterface.v
rename to theories/Raft/RaftMsgRefinementInterface.v
diff --git a/raft/RaftRefinementInterface.v b/theories/Raft/RaftRefinementInterface.v
similarity index 100%
rename from raft/RaftRefinementInterface.v
rename to theories/Raft/RaftRefinementInterface.v
diff --git a/raft/RaftState.v b/theories/Raft/RaftState.v
similarity index 100%
rename from raft/RaftState.v
rename to theories/Raft/RaftState.v
diff --git a/raft/RaftState.v.rec b/theories/Raft/RaftState.v.rec
similarity index 100%
rename from raft/RaftState.v.rec
rename to theories/Raft/RaftState.v.rec
diff --git a/raft/RefinedLogMatchingLemmasInterface.v b/theories/Raft/RefinedLogMatchingLemmasInterface.v
similarity index 100%
rename from raft/RefinedLogMatchingLemmasInterface.v
rename to theories/Raft/RefinedLogMatchingLemmasInterface.v
diff --git a/raft/RefinementCommonDefinitions.v b/theories/Raft/RefinementCommonDefinitions.v
similarity index 100%
rename from raft/RefinementCommonDefinitions.v
rename to theories/Raft/RefinementCommonDefinitions.v
diff --git a/raft/RefinementCommonTheorems.v b/theories/Raft/RefinementCommonTheorems.v
similarity index 100%
rename from raft/RefinementCommonTheorems.v
rename to theories/Raft/RefinementCommonTheorems.v
diff --git a/raft/RefinementSpecLemmas.v b/theories/Raft/RefinementSpecLemmas.v
similarity index 100%
rename from raft/RefinementSpecLemmas.v
rename to theories/Raft/RefinementSpecLemmas.v
diff --git a/raft/RequestVoteMaxIndexMaxTermInterface.v b/theories/Raft/RequestVoteMaxIndexMaxTermInterface.v
similarity index 100%
rename from raft/RequestVoteMaxIndexMaxTermInterface.v
rename to theories/Raft/RequestVoteMaxIndexMaxTermInterface.v
diff --git a/raft/RequestVoteReplyMoreUpToDateInterface.v b/theories/Raft/RequestVoteReplyMoreUpToDateInterface.v
similarity index 100%
rename from raft/RequestVoteReplyMoreUpToDateInterface.v
rename to theories/Raft/RequestVoteReplyMoreUpToDateInterface.v
diff --git a/raft/RequestVoteReplyTermSanityInterface.v b/theories/Raft/RequestVoteReplyTermSanityInterface.v
similarity index 100%
rename from raft/RequestVoteReplyTermSanityInterface.v
rename to theories/Raft/RequestVoteReplyTermSanityInterface.v
diff --git a/raft/RequestVoteTermSanityInterface.v b/theories/Raft/RequestVoteTermSanityInterface.v
similarity index 100%
rename from raft/RequestVoteTermSanityInterface.v
rename to theories/Raft/RequestVoteTermSanityInterface.v
diff --git a/raft/SortedInterface.v b/theories/Raft/SortedInterface.v
similarity index 100%
rename from raft/SortedInterface.v
rename to theories/Raft/SortedInterface.v
diff --git a/raft/SpecLemmas.v b/theories/Raft/SpecLemmas.v
similarity index 100%
rename from raft/SpecLemmas.v
rename to theories/Raft/SpecLemmas.v
diff --git a/raft/StateMachineCorrectInterface.v b/theories/Raft/StateMachineCorrectInterface.v
similarity index 100%
rename from raft/StateMachineCorrectInterface.v
rename to theories/Raft/StateMachineCorrectInterface.v
diff --git a/raft/StateMachineSafetyInterface.v b/theories/Raft/StateMachineSafetyInterface.v
similarity index 100%
rename from raft/StateMachineSafetyInterface.v
rename to theories/Raft/StateMachineSafetyInterface.v
diff --git a/raft/StateMachineSafetyPrimeInterface.v b/theories/Raft/StateMachineSafetyPrimeInterface.v
similarity index 100%
rename from raft/StateMachineSafetyPrimeInterface.v
rename to theories/Raft/StateMachineSafetyPrimeInterface.v
diff --git a/raft/StateTraceInvariant.v b/theories/Raft/StateTraceInvariant.v
similarity index 100%
rename from raft/StateTraceInvariant.v
rename to theories/Raft/StateTraceInvariant.v
diff --git a/raft/TermSanityInterface.v b/theories/Raft/TermSanityInterface.v
similarity index 100%
rename from raft/TermSanityInterface.v
rename to theories/Raft/TermSanityInterface.v
diff --git a/raft/TermsAndIndicesFromOneInterface.v b/theories/Raft/TermsAndIndicesFromOneInterface.v
similarity index 100%
rename from raft/TermsAndIndicesFromOneInterface.v
rename to theories/Raft/TermsAndIndicesFromOneInterface.v
diff --git a/raft/TermsAndIndicesFromOneLogInterface.v b/theories/Raft/TermsAndIndicesFromOneLogInterface.v
similarity index 100%
rename from raft/TermsAndIndicesFromOneLogInterface.v
rename to theories/Raft/TermsAndIndicesFromOneLogInterface.v
diff --git a/raft/TraceUtil.v b/theories/Raft/TraceUtil.v
similarity index 100%
rename from raft/TraceUtil.v
rename to theories/Raft/TraceUtil.v
diff --git a/raft/TransitiveCommitInterface.v b/theories/Raft/TransitiveCommitInterface.v
similarity index 100%
rename from raft/TransitiveCommitInterface.v
rename to theories/Raft/TransitiveCommitInterface.v
diff --git a/raft/UniqueIndicesInterface.v b/theories/Raft/UniqueIndicesInterface.v
similarity index 100%
rename from raft/UniqueIndicesInterface.v
rename to theories/Raft/UniqueIndicesInterface.v
diff --git a/raft/VotedForMoreUpToDateInterface.v b/theories/Raft/VotedForMoreUpToDateInterface.v
similarity index 100%
rename from raft/VotedForMoreUpToDateInterface.v
rename to theories/Raft/VotedForMoreUpToDateInterface.v
diff --git a/raft/VotedForTermSanityInterface.v b/theories/Raft/VotedForTermSanityInterface.v
similarity index 100%
rename from raft/VotedForTermSanityInterface.v
rename to theories/Raft/VotedForTermSanityInterface.v
diff --git a/raft/VotesCorrectInterface.v b/theories/Raft/VotesCorrectInterface.v
similarity index 100%
rename from raft/VotesCorrectInterface.v
rename to theories/Raft/VotesCorrectInterface.v
diff --git a/raft/VotesLeCurrentTermInterface.v b/theories/Raft/VotesLeCurrentTermInterface.v
similarity index 100%
rename from raft/VotesLeCurrentTermInterface.v
rename to theories/Raft/VotesLeCurrentTermInterface.v
diff --git a/raft/VotesReceivedMoreUpToDateInterface.v b/theories/Raft/VotesReceivedMoreUpToDateInterface.v
similarity index 100%
rename from raft/VotesReceivedMoreUpToDateInterface.v
rename to theories/Raft/VotesReceivedMoreUpToDateInterface.v
diff --git a/raft/VotesVotesWithLogCorrespondInterface.v b/theories/Raft/VotesVotesWithLogCorrespondInterface.v
similarity index 100%
rename from raft/VotesVotesWithLogCorrespondInterface.v
rename to theories/Raft/VotesVotesWithLogCorrespondInterface.v
diff --git a/raft/VotesWithLogSortedInterface.v b/theories/Raft/VotesWithLogSortedInterface.v
similarity index 100%
rename from raft/VotesWithLogSortedInterface.v
rename to theories/Raft/VotesWithLogSortedInterface.v
diff --git a/raft/VotesWithLogTermSanityInterface.v b/theories/Raft/VotesWithLogTermSanityInterface.v
similarity index 100%
rename from raft/VotesWithLogTermSanityInterface.v
rename to theories/Raft/VotesWithLogTermSanityInterface.v
diff --git a/raft-proofs/AllEntriesCandidateEntriesProof.v b/theories/RaftProofs/AllEntriesCandidateEntriesProof.v
similarity index 100%
rename from raft-proofs/AllEntriesCandidateEntriesProof.v
rename to theories/RaftProofs/AllEntriesCandidateEntriesProof.v
diff --git a/raft-proofs/AllEntriesIndicesGt0Proof.v b/theories/RaftProofs/AllEntriesIndicesGt0Proof.v
similarity index 100%
rename from raft-proofs/AllEntriesIndicesGt0Proof.v
rename to theories/RaftProofs/AllEntriesIndicesGt0Proof.v
diff --git a/raft-proofs/AllEntriesLeaderLogsProof.v b/theories/RaftProofs/AllEntriesLeaderLogsProof.v
similarity index 100%
rename from raft-proofs/AllEntriesLeaderLogsProof.v
rename to theories/RaftProofs/AllEntriesLeaderLogsProof.v
diff --git a/raft-proofs/AllEntriesLeaderLogsTermProof.v b/theories/RaftProofs/AllEntriesLeaderLogsTermProof.v
similarity index 100%
rename from raft-proofs/AllEntriesLeaderLogsTermProof.v
rename to theories/RaftProofs/AllEntriesLeaderLogsTermProof.v
diff --git a/raft-proofs/AllEntriesLeaderSublogProof.v b/theories/RaftProofs/AllEntriesLeaderSublogProof.v
similarity index 100%
rename from raft-proofs/AllEntriesLeaderSublogProof.v
rename to theories/RaftProofs/AllEntriesLeaderSublogProof.v
diff --git a/raft-proofs/AllEntriesLogMatchingProof.v b/theories/RaftProofs/AllEntriesLogMatchingProof.v
similarity index 100%
rename from raft-proofs/AllEntriesLogMatchingProof.v
rename to theories/RaftProofs/AllEntriesLogMatchingProof.v
diff --git a/raft-proofs/AllEntriesLogProof.v b/theories/RaftProofs/AllEntriesLogProof.v
similarity index 100%
rename from raft-proofs/AllEntriesLogProof.v
rename to theories/RaftProofs/AllEntriesLogProof.v
diff --git a/raft-proofs/AllEntriesTermSanityProof.v b/theories/RaftProofs/AllEntriesTermSanityProof.v
similarity index 100%
rename from raft-proofs/AllEntriesTermSanityProof.v
rename to theories/RaftProofs/AllEntriesTermSanityProof.v
diff --git a/raft-proofs/AllEntriesVotesWithLogProof.v b/theories/RaftProofs/AllEntriesVotesWithLogProof.v
similarity index 100%
rename from raft-proofs/AllEntriesVotesWithLogProof.v
rename to theories/RaftProofs/AllEntriesVotesWithLogProof.v
diff --git a/raft-proofs/AppendEntriesLeaderProof.v b/theories/RaftProofs/AppendEntriesLeaderProof.v
similarity index 100%
rename from raft-proofs/AppendEntriesLeaderProof.v
rename to theories/RaftProofs/AppendEntriesLeaderProof.v
diff --git a/raft-proofs/AppendEntriesReplySublogProof.v b/theories/RaftProofs/AppendEntriesReplySublogProof.v
similarity index 100%
rename from raft-proofs/AppendEntriesReplySublogProof.v
rename to theories/RaftProofs/AppendEntriesReplySublogProof.v
diff --git a/raft-proofs/AppendEntriesRequestLeaderLogsProof.v b/theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v
similarity index 100%
rename from raft-proofs/AppendEntriesRequestLeaderLogsProof.v
rename to theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v
diff --git a/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v b/theories/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.v
similarity index 100%
rename from raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v
rename to theories/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.v
diff --git a/raft-proofs/AppendEntriesRequestTermSanityProof.v b/theories/RaftProofs/AppendEntriesRequestTermSanityProof.v
similarity index 100%
rename from raft-proofs/AppendEntriesRequestTermSanityProof.v
rename to theories/RaftProofs/AppendEntriesRequestTermSanityProof.v
diff --git a/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v b/theories/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.v
similarity index 100%
rename from raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v
rename to theories/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.v
diff --git a/raft-proofs/AppliedEntriesMonotonicProof.v b/theories/RaftProofs/AppliedEntriesMonotonicProof.v
similarity index 100%
rename from raft-proofs/AppliedEntriesMonotonicProof.v
rename to theories/RaftProofs/AppliedEntriesMonotonicProof.v
diff --git a/raft-proofs/AppliedImpliesInputProof.v b/theories/RaftProofs/AppliedImpliesInputProof.v
similarity index 100%
rename from raft-proofs/AppliedImpliesInputProof.v
rename to theories/RaftProofs/AppliedImpliesInputProof.v
diff --git a/raft-proofs/CandidateEntriesProof.v b/theories/RaftProofs/CandidateEntriesProof.v
similarity index 100%
rename from raft-proofs/CandidateEntriesProof.v
rename to theories/RaftProofs/CandidateEntriesProof.v
diff --git a/raft-proofs/CandidateTermGtLogProof.v b/theories/RaftProofs/CandidateTermGtLogProof.v
similarity index 100%
rename from raft-proofs/CandidateTermGtLogProof.v
rename to theories/RaftProofs/CandidateTermGtLogProof.v
diff --git a/raft-proofs/CandidatesVoteForSelvesProof.v b/theories/RaftProofs/CandidatesVoteForSelvesProof.v
similarity index 100%
rename from raft-proofs/CandidatesVoteForSelvesProof.v
rename to theories/RaftProofs/CandidatesVoteForSelvesProof.v
diff --git a/raft-proofs/CausalOrderPreservedProof.v b/theories/RaftProofs/CausalOrderPreservedProof.v
similarity index 100%
rename from raft-proofs/CausalOrderPreservedProof.v
rename to theories/RaftProofs/CausalOrderPreservedProof.v
diff --git a/raft-proofs/CroniesCorrectProof.v b/theories/RaftProofs/CroniesCorrectProof.v
similarity index 100%
rename from raft-proofs/CroniesCorrectProof.v
rename to theories/RaftProofs/CroniesCorrectProof.v
diff --git a/raft-proofs/CroniesTermProof.v b/theories/RaftProofs/CroniesTermProof.v
similarity index 100%
rename from raft-proofs/CroniesTermProof.v
rename to theories/RaftProofs/CroniesTermProof.v
diff --git a/raft-proofs/CurrentTermGtZeroProof.v b/theories/RaftProofs/CurrentTermGtZeroProof.v
similarity index 100%
rename from raft-proofs/CurrentTermGtZeroProof.v
rename to theories/RaftProofs/CurrentTermGtZeroProof.v
diff --git a/raft-proofs/EndToEndLinearizability.v b/theories/RaftProofs/EndToEndLinearizability.v
similarity index 100%
rename from raft-proofs/EndToEndLinearizability.v
rename to theories/RaftProofs/EndToEndLinearizability.v
diff --git a/raft-proofs/EveryEntryWasCreatedHostLogProof.v b/theories/RaftProofs/EveryEntryWasCreatedHostLogProof.v
similarity index 100%
rename from raft-proofs/EveryEntryWasCreatedHostLogProof.v
rename to theories/RaftProofs/EveryEntryWasCreatedHostLogProof.v
diff --git a/raft-proofs/EveryEntryWasCreatedProof.v b/theories/RaftProofs/EveryEntryWasCreatedProof.v
similarity index 100%
rename from raft-proofs/EveryEntryWasCreatedProof.v
rename to theories/RaftProofs/EveryEntryWasCreatedProof.v
diff --git a/raft-proofs/GhostLogAllEntriesProof.v b/theories/RaftProofs/GhostLogAllEntriesProof.v
similarity index 100%
rename from raft-proofs/GhostLogAllEntriesProof.v
rename to theories/RaftProofs/GhostLogAllEntriesProof.v
diff --git a/raft-proofs/GhostLogCorrectProof.v b/theories/RaftProofs/GhostLogCorrectProof.v
similarity index 100%
rename from raft-proofs/GhostLogCorrectProof.v
rename to theories/RaftProofs/GhostLogCorrectProof.v
diff --git a/raft-proofs/GhostLogLogMatchingProof.v b/theories/RaftProofs/GhostLogLogMatchingProof.v
similarity index 100%
rename from raft-proofs/GhostLogLogMatchingProof.v
rename to theories/RaftProofs/GhostLogLogMatchingProof.v
diff --git a/raft-proofs/GhostLogsLogPropertiesProof.v b/theories/RaftProofs/GhostLogsLogPropertiesProof.v
similarity index 100%
rename from raft-proofs/GhostLogsLogPropertiesProof.v
rename to theories/RaftProofs/GhostLogsLogPropertiesProof.v
diff --git a/raft-proofs/InLogInAllEntriesProof.v b/theories/RaftProofs/InLogInAllEntriesProof.v
similarity index 100%
rename from raft-proofs/InLogInAllEntriesProof.v
rename to theories/RaftProofs/InLogInAllEntriesProof.v
diff --git a/raft-proofs/InputBeforeOutputProof.v b/theories/RaftProofs/InputBeforeOutputProof.v
similarity index 100%
rename from raft-proofs/InputBeforeOutputProof.v
rename to theories/RaftProofs/InputBeforeOutputProof.v
diff --git a/raft-proofs/LastAppliedCommitIndexMatchingProof.v b/theories/RaftProofs/LastAppliedCommitIndexMatchingProof.v
similarity index 100%
rename from raft-proofs/LastAppliedCommitIndexMatchingProof.v
rename to theories/RaftProofs/LastAppliedCommitIndexMatchingProof.v
diff --git a/raft-proofs/LastAppliedLeCommitIndexProof.v b/theories/RaftProofs/LastAppliedLeCommitIndexProof.v
similarity index 100%
rename from raft-proofs/LastAppliedLeCommitIndexProof.v
rename to theories/RaftProofs/LastAppliedLeCommitIndexProof.v
diff --git a/raft-proofs/LeaderCompletenessProof.v b/theories/RaftProofs/LeaderCompletenessProof.v
similarity index 100%
rename from raft-proofs/LeaderCompletenessProof.v
rename to theories/RaftProofs/LeaderCompletenessProof.v
diff --git a/raft-proofs/LeaderLogsCandidateEntriesProof.v b/theories/RaftProofs/LeaderLogsCandidateEntriesProof.v
similarity index 100%
rename from raft-proofs/LeaderLogsCandidateEntriesProof.v
rename to theories/RaftProofs/LeaderLogsCandidateEntriesProof.v
diff --git a/raft-proofs/LeaderLogsContiguousProof.v b/theories/RaftProofs/LeaderLogsContiguousProof.v
similarity index 100%
rename from raft-proofs/LeaderLogsContiguousProof.v
rename to theories/RaftProofs/LeaderLogsContiguousProof.v
diff --git a/raft-proofs/LeaderLogsLogMatchingProof.v b/theories/RaftProofs/LeaderLogsLogMatchingProof.v
similarity index 100%
rename from raft-proofs/LeaderLogsLogMatchingProof.v
rename to theories/RaftProofs/LeaderLogsLogMatchingProof.v
diff --git a/raft-proofs/LeaderLogsLogPropertiesProof.v b/theories/RaftProofs/LeaderLogsLogPropertiesProof.v
similarity index 100%
rename from raft-proofs/LeaderLogsLogPropertiesProof.v
rename to theories/RaftProofs/LeaderLogsLogPropertiesProof.v
diff --git a/raft-proofs/LeaderLogsPreservedProof.v b/theories/RaftProofs/LeaderLogsPreservedProof.v
similarity index 100%
rename from raft-proofs/LeaderLogsPreservedProof.v
rename to theories/RaftProofs/LeaderLogsPreservedProof.v
diff --git a/raft-proofs/LeaderLogsSortedProof.v b/theories/RaftProofs/LeaderLogsSortedProof.v
similarity index 100%
rename from raft-proofs/LeaderLogsSortedProof.v
rename to theories/RaftProofs/LeaderLogsSortedProof.v
diff --git a/raft-proofs/LeaderLogsSublogProof.v b/theories/RaftProofs/LeaderLogsSublogProof.v
similarity index 100%
rename from raft-proofs/LeaderLogsSublogProof.v
rename to theories/RaftProofs/LeaderLogsSublogProof.v
diff --git a/raft-proofs/LeaderLogsTermSanityProof.v b/theories/RaftProofs/LeaderLogsTermSanityProof.v
similarity index 100%
rename from raft-proofs/LeaderLogsTermSanityProof.v
rename to theories/RaftProofs/LeaderLogsTermSanityProof.v
diff --git a/raft-proofs/LeaderLogsVotesWithLogProof.v b/theories/RaftProofs/LeaderLogsVotesWithLogProof.v
similarity index 100%
rename from raft-proofs/LeaderLogsVotesWithLogProof.v
rename to theories/RaftProofs/LeaderLogsVotesWithLogProof.v
diff --git a/raft-proofs/LeaderSublogProof.v b/theories/RaftProofs/LeaderSublogProof.v
similarity index 100%
rename from raft-proofs/LeaderSublogProof.v
rename to theories/RaftProofs/LeaderSublogProof.v
diff --git a/raft-proofs/LeadersHaveLeaderLogsProof.v b/theories/RaftProofs/LeadersHaveLeaderLogsProof.v
similarity index 100%
rename from raft-proofs/LeadersHaveLeaderLogsProof.v
rename to theories/RaftProofs/LeadersHaveLeaderLogsProof.v
diff --git a/raft-proofs/LeadersHaveLeaderLogsStrongProof.v b/theories/RaftProofs/LeadersHaveLeaderLogsStrongProof.v
similarity index 100%
rename from raft-proofs/LeadersHaveLeaderLogsStrongProof.v
rename to theories/RaftProofs/LeadersHaveLeaderLogsStrongProof.v
diff --git a/raft-proofs/LogAllEntriesProof.v b/theories/RaftProofs/LogAllEntriesProof.v
similarity index 100%
rename from raft-proofs/LogAllEntriesProof.v
rename to theories/RaftProofs/LogAllEntriesProof.v
diff --git a/raft-proofs/LogMatchingProof.v b/theories/RaftProofs/LogMatchingProof.v
similarity index 100%
rename from raft-proofs/LogMatchingProof.v
rename to theories/RaftProofs/LogMatchingProof.v
diff --git a/raft-proofs/LogsLeaderLogsProof.v b/theories/RaftProofs/LogsLeaderLogsProof.v
similarity index 100%
rename from raft-proofs/LogsLeaderLogsProof.v
rename to theories/RaftProofs/LogsLeaderLogsProof.v
diff --git a/raft-proofs/MatchIndexAllEntriesProof.v b/theories/RaftProofs/MatchIndexAllEntriesProof.v
similarity index 100%
rename from raft-proofs/MatchIndexAllEntriesProof.v
rename to theories/RaftProofs/MatchIndexAllEntriesProof.v
diff --git a/raft-proofs/MatchIndexLeaderProof.v b/theories/RaftProofs/MatchIndexLeaderProof.v
similarity index 100%
rename from raft-proofs/MatchIndexLeaderProof.v
rename to theories/RaftProofs/MatchIndexLeaderProof.v
diff --git a/raft-proofs/MatchIndexSanityProof.v b/theories/RaftProofs/MatchIndexSanityProof.v
similarity index 100%
rename from raft-proofs/MatchIndexSanityProof.v
rename to theories/RaftProofs/MatchIndexSanityProof.v
diff --git a/raft-proofs/NextIndexSafetyProof.v b/theories/RaftProofs/NextIndexSafetyProof.v
similarity index 100%
rename from raft-proofs/NextIndexSafetyProof.v
rename to theories/RaftProofs/NextIndexSafetyProof.v
diff --git a/raft-proofs/NoAppendEntriesRepliesToSelfProof.v b/theories/RaftProofs/NoAppendEntriesRepliesToSelfProof.v
similarity index 100%
rename from raft-proofs/NoAppendEntriesRepliesToSelfProof.v
rename to theories/RaftProofs/NoAppendEntriesRepliesToSelfProof.v
diff --git a/raft-proofs/NoAppendEntriesToLeaderProof.v b/theories/RaftProofs/NoAppendEntriesToLeaderProof.v
similarity index 100%
rename from raft-proofs/NoAppendEntriesToLeaderProof.v
rename to theories/RaftProofs/NoAppendEntriesToLeaderProof.v
diff --git a/raft-proofs/NoAppendEntriesToSelfProof.v b/theories/RaftProofs/NoAppendEntriesToSelfProof.v
similarity index 100%
rename from raft-proofs/NoAppendEntriesToSelfProof.v
rename to theories/RaftProofs/NoAppendEntriesToSelfProof.v
diff --git a/raft-proofs/OneLeaderLogPerTermProof.v b/theories/RaftProofs/OneLeaderLogPerTermProof.v
similarity index 100%
rename from raft-proofs/OneLeaderLogPerTermProof.v
rename to theories/RaftProofs/OneLeaderLogPerTermProof.v
diff --git a/raft-proofs/OneLeaderPerTermProof.v b/theories/RaftProofs/OneLeaderPerTermProof.v
similarity index 100%
rename from raft-proofs/OneLeaderPerTermProof.v
rename to theories/RaftProofs/OneLeaderPerTermProof.v
diff --git a/raft-proofs/OutputCorrectProof.v b/theories/RaftProofs/OutputCorrectProof.v
similarity index 100%
rename from raft-proofs/OutputCorrectProof.v
rename to theories/RaftProofs/OutputCorrectProof.v
diff --git a/raft-proofs/OutputGreatestIdProof.v b/theories/RaftProofs/OutputGreatestIdProof.v
similarity index 100%
rename from raft-proofs/OutputGreatestIdProof.v
rename to theories/RaftProofs/OutputGreatestIdProof.v
diff --git a/raft-proofs/OutputImpliesAppliedProof.v b/theories/RaftProofs/OutputImpliesAppliedProof.v
similarity index 100%
rename from raft-proofs/OutputImpliesAppliedProof.v
rename to theories/RaftProofs/OutputImpliesAppliedProof.v
diff --git a/raft-proofs/PrefixWithinTermProof.v b/theories/RaftProofs/PrefixWithinTermProof.v
similarity index 100%
rename from raft-proofs/PrefixWithinTermProof.v
rename to theories/RaftProofs/PrefixWithinTermProof.v
diff --git a/raft-proofs/PrevLogCandidateEntriesTermProof.v b/theories/RaftProofs/PrevLogCandidateEntriesTermProof.v
similarity index 100%
rename from raft-proofs/PrevLogCandidateEntriesTermProof.v
rename to theories/RaftProofs/PrevLogCandidateEntriesTermProof.v
diff --git a/raft-proofs/PrevLogLeaderSublogProof.v b/theories/RaftProofs/PrevLogLeaderSublogProof.v
similarity index 100%
rename from raft-proofs/PrevLogLeaderSublogProof.v
rename to theories/RaftProofs/PrevLogLeaderSublogProof.v
diff --git a/raft-proofs/RaftMsgRefinementProof.v b/theories/RaftProofs/RaftMsgRefinementProof.v
similarity index 100%
rename from raft-proofs/RaftMsgRefinementProof.v
rename to theories/RaftProofs/RaftMsgRefinementProof.v
diff --git a/raft-proofs/RaftRefinementProof.v b/theories/RaftProofs/RaftRefinementProof.v
similarity index 100%
rename from raft-proofs/RaftRefinementProof.v
rename to theories/RaftProofs/RaftRefinementProof.v
diff --git a/raft-proofs/RefinedLogMatchingLemmasProof.v b/theories/RaftProofs/RefinedLogMatchingLemmasProof.v
similarity index 100%
rename from raft-proofs/RefinedLogMatchingLemmasProof.v
rename to theories/RaftProofs/RefinedLogMatchingLemmasProof.v
diff --git a/raft-proofs/RequestVoteMaxIndexMaxTermProof.v b/theories/RaftProofs/RequestVoteMaxIndexMaxTermProof.v
similarity index 100%
rename from raft-proofs/RequestVoteMaxIndexMaxTermProof.v
rename to theories/RaftProofs/RequestVoteMaxIndexMaxTermProof.v
diff --git a/raft-proofs/RequestVoteReplyMoreUpToDateProof.v b/theories/RaftProofs/RequestVoteReplyMoreUpToDateProof.v
similarity index 100%
rename from raft-proofs/RequestVoteReplyMoreUpToDateProof.v
rename to theories/RaftProofs/RequestVoteReplyMoreUpToDateProof.v
diff --git a/raft-proofs/RequestVoteReplyTermSanityProof.v b/theories/RaftProofs/RequestVoteReplyTermSanityProof.v
similarity index 100%
rename from raft-proofs/RequestVoteReplyTermSanityProof.v
rename to theories/RaftProofs/RequestVoteReplyTermSanityProof.v
diff --git a/raft-proofs/RequestVoteTermSanityProof.v b/theories/RaftProofs/RequestVoteTermSanityProof.v
similarity index 100%
rename from raft-proofs/RequestVoteTermSanityProof.v
rename to theories/RaftProofs/RequestVoteTermSanityProof.v
diff --git a/raft-proofs/SortedProof.v b/theories/RaftProofs/SortedProof.v
similarity index 100%
rename from raft-proofs/SortedProof.v
rename to theories/RaftProofs/SortedProof.v
diff --git a/raft-proofs/StateMachineCorrectProof.v b/theories/RaftProofs/StateMachineCorrectProof.v
similarity index 100%
rename from raft-proofs/StateMachineCorrectProof.v
rename to theories/RaftProofs/StateMachineCorrectProof.v
diff --git a/raft-proofs/StateMachineSafetyPrimeProof.v b/theories/RaftProofs/StateMachineSafetyPrimeProof.v
similarity index 100%
rename from raft-proofs/StateMachineSafetyPrimeProof.v
rename to theories/RaftProofs/StateMachineSafetyPrimeProof.v
diff --git a/raft-proofs/StateMachineSafetyProof.v b/theories/RaftProofs/StateMachineSafetyProof.v
similarity index 100%
rename from raft-proofs/StateMachineSafetyProof.v
rename to theories/RaftProofs/StateMachineSafetyProof.v
diff --git a/raft-proofs/TermSanityProof.v b/theories/RaftProofs/TermSanityProof.v
similarity index 100%
rename from raft-proofs/TermSanityProof.v
rename to theories/RaftProofs/TermSanityProof.v
diff --git a/raft-proofs/TermsAndIndicesFromOneLogProof.v b/theories/RaftProofs/TermsAndIndicesFromOneLogProof.v
similarity index 100%
rename from raft-proofs/TermsAndIndicesFromOneLogProof.v
rename to theories/RaftProofs/TermsAndIndicesFromOneLogProof.v
diff --git a/raft-proofs/TermsAndIndicesFromOneProof.v b/theories/RaftProofs/TermsAndIndicesFromOneProof.v
similarity index 100%
rename from raft-proofs/TermsAndIndicesFromOneProof.v
rename to theories/RaftProofs/TermsAndIndicesFromOneProof.v
diff --git a/raft-proofs/TransitiveCommitProof.v b/theories/RaftProofs/TransitiveCommitProof.v
similarity index 100%
rename from raft-proofs/TransitiveCommitProof.v
rename to theories/RaftProofs/TransitiveCommitProof.v
diff --git a/raft-proofs/UniqueIndicesProof.v b/theories/RaftProofs/UniqueIndicesProof.v
similarity index 100%
rename from raft-proofs/UniqueIndicesProof.v
rename to theories/RaftProofs/UniqueIndicesProof.v
diff --git a/raft-proofs/VotedForMoreUpToDateProof.v b/theories/RaftProofs/VotedForMoreUpToDateProof.v
similarity index 100%
rename from raft-proofs/VotedForMoreUpToDateProof.v
rename to theories/RaftProofs/VotedForMoreUpToDateProof.v
diff --git a/raft-proofs/VotedForTermSanityProof.v b/theories/RaftProofs/VotedForTermSanityProof.v
similarity index 100%
rename from raft-proofs/VotedForTermSanityProof.v
rename to theories/RaftProofs/VotedForTermSanityProof.v
diff --git a/raft-proofs/VotesCorrectProof.v b/theories/RaftProofs/VotesCorrectProof.v
similarity index 100%
rename from raft-proofs/VotesCorrectProof.v
rename to theories/RaftProofs/VotesCorrectProof.v
diff --git a/raft-proofs/VotesLeCurrentTermProof.v b/theories/RaftProofs/VotesLeCurrentTermProof.v
similarity index 100%
rename from raft-proofs/VotesLeCurrentTermProof.v
rename to theories/RaftProofs/VotesLeCurrentTermProof.v
diff --git a/raft-proofs/VotesReceivedMoreUpToDateProof.v b/theories/RaftProofs/VotesReceivedMoreUpToDateProof.v
similarity index 100%
rename from raft-proofs/VotesReceivedMoreUpToDateProof.v
rename to theories/RaftProofs/VotesReceivedMoreUpToDateProof.v
diff --git a/raft-proofs/VotesVotesWithLogCorrespondProof.v b/theories/RaftProofs/VotesVotesWithLogCorrespondProof.v
similarity index 100%
rename from raft-proofs/VotesVotesWithLogCorrespondProof.v
rename to theories/RaftProofs/VotesVotesWithLogCorrespondProof.v
diff --git a/raft-proofs/VotesWithLogSortedProof.v b/theories/RaftProofs/VotesWithLogSortedProof.v
similarity index 100%
rename from raft-proofs/VotesWithLogSortedProof.v
rename to theories/RaftProofs/VotesWithLogSortedProof.v
diff --git a/raft-proofs/VotesWithLogTermSanityProof.v b/theories/RaftProofs/VotesWithLogTermSanityProof.v
similarity index 100%
rename from raft-proofs/VotesWithLogTermSanityProof.v
rename to theories/RaftProofs/VotesWithLogTermSanityProof.v
diff --git a/systems/VarDRaft.v b/theories/Systems/VarDRaft.v
similarity index 100%
rename from systems/VarDRaft.v
rename to theories/Systems/VarDRaft.v
diff --git a/systems/VarDRaftCorrect.v b/theories/Systems/VarDRaftCorrect.v
similarity index 100%
rename from systems/VarDRaftCorrect.v
rename to theories/Systems/VarDRaftCorrect.v
diff --git a/systems/VarDRaftLog.v b/theories/Systems/VarDRaftLog.v
similarity index 100%
rename from systems/VarDRaftLog.v
rename to theories/Systems/VarDRaftLog.v
diff --git a/systems/VarDRaftLogCorrect.v b/theories/Systems/VarDRaftLogCorrect.v
similarity index 100%
rename from systems/VarDRaftLogCorrect.v
rename to theories/Systems/VarDRaftLogCorrect.v
diff --git a/systems/VarDRaftSerialized.v b/theories/Systems/VarDRaftSerialized.v
similarity index 100%
rename from systems/VarDRaftSerialized.v
rename to theories/Systems/VarDRaftSerialized.v
diff --git a/systems/VarDRaftSerializedCorrect.v b/theories/Systems/VarDRaftSerializedCorrect.v
similarity index 100%
rename from systems/VarDRaftSerializedCorrect.v
rename to theories/Systems/VarDRaftSerializedCorrect.v
diff --git a/systems/VarDRaftSerializedLog.v b/theories/Systems/VarDRaftSerializedLog.v
similarity index 100%
rename from systems/VarDRaftSerializedLog.v
rename to theories/Systems/VarDRaftSerializedLog.v
diff --git a/systems/VarDRaftSerializedLogCorrect.v b/theories/Systems/VarDRaftSerializedLogCorrect.v
similarity index 100%
rename from systems/VarDRaftSerializedLogCorrect.v
rename to theories/Systems/VarDRaftSerializedLogCorrect.v
diff --git a/systems/VarDRaftSerializers.v b/theories/Systems/VarDRaftSerializers.v
similarity index 100%
rename from systems/VarDRaftSerializers.v
rename to theories/Systems/VarDRaftSerializers.v
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000..4ae0b2c
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name VerdiRaft)
+ (package coq-verdi-raft)
+ (synopsis "Verified implementation of the Raft distributed consensus protocol in Coq"))
+
+(include_subdirs qualified)