Path to Insurability#

The underwriter’s question#

Carriers underwriting autonomous-action risk ask one question first: what is the residual risk, and can it be priced? For traditional automation the answer is forty years old. The IEC 61508 family — together with ISO 13849-1 for machine control, DO-178C for airborne software, ISO 26262 for road vehicles — gives carriers a documented body of evidence, audited by a third party, expressed in actuarial-readable quantities: diagnostic coverage, fault-detection time, common-cause-failure scoring, mean time to dangerous failure.

Autonomous AI agents do not yet have that body of evidence. The harmonized standards under the EU AI Act are still being drafted. ISO/IEC TR 5469 is published as a technical report, not yet a Notified-Body assessable standard. Existing AI-risk frameworks (ISO/IEC 23894, ISO/IEC 42001) are management-system standards, not safety-integrity standards.

ANNIE is built to narrow that gap by treating it as an engineering problem, not a marketing one. The goal is not to claim approval before assessment; the goal is to make eventual assessment easier by framing autonomous-agent risk in the same language carriers and safety engineers already use for dangerous equipment.

What “insurable” actually means#

There are two postures a vendor can take into an underwriting conversation. The first is “our AI is safe — trust us.” That posture is uninsurable, and rightly so: the carrier has no evidence to price against, no replay capacity if a claim arises, and no scope for independent verification. Vendor confidence is not a peril class.

The second posture is “here is the evidence stack you can audit, replay, and price against, and here is the boundary of what we claim.” That posture is what industrial control systems present to carriers today. It is the posture ANNIE is engineered to support, with the understanding that certification and policy approval still require independent review.

The shift is structural. Instead of asserting that the model behaves safely, the system constrains what the model is permitted to commit to using a deterministic, formally specified gate. The gate is the safety function. Every proposal the gate accepts is anchored in a cryptographic ledger that any third party can replay using a tool shipped with every license. Every proposal it rejects is also anchored. Every hardware-fault event is logged with a documented response-time budget. None of these mechanisms depend on the language model being trustworthy — they treat it as the untrusted, high-capability channel that needs to be constrained.

That structure is what an underwriter can price. The four-pillar architecture exists for that reason: independent verification, bounded-latency control, hardware-fault containment, and a tamper-evident event log are the four properties a carrier needs to write coverage against autonomous-action risk.

The evidence stack#

Five artifacts are produced by the platform that an underwriter can be handed during a quote process. Each pairs an artifact with what it gives the carrier.

Formal-method proof artifacts. The deterministic safety kernel — ~900 lines of SPARK/Ada across four packages (Oracle_Message, Ring_Buffer, FFI, Crypto) — is verified by GNATprove at Level 2 with 22,534 verification conditions discharged, zero unproved, as of the 2026-05-22 proof run. The breakdown by discharge method: 15,290 prover-discharged by CVC5 (68%), 7,163 flow-analyzed by GNATprove’s flow analyzer (32%), and 81 justified suppressions (documented false-positives in the included keccak SHA3 reference implementation — semantically correct loop-initialization patterns the flow analyzer cannot follow). What this gives the carrier: a class of fault modes — buffer overflow, state-machine invariant violation, message-format corruption, modular-arithmetic edge case — addressed by construction rather than by testing alone, with a verifier the carrier can run independently against the published proof artifacts.
Hash-chained event ledger plus the annie verify tool. Every approved action, every rejected action, every hardware-fault halt, and every ceremony signature is recorded in an append-only Merkle-chained log. The annie verify tool ships with every commercial license and walks the chain end to end, reporting tampering at row-level granularity. What this gives the carrier: post-incident replay capacity that does not require vendor cooperation. The customer’s auditor, the carrier’s loss-adjustment investigator, or a regulator can independently confirm what the agent was authorized to do and when.
Documented diagnostic-coverage argument with bounded fault-detection time. On supported AMD ROCm hardware, the kernel-level fault-response path is measured against a documented microsecond budget once the silicon raises a compute exception. The budget is platform-specific and published per release. What this gives the carrier: a number that maps directly onto ISO 13849-1’s fault-detection-time requirement for the dual-channel patterns the architecture is designed against.
Published per-release worst-case-latency measurements. Each release ships with measured worst-case latency for the hardware-fault response and for the deterministic-cadence control loop on supported platforms. A regression in either number is treated as a release blocker. What this gives the carrier: trend data, in a form that supports actuarial fitting, with vendor accountability for non-regression.
Post-quantum signed receipts. Every ledger entry that carries an authorization is signed using NIST-standardized ML-DSA post-quantum signatures. What this gives the carrier: evidence durability under future cryptographic-attack scenarios, including the case where today’s signatures become forgeable.

