We are working toward applying formal methods from the application security testing side, but I believe the same kind of approach can be applied to business logic verification as well. For that, we are using the taint analysis technique — a fairly well-established formal methods approach, but still not widely applied in the field because of the complexity of dataflows in real codebases.

Scaling formal methods beyond AST pattern matching and some simple type checking turns out to be a really hard task! It took years of research and development to reach the point where taint analysis enables us to trace interprocedural dataflows in real codebases in minutes and find deeply hidden vulnerabilities.

If this sounds interesting to you, take a look at our project: https://github.com/seqra/opentaint