I arrive a bit late to this question but here's my answer, I hope it is useful: There is a very prolific synthetic approach to Lorentzian geometry (and GR) first introduced by Kunzinger and Sämann [1] where they define the notion of "Lorentzian (pre-)length space", which is a causal set with a chronological relation and a lower semicontinuous time separation function satisfying some extra properties. There are a lot of results that can be translated from the smooth setting to this synthetic setting such as the causal ladder of spacetimes. This also has the advantage that is the "analogous" case to metric geometry of length spaces so people also study classic metric results (as in Alexandrov geometry) in the Lorentz case as a notion of **timelike curvature bounds** is available in Lorentzian length spaces. There's also a notion of **ricci curvature bounds** to obtain synthetic energy conditions via optimal transport. A very interesting paper was published by Cavalletti and Mondino [2] where they prove Hawking type singularity theorems in this setting. I understand that there is a program by a lot of people (Kunzinger, Sämann, Gigli, McCann, Beran, Rott, Ohanyan, Calisti, and maybe I'm forgetting someone) to develop non-smooth hyperbolic calculus in this Lorentzian length spaces in a similar manner to what optimal transport has allowed people to do in RCD spaces.