Verifying Reliable Network Components in a Distributed Separation Logic with Dep...
summary
Claims a verified reliable client–server communication stack implemented in an OCaml-like language (about 300–400 lines of code) that runs over UDP and enforces ordering, retransmit and ACK logic; verification uses Aneris (a distributed separation logic built on Iris), dependent separation protocols and a new session escrow pattern to link duplicable network certificates with logical protocol buffers, enabling send/receive specs and a verified RPC and lazily replicated key‑value store; all proofs and code are formalized in Coq and artifacts are available.
AI-written summary · about
chapters (15)
- 0:00Research introduction
- 1:28Unreliable communication example
- 3:17Program logic design
- 4:38Dependent protocols
- 8:32Distributed network challenges
- 9:36Verifying reliable networks
- 11:51Reliable client-server design
- 13:00Formal translation setup
- 14:44Resource transfer in networks
- 18:01Dependent transfer in ACT
- 20:35Session escrow pattern
- 22:58Verifying send/receive
- 23:44Verified RPC on library
- 24:27Impact on distributed apps
- 25:54Q&A
related talks
15mModular Verification of Op-Based CRDTs in Separation Logic
16mIgloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verifica
18mDistributed Causal Memory for Higher-Order Distributed Separation Logic
28mReasoning about Distributed Reconfigurable Systems
48mThe Verification of a Distributed System
15mStatically Verified Refinements for Multiparty Protocols
26mCryptis: Cryptographic Reasoning in Separation Logic
21mSeparation Logics for Probability, Concurrency, and Security