I found the Developer Voices discussion[1][2] with Joran Dirk Greef, creator of TigerBeetle, to be fascinating. They mentioned that the rigorous correctness proofs that exist for Raft and Paxos assume an absence of disk faults, but that more modern theory includes fixes for that, as long as you marry the log writing and consensus algorithms together properly rather than keeping each as a separate black box.
I second this recommendation. I'm impressed by what TigerBeetle has accomplished, and would love to see more of the industry approach software engineering with their philosophy and rigour.
The TigerStyle video is well worth watching for anyone who wants to build defect-free software systems, or recognizes that this is the correct thing to aim for. https://www.youtube.com/watch?v=w3WYdYyjek4
[1] https://podcasts.apple.com/us/podcast/databases-ambitions-an...
[2] https://www.youtube.com/watch?v=ayG7ltGRRHs