From Paper to Proof: How We Can Formally Verify Blockchain Protocols with Lean4