"Lightweight formal methods" meaning you build a model of some program logic and test it's properties hold. https://forge-fm.github.io/book/

Beyond that is dependent types