diff --git a/PutAndVerify/MC.cfg b/PutAndVerify/MC.cfg
new file mode 100755
index 0000000..3e9d5cb
--- /dev/null
+++ b/PutAndVerify/MC.cfg
@@ -0,0 +1,23 @@
+\* MV CONSTANT declarations
+CONSTANTS
+Alice = Alice
+Bob = Bob
+\* MV CONSTANT definitions
+CONSTANT
+CLIENTS <- const_172889209848054000
+\* SYMMETRY definition
+SYMMETRY symm_172889209848055000
+\* CONSTANT definitions
+CONSTANT
+WITH_CRASHING <- const_172889209848056000
+\* CONSTANT definitions
+CONSTANT
+WITH_RO <- const_172889209848057000
+\* SPECIFICATION definition
+SPECIFICATION
+WVSpec
+\* INVARIANT definition
+INVARIANT
+WVConsistency
+WVTypeOk
+\* Generated on Mon Oct 14 15:48:18 CST 2024
diff --git a/PutAndVerify/MC.tla b/PutAndVerify/MC.tla
new file mode 100755
index 0000000..0540603
--- /dev/null
+++ b/PutAndVerify/MC.tla
@@ -0,0 +1,32 @@
+---- MODULE MC ----
+EXTENDS WriteAndVerify, TLC
+
+\* MV CONSTANT declarations@modelParameterConstants
+CONSTANTS
+Alice, Bob
+----
+
+\* MV CONSTANT definitions CLIENTS
+const_172889209848054000 == 
+{Alice, Bob}
+----
+
+\* SYMMETRY definition
+symm_172889209848055000 == 
+Permutations(const_172889209848054000)
+----
+
+\* CONSTANT definitions @modelParameterConstants:1WITH_CRASHING
+const_172889209848056000 == 
+FALSE
+----
+
+\* CONSTANT definitions @modelParameterConstants:2WITH_RO
+const_172889209848057000 == 
+FALSE
+----
+
+=============================================================================
+\* Modification History
+\* Created Mon Oct 14 15:48:18 CST 2024 by Hillium
+
diff --git a/PutAndVerify/README.md b/PutAndVerify/README.md
new file mode 100644
index 0000000..2db2ef3
--- /dev/null
+++ b/PutAndVerify/README.md
@@ -0,0 +1,10 @@
+# Put and Verify Committing
+
+This algorithm allows you write to a file exactly-once in a object storage 
+supports `PUT` and `LIST` and the two operations have strong consistency.
+
+The model constants:
+
+- `CLIENTS`: The participants of the algorithm.
+- `WITH_CRASHING`: Allow any of participants crash after sending a write message before receiving a response.
+- `WITH_RO`: Allow "read-only" clients to participate. The algorithm then becomes a `RWLock` implementation: *many of "read-only" clients commit* or *exactly one of "read-write" client commits*.
\ No newline at end of file
diff --git a/PutAndVerify/WriteAndVerify.tla b/PutAndVerify/WriteAndVerify.tla
new file mode 100755
index 0000000..aa8e068
--- /dev/null
+++ b/PutAndVerify/WriteAndVerify.tla
@@ -0,0 +1,92 @@
+--------------------------- MODULE WriteAndVerify ---------------------------
+
+CONSTANT CLIENTS, WITH_RO, WITH_CRASHING
+
+VARIABLE storage, clState, clFavor
+
+Vars == << storage, clState, clFavor >>
+
+WVTypeOk == /\ storage \in [ CLIENTS -> { "none", "empty", "written", "written-ro", "empty-ro" } ]
+            /\ clState \in [ CLIENTS -> { "begin", "precheck-done", "blank-written", 
+                                          "write-check-done", "committed", "aborted", "crashed" } ]
+            /\ clFavor \in [ CLIENTS -> { "read-write", "read-only" } ]
+
+WVInit == /\ storage = [ cli \in CLIENTS |-> "none" ]
+          /\ clState = [ cli \in CLIENTS |-> "begin" ]
+          /\ clFavor = [ cli \in CLIENTS |-> "read-write" ]
+
+(* Only one execution can be committed. *)
+(* Once committed, the file has been written. *)
+WVConsistency == /\ \A i, j \in CLIENTS : 
+                    i /= j /\ storage[i] = "written" => ~storage[j] \in { "written", "written-ro" }
+
+(* "Verify" condition: storage only contains our file or nothing. *)
+Check(c) == /\ clFavor[c] = "read-write" =>
+               \A f \in CLIENTS : f /= c => storage[f] = "none"
+            /\ clFavor[c] = "read-only" =>
+               (* No conflicting write. *)
+                \A f \in CLIENTS : f /= c => ~storage[f] \in { "empty", "written" }  
+
+Precheck(c) ==    /\ clState[c] = "begin" 
+                  /\ IF Check(c) 
+                     THEN clState' = [ clState EXCEPT ![c] = "precheck-done" ]
+                     ELSE clState' = [ clState EXCEPT ![c] = "aborted" ]
+                  /\ UNCHANGED << storage, clFavor >>
+
+IsRO(c) == clFavor[c] = "read-only"
+
+DoWriteBlank(c) == /\ clState[c] = "precheck-done"
+                   /\ storage' = [ storage EXCEPT ![c] = IF IsRO(c) THEN "empty-ro" ELSE "empty" ]
+                   
+WriteBlank(c) == /\ DoWriteBlank(c)
+                 /\ clState' = [ clState EXCEPT ![c] = "blank-written" ]
+                 /\ UNCHANGED << clFavor >>
+                 
+
+ConflictCheck(c) == /\ clState[c] = "blank-written" 
+                    /\ IF Check(c) 
+                       THEN clState' = [ clState EXCEPT ![c] = "write-check-done" ]
+                       ELSE clState' = [ clState EXCEPT ![c] = "aborted" ]
+                    /\ UNCHANGED << storage, clFavor >>
+                    
+(* Delete the file when aborted. *)
+RollBack(c) == /\ clState[c] = "aborted"
+               /\ storage[c] /= "none"
+               /\ storage' = [ storage EXCEPT ![c] = "none" ]
+               /\ clState' = [ clState EXCEPT ![c] = "begin" ]
+               /\ UNCHANGED << clFavor >>
+
+DoCommit(c) == /\ clState[c] = "write-check-done"
+               /\ storage' = [ storage EXCEPT ![c] = IF IsRO(c) THEN "written-ro" ELSE "written" ]
+             
+Commit(c) == /\ DoCommit(c)
+             /\ clState' = [ clState EXCEPT ![c] = "committed" ]
+             /\ UNCHANGED << clFavor >>
+             
+BeRO(c) == /\ clState[c] = "begin"
+           /\ clFavor[c] = "read-write"
+           /\ clFavor' = [ clFavor EXCEPT ![c] = "read-only" ]
+           /\ UNCHANGED << clState, storage >>
+           
+WrittenAndCrash(c) == /\ clState' = [ clState EXCEPT ![c] = "crashed" ]
+                      /\ DoWriteBlank(c) \/ DoCommit(c)
+                      /\ UNCHANGED << clFavor >>
+                      
+
+WVNext == \E c \in CLIENTS: \/ Precheck(c)
+                            \/ WriteBlank(c)
+                            \/ ConflictCheck(c)
+                            \/ RollBack(c)
+                            \/ Commit(c)
+                            \/ WITH_CRASHING /\ WrittenAndCrash(c)
+                            \/ WITH_RO /\ BeRO(c)
+                            
+
+WVSpec == WVInit /\ [][WVNext]_Vars
+                    
+THEOREM WVSpec => [](WVConsistency /\ WVTypeOk)
+               
+=============================================================================
+\* Modification History
+\* Last modified Wed Dec 18 14:00:06 CST 2024 by Hillium
+\* Created Sat Jun 29 10:41:34 CST 2024 by Hillium