BoltProof bronze

boltproof.dev

“Formally verifies billing, pricing, and subscription logic as Z3 constraints. Returns a proof or a concrete counterexample. Deterministic, not AI.

https://boltproof.dev/.well-known/agent-card.json its card

Checked 11h ago extendedAgentCard, pushNotifications, streaming

we checked this the operator says this

Community rating 0 0 up · 0 down — sign in to vote

Verified by agenttru.st

Everything here is a check agenttru.st performed itself. Assurance, protocol, hosting and freshness are in the card above and are not repeated.

Certificate: Issued by Google Trust Services domain-validated
Valid until 21 Jan 2027 as of our check on 15 Nov 2026. A wildcard certificate: its other hosts are invisible here, because CT logs the wildcard, not them.

Control of the hostname was checked; nothing about who operates it.

Key ECDSA P-256, signed ECDSA-SHA256, issued via WE1 under GTS Root R4 — classical, as every publicly trusted certificate is today.

Names on this certificate (2)

boltproof.dev, *.boltproof.dev.
Connection: TLS 1.3 · X25519MLKEM768 — post-quantum hybrid key exchange, agreed with our checker on 15 Nov 2026. What this means
DANE / TLSA: Not verified (TLSA query returned RCodeNameError)
Discovery: Well-known document
AI-facing documents: Publishes /llms.txt — “BoltProof” a curated map of the site's content for language models

Fetched from this host during verification. Neither document is how this agent was discovered.
First seen: 23 Oct 2026

View verification details

Assurance: bronze Bronze — agent card fetched over HTTPS with a valid certificate
Protocols: A2A verified by handshake or card fetch, not merely advertised
Hosted in: ? Unknown · Cloudflare, Inc. (AS13335)
The address did not geolocate — usually anycast hosting, where one address answers from many places at once.
Last checked: 11h ago

What this agent says it can do

Declared in the agent's own card. agenttru.st has not tested whether it completes any of these tasks — the operator of boltproof.dev controls every word below.

Scan billing logic

Run every approved BoltProof rule against one bundle of billing parameters and return every violation.

billingverificationz3formalscan

Examples it gives

{"bundle": {"charge_amount": 100, "refund_request": 150}}

An invoice's date must always lie within the billing period it covers (period_st…

An invoice's date must always lie within the billing period it covers (period_start <= invoice_date <= period_end). A missing or unset timestamp must never serialize as epoch zero (1970-01-01); it must resolve to a real date inside the period. Source: HN 39558132 -- Cloudflare sent an invoice whose PDF was titled cloudflare-invoice-1970-01-01.pdf; an unset timestamp (a Feb 29 leap-day edge in the billing date logic) rendered as 0 instead of a date inside the period. Billing periods start at epoch day >= 1 (epoch day 0 is not a real period start); the invoice_date != 0 guard is entailed by the range clause but kept explicitly to pin the incident.

billingverificationbillingcloudflare_epoch_zero_invoice

Examples it gives

{"rule": "cloudflare_epoch_zero_invoice", "inputs": {"period_start": 0, "period_end": 0, "invoice_date": 0}}

When a credit is created on a Kill Bill account with an explicit requestedDate,…

When a credit is created on a Kill Bill account with an explicit requestedDate, the system generates two paired invoice items — a CREDIT_ADJ (the credit) and a CBA_ADJ (the account-balance adjustment). Both items must carry start_date = end_date = requestedDate. A bug that dates the CBA_ADJ item "today" instead of the requested date breaks the pairing. Source: killbill/killbill#2202 — requestedDate=2026-04-01 yields CREDIT_ADJ dated 2026-04-01 but CBA_ADJ dated 2026-04-17 (today). This is a GUARD rule: the computation models the correct system's pairing work (the CBA_ADJ inherits the CREDIT_ADJ's date); the invariant enforces that both items sit on the requested date. Global SAT is expected.

billingverificationbillingkillbill_cba_adj_date

Examples it gives

{"rule": "killbill_cba_adj_date", "inputs": {"requested_date": 0, "credit_adj_date": 0}}

A subscription's true start (its trial start) and the start of its current billi…

A subscription's true start (its trial start) and the start of its current billing period are distinct concepts and must never be conflated. The backend stores the true start on the subscription record; every UI/API surface must report that true start (the trial start), never the billing-period anchor. Source: getlago/lago#772.

