Towards Verifiable-by-Design Smart Contracts: A Declarative Limit Order Books Implementation
This paper introduces an on-chain limit order book built with a declarative smart contract language. By expressing conservation, ordering, and state-transition constraints directly, the design aims to make core properties easier to verify before deployment.