On lightweight formal methods, a favorite of mine that's not widely known is trace verification using Linear Temporal Logic [0].
Basically you just need to log events - which you can even have for free in event-driven architectures etc - and run some predicates on execution traces, e.g. "Always(Locked, Implies(Eventually(Unlocked)))", etc.
One can run it on historical traces, but also couple it to stress tests, fuzzing etc to explore the state space.
Quite simple, powerful and widely applicable, and doesn't require a model, just predicates.