Demonstration of formally verified chaincode generation for Hyperledger Fabric

We will show some preliminary results of our ongoing work to enable formal specification and verification of HLF chaincode. The proposed methodology consists in using the tool Why3 [1] (and its underneath language WhyML, and third-party SMT solvers) to specify, implement and prove the chaincodes. The tool Why3 then extracts an OCaml chaincode. Finally, we developped OCaml-chaincode-shim [2] to make OCaml chaincodes executable by an HLF peer. We will demonstrate the application of this methodology on a no code development scenario of a workflow supervisor (that could be a critical component of an industrial supply chain traceability system). This scenario starts with an abstract specification of the workflow in a graphical formalism (in the vein of [3]) and ends with a formally verified chaincode living in a HLF testnet.

[1] : Filliâtre, J. C., & Paskevich, A. (2013, March). Why3—where programs meet provers. In European symposium on programming (pp. 125-128). Springer, Berlin, Heidelberg.
[2] : https://github.com/hyperledger-labs/fabric-chaincode-ocaml
[3] : Bistarelli, S., Faloci, F., & Mori, P. (2021, November). *. chain: automatic coding of smart contracts and user interfaces for supply chains. In 2021 Third International Conference on Blockchain Computing and Applications (BCCA) (pp. 164-171). IEEE.