Formal Methods
Adaptive Formal Verification for Automated Remediation
A structured-contract approach that verifies every proposed remediation action against live system state, policy, and in-flight conflicts.
Mohan Murari, Raghav Balasubramaniam — Raincurve Research
Abstract
AI reasoning over infrastructure telemetry is inherently probabilistic. That is acceptable for an alert reviewed by a human, but not for an action executed against production. Raincurve represents each proposed remediation as a structured contract with explicit, machine-checkable constraints and requires adaptive formal verification against current system state and policy before execution.
Actions as contracts
Each action specifies what it does, the preconditions it assumes, and the constraints it must not violate. This makes the action itself auditable and machine-checkable, rather than relying on a natural-language explanation or opaque API call.
Verification procedure
Before execution, each contract is checked against current system state, operator-defined policy constraints, and in-flight conflicts with overlapping actions. Any failed check blocks execution and surfaces the exact violated constraint for operator review.
Conclusion
Adaptive verification separates diagnostic confidence from execution safety: a model may propose a useful action, but only an independently explainable verification pass allows it to reach production.