3 papers
cs.LO2022
An approach to translating Haskell programs to Agda and reasoning about them
Harold Carr, Christa Jenkins, Mark Moir +2
We are using the Agda programming language and proof assistant to formally verify the correctness of a Byzantine Fault Tolerant consensus implementation based on HotStuff / LibraBF…
cs.DC2022
Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version
Harold Carr, Christopher Jenkins, Mark Moir +2
LibraBFT is a Byzantine Fault Tolerant (BFT) consensus protocol based on HotStuff. We present an abstract model of the protocol underlying HotStuff / LibraBFT, and formal, machine-…
cs.CR2021
Formal Verification of Authenticated, Append-Only Skip Lists in Agda: Extended Version
Victor Cacciari Miraldo, Harold Carr, Mark Moir +2
Authenticated Append-Only Skiplists (AAOSLs) enable maintenance and querying of an authenticated log (such as a blockchain) without requiring any single party to store or verify th…