Towards Verifiable-by-Design Smart Contracts: A Declarative Limit Order Books Implementation

Abstract

We present a declarative approach to on-chain limit order books (LOBs) that prioritizes formal verification over raw throughput. Unlike automated market makers, LOBs offer granular control and capital efficiency but are difficult to verify when implemented imperatively in Solidity. Using Pint, a declarative domain-specific language, we encode LOB matching logic, price-time priority, partial fills, and asset conservation, as first-order constraints. Off-chain solvers compute valid state transitions, while the blockchain performs lightweight constraint verification. We implement eight LOB predicates and evaluate performance using real-world transaction traces. Our declarative LOBs achieve 141 predicates/s for simple operations and 11 predicates/s for complex settlement with 1,000 accounts. Performance correlates strongly with state access patterns rather than constraint complexity. Critically, our approach eliminates verification challenges that make imperative smart contracts hard to formally verify, such as unbounded loops, recursion, cross-contract/function calls, and complex control flow. This enables correctness-by-construction through constraint satisfaction, removing the need to prove implementation conformance to specifications. This work demonstrates the first practical evidence that declarative LOBs achieve reasonable performance while providing superior verification guarantees for DeFi protocols.