Formal guarantees for AI workflows: a Cartesian approach to guardrails

Descartes' Discourse on the Method gave the French engineering tradition its spine, in four rules: accept nothing as true that you do not clearly know to be so; divide each difficulty into as many parts as you can; proceed from the simplest matters to the most complex; and enumerate so completely that you are sure you have left nothing out. École Polytechnique built a whole engineering culture on that Cartesian rigor.

It shows up in a place that should make every AI engineer pause: the driverless Paris Métro Line 14, whose safety-critical control software was mathematically proven correct — using the formal B-method — before it ever carried a passenger. Not tested until they felt confident. Proven. The question this raises for us is not "can we prove an AI right?" It is: which parts of an AI workflow deserve proof, and which only deserve evaluation?

The probabilistic core and the deterministic shell

An AI workflow is not one kind of thing. It has a probabilistic core — the model, which is inherently uncertain and cannot be proven correct in any useful sense — wrapped in a deterministic shell: the code that masks PII, checks policy, enforces spend limits, routes to approval, and calls connectors.

You cannot prove the model will write a good quote. But you can prove that no field tagged as PII ever leaves the system unmasked, that no spend exceeds its budget, that no unauthorized action reaches a connector. The Cartesian move is to stop treating the workflow as one undifferentiated blob of "AI" and separate the part that must be good from the part that must be correct.

Rule one: specify before you build

Descartes' first rule — accept nothing you cannot clearly state — is, in software, the demand for a specification. A property you cannot state precisely, you cannot verify at all. "The system protects privacy" is not a specification. "No output field derived from a column tagged PII appears in any outbound payload without passing through the masking function" is.

Writing that sentence is most of the work. It forces you to define what PII means in your data model, what "outbound" includes, and what masking guarantees. Most privacy incidents are not verification failures; they are specification failures — nobody ever said exactly what was supposed to be true.

Rule two: divide the difficulty

The second rule is decomposition. Split every workflow requirement into two piles:

• Must be correct — masking, authorization, spend caps, the audit record. These are deterministic, safety-critical, and small. Here, aim for proof.
• Must be good — the draft, the tone, the summary, the recommendation. These are probabilistic and open-ended. Here, aim for evaluation.

The mistake is applying one standard to both: demanding proofs of the model (impossible) or accepting "it seemed fine in testing" for the masking layer (negligent). Different piles, different discipline.

Rule three: climb from tests to proofs

Dijkstra's warning is the hinge of the whole field: testing can show the presence of bugs, but never their absence. For the "must be good" pile, tests and evals are the right and only tool. For the "must be correct" pile, you can climb a ladder of increasing assurance:

• Types that make illegal states unrepresentable — an unmasked value simply cannot be passed to a send function.
• Invariants and assertions checked at every boundary.
• Property-based testing that generates thousands of adversarial inputs against a stated property.
• Formal verification where the stakes justify it, proving the property holds for all inputs, not a sample.

This is not exotic. Xavier Leroy's CompCert is a C compiler proven correct with the Coq proof assistant; Jean-Raymond Abrial's B-method verified the Line 14 control system. The tooling exists, and the point is not to verify everything — it is to spend proof where the cost of being wrong is unbounded.

Rule four: enumerate completely

Descartes' final rule — leave nothing out — is, for AI workflows, the audit trail as a proof obligation. Every consequential step must be accounted for: which guardrails ran, which passed, what was masked, who approved. An enumeration with gaps is not an enumeration. If a run can take an action that appears nowhere in the record, your shell is not complete, and completeness is a property you can specify and check like any other.

Where PromptRails draws the line

We are explicit about which pile each thing lands in. The model's outputs are evaluated — scored, sampled, reviewed — because that is the honest tool for a probabilistic core. The shell around it is built to be correct: PII masking runs deterministically before any data reaches a model, policy and spend checks are enforced rather than suggested, and every run enumerates what it did into an audit trail.

The Cartesian lesson is not that AI can be proven safe — it cannot, and pretending otherwise is its own failure. It is that a probabilistic system can have a provable shell, and that drawing the line clearly between the two is what separates engineering from hope. The Métro runs driverless under Paris because someone insisted on proving the part that had to be right. Your guardrails deserve the same insistence.

References

1. René Descartes, Discourse on the Method, 1637 (Cambridge University Press edition, 1985).
2. Jean-Raymond Abrial, The B-Book: Assigning Programs to Meanings, Cambridge University Press, 1996.
3. Xavier Leroy, Formal Verification of a Realistic Compiler, Communications of the ACM, 52(7), 2009.
4. Edsger W. Dijkstra, The Humble Programmer, Communications of the ACM, 15(10), 1972.

---

Want to see where the provable shell ends and evaluation begins in your workflow? Book a 30-minute technical review.