Thinking about a random number generator: Part 1 | Protocols Made Fun

[giscus[bot]]

Thinking about a random number generator: Part 1 | Protocols Made Fun

Foreword. This is my first blog post about protocol specification since I have left Informal Systems. Having a bit of free time on my hands, I want to show everyone how to think about code and protocols with specification languages such as TLA+ and Quint as well as with tools such as Apalache and TLC. There are no patented methods behind. What I am explaining is common knowledge in computer-aided verification and model checking. As is the case with programming languages, you just need to practice and get a bit of expertise in using these tools. Obviously, I am biased towards Quint and Apalache. I believe both projects are great, but it’s not my job to sell them to you 🍸.

https://protocols-made-fun.com/quint/2024/01/04/prng-part1.html