Abstract
Smart contracts written using the Solidity programming language of the Ethereum platform are well-known to be subject to bugs and vulnerabilities, which already have led to the loss of millions of dollars worth of assets. Since smart contract code cannot be updated to patch security flaws, reasoning about smart contract correctness to ensure the absence of vulnerabilities before their deployment is of the utmost importance. In this paper, we present a formal approach for generating correct smart contracts from B specification that verify safety properties. Our approach consists of two phases: first a smart contract and its properties are specified and verified in B, then a set of rules we defined are applied to generate the correct smart contract code in Solidity. The approach is implemented in a tool that can generate Solidity contract from a proven B project. The whole approach is demonstrated by a case study on the ERC-20 (Ethereum Request for Comments 20) Wrapped Ether (WETH) contract, which is abstractly specified in B, with invariants stating correctness properties, modeled checked with ProB for temporal properties, implemented in B0, proven correct, and automatically translated into a Solidity contract.
This work was supported by the ANR projet DISCONT, Public Safety Canada and NSERC.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abrial, J.: The B-Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
B2sol translation tool. https://github.com/ICECCS2024/B2SolPrototype
Banach, R.: Verification-led smart contracts. In: Bracciali, A., Clark, J., Pintore, F., Rønne, P.B., Sala, M. (eds.) FC 2019. LNCS, vol. 11599, pp. 106–121. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-43725-1_9
Bhargavan, K., et al.: Formal verification of smart contracts: short paper (2016). https://doi.org/10.1145/2993600.2993611
Buterin, V.: Critical update re: Dao vulnerability. https://blog.ethereum.org/2016/06/17/critical-update-re-dao-vulnerability/
Buterin, V.: Ethereum: a next-generation smart contract and decentralized application platform (2014). https://github.com/ethereum/wiki/wiki/White-Paper
Butler, M., et al.: The first twenty-five years of industrial use of the B-method. In: ter Beek, M.H., Ničković, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 189–209. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58298-2_8
Chen, T., et al.: Under-optimized smart contracts devour your money. In: IEEE 24th International Conference on Software Analysis, Evolution and Reengineering, SANER 2017 (2017). https://doi.org/10.1109/SANER.2017.7884650
Ethereum: Solidity documentation. release 0.7.0. https://docs.soliditylang.org/en/v0.7.0/
Garfatta, I., et al.: Model checking of vulnerabilities in smart contracts: a solidity-to-CPN approach. https://doi.org/10.1145/3477314.3507309
Grieco, G., et al.: Echidna: effective, usable, and fast fuzzing for smart contracts. https://doi.org/10.1145/3395363.3404366
Luu, L., et al.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (2016). https://doi.org/10.1145/2976749.2978309
Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https://bitcoin.org/bitcoin.pdf
Nehai, Z., et al.: Model-checking of smart contracts. In: IEEE International Conference on Internet of Things 2018 (2018). https://doi.org/10.1109/Cybermatics_2018.2018.00185
Nguyen, T.D., et al.: sFuzz: an efficient adaptive fuzzer for solidity smart contracts. https://doi.org/10.1145/3377811.3380334
Nikolic, I., et al.: Finding the greedy, prodigal, and suicidal contracts at scale. In: 34th Annual Computer Security Applications Conference, ACSAC. https://doi.org/10.1145/3274694.3274743
Singh, N.K., et al.: Formal verification and code generation for solidity smart contracts. In: Distributed Computing to Blockchain. https://doi.org/10.1109/COMPSAC51774.2021.00183
Suvorov, D., Ulyantsev, V.: Smart contract design meets state machine synthesis: case studies
Tikhomirov, S., et al.: Smartcheck: static analysis of ethereum smart contracts. https://doi.org/10.1145/3194113.3194115
Tolmach, P., et al.: A survey of smart contract formal specification and verification (2022). https://doi.org/10.1145/3464421
Torres, C.F., et al.: Confuzzius: a data dependency-aware hybrid fuzzer for smart contract. https://doi.org/10.1109/EUROSP51992.2021.00018
Zhu, J., et al.: Formal simulation and verification of solidity contracts in Event-B. In: IEEE 45th Annual COMPSAC 2021 (2021). https://doi.org/10.1109/COMPSAC51774.2021.00183
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Baba, F., Mammar, A., Frappier, M., Laleau, R. (2025). Modeling and Verification of Solidity Smart Contracts with the B Method. In: Bai, G., Ishikawa, F., Ait-Ameur, Y., Papadopoulos, G.A. (eds) Engineering of Complex Computer Systems. ICECCS 2024. Lecture Notes in Computer Science, vol 14784 . Springer, Cham. https://doi.org/10.1007/978-3-031-66456-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-031-66456-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-66455-7
Online ISBN: 978-3-031-66456-4
eBook Packages: Computer ScienceComputer Science (R0)