We describe ongoing work developing a semantic infrastructure for designing automated and interactive amortised cost analyses based on synthesising potential functions for randomised data structures. These analyses can synthesise amortised complexity bounds that are tight and correct by construction. The architecture combines established and recent ideas from program logics for data structure specification, weakest pre-condition quantitative reasoning, semantics of probabilistic programming, and amortised resource analysis synthesis.