HI Everyone,
We published a new technical article walking through a real experiment: using Claude and CodeLogician to formally verify a Stripe payment flow. This is a real example of what one of our engineers ran into, working through a Stripe integration and wanting to see how far the tooling could take us. Claude translated the Python into a formal model, wrote verification goals, ran the CLI, and iterated on counterexamples, all in one loop. ImandraX was the auditor.
The results were concrete. Claude wrote a real bug in capture_payment - one it would never have caught through self-review or self-generated tests. It also wrote logically flawed verification goals with full confidence, confusing what it meant informally with what it actually stated formally. And where Claude would have written around 10 test cases, the formal region decomposition found 84, mathematically exhaustive, not just the cases someone thought to check.
The article walks through every step, including the full refinement loop and how the generated tests were used to validate the Python implementation. The code is on Github.
Read the full article here: https://medium.com/imandra/managing-complexity-with-math-and-logic-changing-stripe-payment-flow-with-claude-and-codelogician-cdd386001e40