Category: formal-verification
Posts in this Category (3)
Convergence vs Consensus in Distributed Systems
Published on: October 20, 2025
Convergence and consensus are two closely-related properties of distributed systems implementing the replicated state machine (RSM) abstraction. While convergence requires replicas to eventually agree on the value of a decision variable, consensus requires them to never disagree. This subtle distinction makes all the difference in practice: while convergence can be...Extraction in Coq
Published on: May 31, 2016
Extraction erases Props Extraction in Coq works by erasing Props. For example, consider the following definition of div: Definition div (m n : nat)(H : n<>0): nat := NPeano.div m n. div expects a proof that its second argument is non-zero. Indeed, in coq, it is impossible for div to...Coq Basics
Published on: April 09, 2014
GADTs vs Inductive Datatypes Consider the following definition of Nat-indexed Vector GADT in OCaml and Haskell: OCaml: (* vec : * -> * -> * *) type (_,_) vec = | Nil : ('a,zero) vec | Cons : 'a * ('a,'b) vec -> ('a,'b succ) vec Haskell: data Vec ::...