Verification & Bench
OiC.OS delivers verified accounting: not a dashboard claim, but checks that survive load. This page states what we verify, at which economic scale we think, and how categorical invariants (QEB, Noether / gauge, adjunctions) fit the product story.
For the operator view of certificates and ClosedMacro, see Help — ClosedMacro & invariants.
Why verification is the product
Enterprise systems already post millions of lines. The hard question is whether the institution still makes sense: bilateral mirrors closed, contracts inside their type, macro aggregates consistent with micro bookings, learning steps that do not break the Sim⊣Est adjunction.
We treat those as invariants of the model, checked on every run — Acc CERT, gold / paper / Agda-style chips in the workbench — not as a quarterly reconciliation project.
Scale ladder (accounting load)
Orders of magnitude we use when talking about corporate and systemic load (ledger postings, not only RTGS):
| Stage | Rough size | Bookings / day (order) |
|---|---|---|
| 1 Konzern (one large group) | ~30 000 accounts | ~500 000 |
| DAX40-class index | ~40 groups | ~20 000 000 |
| Currency-union class | ~1 000 group-equivalents | ~500 000 000 |
These are planning units for AccCat / DEB stress — Pacioli balance must stay true under streaming postings. GPU acceleration helps the Acc kernel (cyclic DEB / Pacioli); it is not a substitute for Gov and Dec consistency on the full OS.
QEB versus “books that only look closed”
Classical double entry (DEB) is necessary honesty inside one entity. Business between agents needs quadruple-entry bookkeeping (QEB): my receivable is your payable, mirrored in real time. OiC.OS AccCat is built for that bilateral discipline.
| Check | Meaning |
|---|---|
| Pacioli / DEB balance | Debits equal credits in the streamed posting set |
| QEB mirrors | Bilateral claims stay paired across counterparties |
| Macro / sheaf glue | Local Acc / Dec / Gov sections at time t glue to one global state |
| Gov WITHIN | Fired contracts stay inside the typed institution |
Noether, gauge, adjunctions
Category-theoretic language is not ornament; it names the conservation laws we want on the books:
- Noether-style invariants — symmetries of the institutional “action” that yield conserved quantities (e.g. balance identities that survive admissible rewrites).
- Gauge — freedom in how you present accounts that must not change observable settlement; illegal gauges are rejected.
- Adjunctions (Sim ⊣ Est) — simulation produces Audit series; estimation / Expr learns structure or parameters back into the model; the fixpoint (
lib expr fixpointin the workbench) is the counit of that adjunction. - ClosedMacro — standing view of Unit / Counit, sheaf snapshot, dual / coplay — the place where “the macro closed” is made visible.
Together: QEB + Noether / gauge + adjunction invariants = verified accounting under redesign, not only under steady posting.
What a bench run answers
A serious bench answers, for a chosen scale:
- Did Pacioli (and QEB mirrors where modelled) stay balanced?
- Did institutional certificates (Acc / Gov / Dec / sheaf / terminal) remain ok?
- What throughput (bookings per second) did the Acc kernel achieve on CPU / GPU?
It does not by itself prove that your CRM or WMS screens are pretty. It proves that the spine you orchestrate them with still closes.
Economics kernels under load
We grow verification along the same ladder as content:
einbank → zweibank / dreibank → liquipool / supplychain → holding- and union-scale Acc stress.
Product pages: Modeling Service · LiquiPool · Islamic Banking · Worlds.
Access
Public site: this documentation. Live bench and workbench: team Tailnet (test.app.oicos.systems). Collaboration: contact@oicos.systems.