
research note
IsabeLLM — Automated Theorem Proving Applied to Formally Verifying Consensus
This paper addresses the challenge of formally verifying blockchain consensus protocols, specifically Bitcoin's Proof-of-Work, using automated theorem proving augmented by large language models (LLMs)










