Hacker News new | past | comments | ask | show | jobs | submit login

This is great stuff. I did something similar in a 2020 paper[1] using Coq. I did not find Coq particularly suited for this type of work. Isabelle/HOL looks promising.

One thing to note is that these types of verifications can become difficult when the systems are layered. Even the simplest real world systems are layered, when you factor in the underlying transport for the messages. The TLC paper provided a way for distributed systems to be composed in a way that reduces the complexity of the proofs for each distributed component.

[1] https://dl.acm.org/doi/10.1145/3409005




What difficulties did you face using Coq?




Consider applying for YC's Summer 2025 batch! Applications are open till May 13

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: