End-to-end formal verification
TLS
for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif
user authentication protocol defined by the Information Card Profile V1.0
derive formal proofs using ProVerif
Protocol implementation in F#(Bhargavan et al. , 2006) to CryptoVerif Scripts
Distributed Protocol Combinators
Kristoffer Just, Arndal Andersen and Ilya Sergey
"Declarative programming over distributed protocols"
Distributed Protocol Combinators (DPC)—a set of versatile higher-order programming primitives implemented in Haskell
RPC-based cloud calculator and its variations, to distributed locking, Two-Phase Commit , and Paxos consensus
In contrast Disel and other static verification frameworks that enforce protocol adherence via (dependent) type systems (embedded in Coq or other proof assistants) 11,24, we verify protocol properties dynamically. Yoichi Hirai