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…