Money maths you can prove — to the penny.
A library of financial calculations that are formally verified: every figure is computed in whole pennies — no floating point ever touches money — and every calculation carries a machine-checked proof that it equals its specification exactly. Not “well tested.” Proven. Callable from Excel, VBA, C#, Python, Java, Go — anything that speaks C.
“Don’t lose your money, honey — use formally proven software.”
The proof, not a promise
Discharged by gnatprove at level 3, and re-checkable from source —
the proof isn’t a claim in a brochure, it’s a command you can run yourself.
The value you buy is audit time you don’t spend.
What it computes
Money core
Add & subtract, apply-rate, round half-even, N-way / weighted / pro-rata splits — penny-exact, shares always sum to the total.
Interest & time-value
Simple & compound interest, present value, amortization that reconciles to the penny, APR checker, Rule of 78.
Tax & statutory
Income tax, the means-test taper, National Insurance, VAT (forward & reverse), SDLT, CGT, gross-up, and a progressive-band primitive that composes any jurisdiction’s brackets.
Markets & dates
FX, margin / markup, stacked discount, break-even, commission, LTV, depreciation, and leap-correct day-counts (30/360, ACT/365F, ISDA Actual/Actual).
Built for the audit, not just the answer
- Penny-exact by construction. Integer minor units throughout — no floating-point rounding can creep into a balance.
- Bad input can’t reach a calculation. An out-of-bounds call returns a status code naming which bound broke, and never echoes the value.
- A tamper-evident record. An append-only, hash-chained ledger of what was computed — alter any field and the chain breaks.
- A receipt that binds the figure to the proof. Each run produces a re-checkable stamp tying this output, from this binary, to the proof that backs it.
- One engine, every jurisdiction. Rates and thresholds are inputs, not hard-coded — proven once, for all inputs, so there’s no per-country fork to drift.
Two certificates, one codebase
The calculation never changes — you choose how deep the proof goes.
| Tier | What it guarantees |
|---|---|
| Lite · free | Absence of runtime errors — won’t crash, overflow, or corrupt. |
| Hallmark | Every calculation provably equals its specification, re-checkable from source. |
Drop it into what you already use
On Windows it ships as a single self-contained DLL — the runtime is baked in, so the
customer installs nothing. Bindings for Excel / VBA and C are included; from any language
that speaks C, you call the prudence_* functions with amounts in pennies.
UK timezone · every enquiry is read and answered by a human · typical reply within one working day.