Implementing Fast Tendermint in Malachite with Quint and LLM

We have recently worked on a protocol we call Fast Tendermint, for people familiar with BFT consensus literature, "a la Fast Byzantine Consensus", https://lnkd.in/djVBcrjz. We believe that this version of Tendermint will be a very interesting choice for PoA setups needing low latency/high throughput. But this post is not about Fast Tendermint; it is about our approach in implementing Fast Tendermint in the Malachite. Namely, we have challenged ourselves to do this non-trivial protocol/implementation change to the Malachite codebase in less than a week's time, leveraging Quint and an LLM tool, and following a novel process/tolling we find super promising. TLDR: the experiment was successful and the results are very promising, and you can read more about it in the post below. But I want to share a few interesting points which came from this exercise that people might find useful. First, the strongest feedback and feeling from the team was that they are tired of "coding in English" and reading generated code, and that they want to write some real code and use proper tools for it 😀 Second, they have been frustrated by the nondeterministic output of the LLM (even in scenarios which from a human perspective seem very easy), and we have an internal joke that we are back to "it works on my machine" time; although it is actually more "it works in my session", but even that is not consistently the case 🙃 . Don't get me wrong, LLMs are amazing, and you can read in the post what the areas are where it really works great, but it is not a silver bullet (at least not yet), and this exercise has shown us areas where things can be improved and we can bring value. At Informal, we feel very strongly that English (natural language) is not the right tool to guide and constrain LLMs, and that Quint has a lot to offer in that context. And we are doubling down on this and developing more tools that will address issues we have observed and strengthen the good sides further as well. If you are working on distributed systems (consensus/blockchain/database systems) or other kinds of complex protocols or systems (trading systems, cryptographic and privacy protocols), etc., and you would like to explore ways Quint can bring value to your use cases, please reach out. We are offering free consultations where we demo what we currently have and are happy to explore your use cases. And don't forget that with Quint and LLMs you can be playing instead of reading, and that is definitely more fun 😉