This repo contains a short and incomplete Isabelle proof script for the section 4.3: Forkable Strings in Aggelos Kiayias et al's Ouroboros: A Provably Secure Proof-of-Stake Blockchain Protocol (

  • All definitions up to 4.17

  • Isabelle code is already compatible with Isabelle2017 (the latest public version)

Current status

Proposition 4.18

  • Formalisation of Proposition 4.18 finished

Lemma 4.19:

m(nil) = (0, 0) [DONE] and, for all strings w ∈ {0, 1}*, [There is a typo in the paper in which there is a word "nonempty" describing w but actually w can be empty] m(w1) = (λ(w) + 1, µ(w) + 1), [Done] and m(w0) = (λ(w) − 1, 0) if λ(w) > µ(w) = 0, (0, µ(w) − 1) if λ(w) = 0, (0, µ(w) − 1) if λ(w) = 0, (λ(w) − 1, µ(w) − 1) otherwise. Furthermore, for every string w, there is a closed fork Fw |- w for which m(w) = (λ(Fw), µ(Fw)).

Proof by cases with a precondision as will be used for induction proof as a whole - 3 main cases: nil, w1, and w0 - the first and second cases are formalised - remaining for the third case it requires us formalising the statement that there is a unique forks prefix F' |- w of F |- w0 in a way that F only has a tail to contain the last honest index

Future goals

Theorem 4.13: might follow this proof: instead of the original one from the Ouroboros paper.