https://www.microsoft.com/en-us/research/project/network-ver...
Have you investigated Security Hub by chance?
This, of course, assumes that the math is sound.
There's an analogy to unit tests. You can write a unit test for a function, and the test can pass, but if you've made a mistake in the test itself, it might give you a false sense of assurance.
I have no doubt that Amazon is very rigorous with this, although if they're explicitly touting these tools in terms of allowing clients to meet regulatory compliance obligations, it would be cool to have some sort of third-party audit of the math.
Note that tests will often catch cases where the math is not sound. Because you are putting an expected result it is more likely that you have a sound reason for that expected result even if you cannot express is mathematically. I recommend you use both: in the real world they cover different areas of the problem.