Proving completeness of an eventually perfect failure detector in Lean4 https://lobste.rs/s/adl5af #distributed #formalmethods
https://protocols-made-fun.com/lean/2025/06/10/lean-epfd-completeness.html
If you have a fediverse account, you can quote this note from your own instance. Search https://mastodon.social/users/lobsters/statuses/114665993844766613 on your instance and quote it. (Note that quoting is not supported in Mastodon.)