  As smart contracts are growing in size and complexity, it becomes harder and
harder to ensure their correctness and security. Due to the lack of isolation
mechanisms a single mistake or vulnerability in the code can bring the whole
system down, and due to this smart contract upgrades can be especially
dangerous. Traditional ways to ensure the security of a smart contract,
including DSLs, auditing and static analysis, are used before the code is
deployed to the blockchain, and thus offer no protection after the deployment.
After each upgrade the whole code need to be verified again, which is a
difficult and time-consuming process that is prone to errors. To address these
issues a security protocol and framework for smart contracts called Cap9 was
developed. It provides developers the ability to perform upgrades in a secure
and robust manner, and improves isolation and transparency through the use of a
low level capability-based security model. We have used Isabelle/HOL to develop
a formal specification of the Cap9 framework and prove its consistency. The
paper presents a refinement-based approach that we used to create the
specification, as well as discussion of some encountered difficulties during
this process.
