Smart contracts are programs building on blockchain technology.
They implement functionality that has been agreed on between
the concerned parties on a network. However, their immutability
and exposed position make them vulnerable to programming errors,
leading to faulty behavior and possible exploits. Therefore,
smart contracts demand a particularly thorough analysis,
ideally using formal program verification. In this paper, we
present an approach for the deductive verification of
Hyperledger Fabric smart contracts using the KeY prover.
We have extended KeY to handle Fabric ledger implementations;
in particular, we have developed mechanisms for reasoning about
serialization and object persistence. The feasibility of our
approach is demonstrated with a small case study.