WebAssembly modules are deployed in environments that are sensitive to the cost of execution: web browsers, edge computing platforms, IOT devices, smart contracts, to name a few. The ability to statically determine the execution cost of a Web Assembly function (and the functions it calls) is an important problem whose solution can lead to improved functionality, reliability, and security of Wasm code in these environments. Contrast this with the current practice of determining the execution cost at run time, after the fact, thus not preventing computing resources from being inappropriately consumed. In this workshop session, we build on our earlier work [6] and that of other researchers to describe our work on a formalization of the execution costs of Web Assembly and an implementation of that formalization in Coq. We also present ongoing work on a tool generated from the Coq implementation. These are based on a fork of the wasm-cert project, a mechanization and proof of soundness of the Wasm specification. Our implementation generates parametric execution cost bounds for the functions in a given WebAssembly module. The execution cost formalization uses instruction count as a cost measure, basic blocks for non-looping code blocks, extended basic blocks when loops are present, and loop cost analysis. These concepts are being applied to arrive at a general set of inequalities that can be solved to produce a cost bound. We solve these inequalities through a combination of mechanisms, including algebraic reduction, loop patterns, and SMT solvers. We are testing this work on a set of publicly available applications and libraries that have been compiled into Wasm. The main conclusion from our work is that the formal specification [5] of Wasm and its mechanization provide a means to successfully reason about complex program properties in the practical settings that our test suite represents.