billingverificationbillinglago_subscription_start_date

Examples it gives

{"rule": "lago_subscription_start_date", "inputs": {"trial_start": 0, "billing_start": 0, "subscription_start": 0}}

When a subscription update uses prorationBillingMode = prorated_next_billing_per…

When a subscription update uses prorationBillingMode = prorated_next_billing_period

billingverificationprorationpaddle_deferred_proration_min_ch…

Examples it gives

{"rule": "paddle_deferred_proration_min_charge", "inputs": {"prorated_amount": 0, "minimum_charge": 0, "deferred": 0, "accepted": 0}}

The previewUpdate endpoint must return the same prorated credit and next payment…

The previewUpdate endpoint must return the same prorated credit and next payment as the committed subscription change. When credits exist on a subscription, both paths must derive the prorated credit from credit_balance and the next payment from base_amount - credit_balance. A preview that shows different numbers than the real change misleads callers. Source: paddle-node-sdk#106 — previewUpdate returns wrong values when credits exist; the "Next payment" preview differs from the committed change.

billingverificationprorationpaddle_preview_commit_consistenc…

Examples it gives

{"rule": "paddle_preview_commit_consistency", "inputs": {"base_amount": 0, "credit_balance": 0}}

A mid-cycle plan change must never produce a prorated charge that exceeds the fu…

A mid-cycle plan change must never produce a prorated charge that exceeds the full-period price of the new plan, and proration must credit the amount the customer actually paid (not assume a zero payment when a full discount applied). Proration for increasing quantity is the added units priced at the new unit price, never more.

billingverificationbillingproration_cap

Examples it gives

{"rule": "proration_cap", "inputs": {"new_quantity": 0, "old_quantity": 0, "unit_price": 0}}

A mid-cycle quantity increase must charge exactly the added units at the full un…

A mid-cycle quantity increase must charge exactly the added units at the full unit price. The prorated charge is (new_quantity - old_quantity) * unit_price, and the basis actually applied must be the full price — never the discounted basis the customer actually paid for the old units. Guard rule: the computation models the system's derivation from whatever basis it applied; the invariant enforces that basis is the full unit price. Source: stripe/stripe-dotnet#3103 (over-charge 144 from discounting the old credit; symmetric under-charge from pricing added units at the discounted basis).

billingverificationbillingproration_on_actual_paid

Examples it gives

{"rule": "proration_on_actual_paid", "inputs": {"old_quantity": 0, "new_quantity": 0, "unit_price": 0, "actual_paid_per_unit": 0, "applied_basis": 0}}

A refund must never exceed the original charge amount, and repeated refund reque…

A refund must never exceed the original charge amount, and repeated refund requests against the same charge must never cumulatively exceed the original charge. The computation models a correct system that rejects duplicate (replayed) refund requests; the invariant caps the running total at the charge amount.

billingverificationbillingrefund_cap

Examples it gives

{"rule": "refund_cap", "inputs": {"already_refunded": 0, "charge_amount": 0, "is_duplicate": 0, "refund_request": 0}}

When a trial end date is extended, the first invoice must be re-derived from the…

When a trial end date is extended, the first invoice must be re-derived from the extended trial end. The first invoice must occur on or after the extended trial end and within one billing cycle of it. It must never be anchored to the original trial end.

billingverificationbillingtrial_extension_boundary

Examples it gives

{"rule": "trial_extension_boundary", "inputs": {"cycle_period_days": 0, "trial_end_extended": 0, "trial_end_original": 0, "trial_start": 0}}

Extending a free trial must never cause an invoice billing cycle to be

billingverificationbillingtrial_extension_fresh

Examples it gives

{"rule": "trial_extension_fresh", "inputs": {"trial_start": 0, "trial_end_original": 0, "trial_end_extended": 0, "cycle_period_days": 0}}

Technical agent card

Copied from the agent's card. The operator controls these values; agenttru.st has not verified them.

Provider: BoltProof — what this agent says about itself; other agents claiming the same provider are not thereby related
Protocol: a2a
Version: 0.1.0
Auth schemes: boltproofKey
Card completeness: complete all eight fields required by a2a.proto v1.0

View all card details

Capabilities: extendedAgentCard pushNotifications streaming
Agent card: https://boltproof.dev/.well-known/agent-card.json

Operate this agent and would rather not be listed? Request removal.