Failure mode framing#

Underwriters need both halves of the picture: what the system addresses, and what it does not. ANNIE’s scope is precise; the carrier’s policy language has to reflect that precision.

In scope for the safety kernel. Hardware-fault propagation from the accelerator into the agent’s action surface. Violation of the formally specified ethics rules by an action the agent has proposed. Tampering with the event ledger after the fact. License bypass or replay. Excursion of the control loop past its documented latency budget — the deployment refuses to start rather than run degraded.

Out of scope for the safety kernel. The shape of the language model’s hallucinations — the architecture treats the model as untrusted by construction and constrains what it can commit to, but does not improve its outputs. Application-layer compensation logic for actions that were correctly authorized but turned out wrong at the business level. Side-channel attacks against the host operating system. Physical access to the deployment hardware. Errors introduced by the integrating application above the kernel’s authorization boundary.

The honest split matters because policy wording follows it. The carrier writes coverage against the failure modes the kernel addresses; the customer carries — or insures separately — the failure modes outside that boundary. Both lists are documented and reviewed before a policy is bound.

A failure-mode and effects analysis structured against the in-scope list is part of the safety case summary distributed under NDA to qualified carriers. The public page describes the existence and shape of that document; it does not reproduce the analysis itself, because doing so would publish information that prospective adversaries could use.

Diagnostic coverage — claim and scope#

ANNIE is designed against the dual-channel-with-continuous-diagnostic pattern that ISO 13849-1 names Category 4. Strict Category 4 conformance requires diagnostic coverage at or above 99 percent and fault-detection time below the process safety time, validated by a Notified Body against a documented safety case the team has not yet commissioned. This is the most-scrutinized paragraph for an underwriter, so it has to be unambiguous.

What the platform claims today:

The architectural pattern is Category 3 / 4 dual-channel.
A continuous diagnostic — the deterministic-cadence control loop — runs at a documented rate published per release.
A hardware-fault response path is measured against a documented microsecond budget on supported platforms; the budget is measured and the measurement is published.
The SPARK kernel that implements the dual-channel safety logic is formally verified at GNATprove Level 2 with zero unproved verification conditions (see §3 above).

What the platform does not claim today: a third-party-assessed diagnostic-coverage percentage, a third-party-assessed mean-time-to-dangerous-failure number, or any Performance Level / Safety Integrity Level. Those quantities require an audited safety case which is a separately scoped workstream.

Claiming only what is measured is the policy; the alternative is a number a carrier cannot defend.

Alignment and certification — what is and is not claimed#

The functional-safety framing page on this site already states the alignment-versus-certification distinction in technical detail. The same distinction matters for an underwriter, in different vocabulary.

The platform is designed against the IEC 61508 family of standards. Architectural patterns that those standards specify — independent monitor on a separate channel from the high-capability component, continuous diagnostic running faster than the actuation surface, safe-state-on-fault response, tamper-evident event history — are implemented in the source. The patterns are observable in the design.

The platform is not certified to those standards. There is no Notified-Body assessment, no CE / UKCA marking, no SIL / ASIL / PL claim, and no published MTTFd / DC / CCF numbers. Carrier-required certification, where the carrier’s policy language demands it, is not yet present. The path to that certification is the engineering workstream this page describes the start of: building the system and its evidence in a way that should reduce future review friction, not bypass review.

How carriers and MGAs engage#

Carriers, MGAs, and brokers can request the NDA-gated safety case summary by mailing preorder@verifiableproof.systems with the subject line “Insurance” or “Carrier”. Same triage discipline as the executive summary’s other engagement hooks: response within two business days, NDA exchanged before the document is sent.