K∴

kar-tally

deterministic budget-cap ledger auditor
SOVEREIGN · 1 FILE OFFLINE-CAPABLE NO LLM JUDGE

1 What this is

An AI agent (or any automated system) is given a spending cap and a log of actions it took, each with a cost and a running balance it claims to have left. kar-tally recomputes that log from scratch — cap minus cumulative cost, step by step — and reports whether the claimed numbers are actually consistent with the raw entries, whether the sequence has any gaps or duplicates, and whether the cap was ever exceeded at any point, even if a later entry's claimed balance was edited to hide it.

There is no model in the loop. The verdict is pure arithmetic and comparison over the numbers you give it — anyone can take the same entries and cap, redo the same three checks by hand, and get the identical PASS/FAIL. That's the whole proof.

! Honest limits

This tool proves internal arithmetic consistency of a ledger you provide — it does not know whether the ledger matches what actually happened outside the browser (a real API bill, a real token meter). It trusts that each row's seq number genuinely corresponds to one real event; if an attacker rewrites every field of an entry consistently (cost, balance, and reuses the next seq), this check alone cannot detect that the underlying event was fabricated — it can only prove the numbers you handed it are self-consistent (or aren't). Pair it with an independent event source (server logs, provider invoices) for full assurance. It is a consistency and tamper-evidence check, not a live billing feed.

2 Ledger input

balance = the claimed running balance after this entry's cost is deducted.

3 Verification result

NOT RUN Click "Verify ledger" to recompute the entries on the left.
  • No violations to show yet.
#seqactoractioncostclaimed bal.recomputedok
SHA-256 fingerprint of this input—

4 Live self-test

Runs six known ledgers — one clean, five deliberately tampered in different ways — through the exact same verifyLedger() function above, and checks that each one is judged the way it honestly should be. This is the end-to-end proof that the auditor actually catches what it claims to catch.

View the exact verifier source running on this page