US 11,816,018 B2
Systems and methods of formal verification
Zhong Shao, Branford, CT (US); Ronghui Gu, New Haven, CT (US); Vilhelm Sjoberg, New Haven, CT (US); Jieung Kim, New Haven, CT (US); and Jeremie Koenig, New Haven, CT (US)
Assigned to Yale University, New Haven, CT (US)
Filed by Yale University, New Haven, CT (US)
Filed on Jul. 12, 2022, as Appl. No. 17/862,480.
Application 17/862,480 is a division of application No. 16/767,569, granted, now 11,409,630, previously published as PCT/US2018/062883, filed on Nov. 28, 2018.
Claims priority of application No. 17/61318 (FR), filed on Nov. 28, 2017.
Prior Publication US 2022/0365862 A1, Nov. 17, 2022
Int. Cl. G06F 9/44 (2018.01); G06F 11/36 (2006.01)
CPC G06F 11/3608 (2013.01) 20 Claims
OG exemplary drawing
 
1. A method for verifying smart contracts, comprising:
modeling one or more smart contracts on a blockchain as a concurrent abstraction layer, wherein:
each of the one or more smart contracts on the blockchain contains computer executable code configured to execute one or more transactions to generate associated state information,
the blockchain is configured to be maintained by one or more nodes on a distributed network, and
the concurrent abstraction layer includes a layer implementation, an underlay interface, and an overlay interface; and the layer implementation includes the one or more smart contracts on the blockchain; and
verifying correctness of the one or more smart contracts, at least in part by constructing a formal proof that the layer implementation, running on top of the underlay interface, simulates the overlay interface, wherein constructing the formal proof comprises:
modeling transactions performed by the one or more smart contracts on the blockchain using a first logical global log; and
verifying that the first logical global loci is consistent with a second logical global log representing acceptable behavior of the smart contracts.