diff --git a/README.md b/README.md
index e7818021..b7f9da5a 100644
--- a/README.md
+++ b/README.md
@@ -11,9 +11,15 @@
 [coqdoc-link]: https://runtimeverification.github.io/vlsm-docs/latest/coqdoc/toc.html
 
 
-A validating labelled state transition and message production system
-(VLSM) abstractly models a distributed system with faults. This project
-contains a formalization of VLSMs and their theory in the Coq proof assistant.
+The theory of Validating Labelled State transition and Message
+production systems (VLSMs) can be used to abstractly describe
+and prove properties of distributed systems executing in
+the presence of faults. This project contains a formalization
+of this theory in the Coq proof assistant along with several
+examples of distributed protocols modeled and verified using VLSMs,
+including the ELMO (Equivocation-Limited Message Observer)
+family of message validating protocols and the Paxos protocol
+for crash-tolerant distributed consensus.
 
 ## Meta
 
diff --git a/coq-vlsm.opam b/coq-vlsm.opam
index 87029c01..217eef01 100644
--- a/coq-vlsm.opam
+++ b/coq-vlsm.opam
@@ -9,9 +9,15 @@ license: "BSD-3-Clause"
 
 synopsis: "Coq formalization of validating labelled state transition and message production systems"
 description: """
-A validating labelled state transition and message production system
-(VLSM) abstractly models a distributed system with faults. This project
-contains a formalization of VLSMs and their theory in the Coq proof assistant."""
+The theory of Validating Labelled State transition and Message
+production systems (VLSMs) can be used to abstractly describe
+and prove properties of distributed systems executing in
+the presence of faults. This project contains a formalization
+of this theory in the Coq proof assistant along with several
+examples of distributed protocols modeled and verified using VLSMs,
+including the ELMO (Equivocation-Limited Message Observer)
+family of message validating protocols and the Paxos protocol
+for crash-tolerant distributed consensus."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
diff --git a/meta.yml b/meta.yml
index 725f0154..31747c07 100644
--- a/meta.yml
+++ b/meta.yml
@@ -12,9 +12,15 @@ synopsis: >-
   and message production systems
 
 description: |-
-  A validating labelled state transition and message production system
-  (VLSM) abstractly models a distributed system with faults. This project
-  contains a formalization of VLSMs and their theory in the Coq proof assistant.
+  The theory of Validating Labelled State transition and Message
+  production systems (VLSMs) can be used to abstractly describe
+  and prove properties of distributed systems executing in
+  the presence of faults. This project contains a formalization
+  of this theory in the Coq proof assistant along with several
+  examples of distributed protocols modeled and verified using VLSMs,
+  including the ELMO (Equivocation-Limited Message Observer)
+  family of message validating protocols and the Paxos protocol
+  for crash-tolerant distributed consensus.
 
 publications:
 - pub_doi: 10.48550/arXiv.2202.12662