This paper describes the design and an implementation exploration for *symbolic contracts*: contract assertions whose predicate has, by default, no run-time representation at all, and whose truth is instead established and consumed purely by the compiler's own static reasoning about the program. We explain what a symbolic function is, the escape hatch for predicates that are known to be unprovable in context, how the static analysis of symbolic contracts relates to the concerns raised in [P3362](https://wg21.link/p3362), and, perhaps counterintuitively given the "no run-time representation" framing, how symbolic contracts also support an entirely optional, opt-in run-time checking mode that works *across* translation units.