<p>You can find a formal model and proof of Paxos and Byzantine Paxos written by L. Lamport et al at <a href="http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html" rel="nofollow">http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html</a>. </p>

<p>The model can be checked using the <a href="http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html" rel="nofollow">TLA+ toolbox</a>.</p>

<p>Notice that the author of the Paxos algorithm, the formal model above, and even the TLA+ modeling language is the same person:)</p>

CC BY-SA 3.0
2013-06-16T19:12:30.703Z
2013-06-16T19:12:30.703Z
marcmagransdeabril
<p>I think you can get a better idea by referring the following paper,
Model Checking for Programming Languages using VeriSoft by Patrice Godefroid</p>

CC BY-SA 3.0
2013-06-17T02:47:51.313Z
I have not downvoted but please avoid from providing such generic answers which are not specific to the question being asked.
Vijay D
CC BY-SA 3.0
2012-06-09T04:07:24.107Z
2012-06-09T04:07:24.107Z
ModelChecker
<p>I have implemented consensus algorithm (based on Paxos). I have added some random test cases and it seems fine. To be sure, I want to do testing via model checking. I couldn't find a correct article for it. Are there any standard references on how to do model checking for Paxos?</p>

CC BY-SA 3.0
2013-06-17T02:49:14.273Z
Have you tried a Google search with the title of your question? There are several related articles. Have you read them? If they do not answer your question, please point out why.
Vijay D
<reference-request><dc.distributed-comp><model-checking>
Model checking Paxos
mohan
# Model checking Paxos

(Asked by: username_0 on 2012-06-08)

I have implemented consensus algorithm (based on Paxos). I have added some random test cases and it seems fine. To be sure, I want to do testing via model checking. I couldn't find a correct article for it. Are there any standard references on how to do model checking for Paxos?

**Tags:** reference-request, dc.distributed-comp, model-checking
> **Comments:**
> **username_1**: Have you tried a Google search with the title of your question? There are several related articles. Have you read them? If they do not answer your question, please point out why.  

---

## 2 answers

### Answer by username_2 on 2013-06-16. Score: 2

You can find a formal model and proof of Paxos and Byzantine Paxos written by L. Lamport et al at <http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html>.

The model can be checked using the [TLA+ toolbox](http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).

Notice that the author of the Paxos algorithm, the formal model above, and even the TLA+ modeling language is the same person:)


---

### Answer by username_3 on 2012-06-09. Score: -1

I think you can get a better idea by referring the following paper,
Model Checking for Programming Languages using VeriSoft by Patrice Godefroid

> **Comments:**
> **username_1**: I have not downvoted but please avoid from providing such generic answers which are not specific to the question being asked.  

---

