Static analysis of smart-contracts is becoming more widespread on blockchain platforms. Analyzers rely on techniques like symbolic execution or model checking, but few of them can provide strong soundness properties and guarantee the analysis termination at the same time. As smart-contracts often manipulate economic assets, proving numerical properties beyond the absence of runtime errors is also desirable. Smart-contract execution models differ considerably from mainstream programming languages and vary from one blockchain to another, making state-of-the-art analyses hard to adapt. For instance, smart-contract calls may modify a persistent storage impacting subsequent calls. This makes it difficult for tools to infer invariants and high-level security properties required to formally ensure the absence of exploitable vulnerabilities.

The Michelson smart-contract language, used in the Tezos blockchain, is strongly typed, stack-based, and has a strict execution model designed to leave few opportunities for implicit runtime errors. At this moment, few analysis tools support it. We present a work in progress static analyzer for Michelson based on Abstract Interpretation and implemented within MOPSA, a modular static analyzer. Our tool supports the semantic features of Michelson, including inner calls to external contracts. It can prove the absence of runtime errors and infer invariants on the persistent storage over an unbounded number of calls. It is also being extended to prove high-level numerical and security properties.