Stuff like these. It overlaps with model-driven development where you work at a higher level in constrained way to knock out many issues. Then, it generates safe code from that which you also check with tests or other tools.

https://en.wikipedia.org/wiki/Stateflow

https://en.wikipedia.org/wiki/Simulink

Recent example from high-assurance security:

https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/hard...