Finance, billing and risk
Calculations that do not go wrong silently: the balance converges to absolute, and the rounding remainder stays visible instead of being lost. For areas where a wrong number costs money and has to be audited.
Numerical library · PyPI 1.1.0 · Lean 4
Balansis Active Development
A computation library in which division by zero, overflow and loss of precision do not crash the calculation but become explicit and auditable. The algebra of the model is proved in Lean 4; the code is open on PyPI (1.1.0, AGPL-3.0 or a commercial licence).
The problem
Ordinary float arithmetic silently loses significant digits when it adds quantities of different magnitudes (catastrophic cancellation) and returns nan/inf on overflow. The error raises no signal — it simply corrupts the result further down the pipeline: a financial calculation, an engineering simulation or an ML normalisation produces a plausible but wrong number.
Why existing solutions fail
A naive float sum discards the rounding remainder without a trace. Individual compensation techniques exist, but they are usually not type-safe and not formally verified — they cannot be trusted where correctness has to be proved rather than declared: billing, risk, regulated calculations.
How it works
Every addition keeps its rounding remainder, and the remainder is carried forward instead of being thrown away; the result is typed. The baseline for a fair comparison is the naive sum, not Kahan: the differentiator is explicit, auditable compensation, not a claim of “higher accuracy”. At its base is an experimental computational model (ACT); the code is open, and the algebra of the model is proved in Lean 4 over ℝ — float64 behaviour is not formally proved.
Demo
Technology
- Python
- Lean 4
- NumPy
- PyPI
- mypy strict
Use cases
Engineering simulations and ML normalisation
Stable aggregation of quantities of different magnitudes and an overflow-safe softmax on large logits — stable probabilities instead of nan.
Regulated domains
Proofs, not declarations: the algebra of the model is proved in Lean 4 — an argument where properties have to be shown to a reviewer. These proofs do not cover float64 behaviour.
Evidence
Formal proofs in Lean 4: 153 theorems about the model, zero gaps
The formal project builds without a single sorry/admit — the proofs exist and pass the checker; they are not just claimed in words. What is proved is the algebra of a model isomorphic to ℝ; float64 behaviour is not formalised. Count as of 05.10.2026.
Reproduce: lake build + grep -r "sorry\|admit" formal/
Catastrophic cancellation: naive = 93 (wrong) vs compensated = 3333
On a documented scenario the naive float sum gives 93 and the compensated one gives 3333, which matches the Decimal reference. The baseline is the naive sum, not Kahan.
Reproduce: pytest tests/test_documented_scenarios.py
Overflow-safe softmax: naive = nan vs stable probabilities
On large logits the naive softmax returns nan; the compensated one returns valid probabilities, sum = 1.
Reproduce: pytest tests/test_documented_scenarios.py
Test run: 870 passed, 0 failed
The test suite passes with no failures — laboratory branch (1.2.0, not yet released), pure-Python path, 05.10.2026. Line coverage is 76% against the project’s own threshold of 80%.
Reproduce: pytest
Integration
A Python library (PyPI). It goes into the calculation layer in place of naive arithmetic — where loss of precision is unacceptable.
Cost the effect on your own figures
AVA is a process-economics calculator. In a couple of minutes it shows whether this pays off in your case — before any call, with no commitment.
Estimate with AVALet us look at your task
Tell us what needs solving. If it cannot be solved or will not pay off, we will say so up front, before any work starts.
or write to us directly: hello@xteam.pro