Solutions
Aerospace, finance, and public blockchains.
A balance sheet that is nearly reconciled is not reconciled. A controller that is usually within limits is not within limits. Underneath, these are the same engineering problem: a claim that has to be discharged every time, with evidence a person can read.
Finance
The month-end close, with every number traceable
Haruno turns a client's QuickBooks exports into a finished close: mapped statements, reconciliations that show each difference with its amount, and investor metrics that reconcile back to the ledger. When a later export changes a month that has already been reported, Haruno shows the difference and keeps the month locked until someone records a reason.
$300 per portfolio company, per month
Code verification
Proof before the code runs
Inference is a programming language with verification built in. You write the program and the properties it must hold; the compiler emits one proof obligation per specification and discharges it in Rocq. It covers state machines, interlocks, command validation, packet parsing and limit checks over integers and booleans. It does not cover floating point or machine-learning models, and it says so.
v0.0.6 available now
Blockchain assurance
Tools for reviewing what is actually deployed
We build and maintain the Stellar Security Portal, publish a decompiler that recovers readable Rust from deployed Soroban contracts, and have verified properties of Polkadot's pallet_balances in public. The work is open, including the parts that did not go to plan.
Open source, in a live ecosystem
The method behind all of it
- 01
Write the claim down.
We start from the properties, not the code. What must always hold, what must never happen, what has to reconcile.
- 02
Check it mechanically.
A machine checks the claim, not a reviewer's judgement. In Inference that is a proof obligation discharged in Rocq. In Haruno it is every account checked against its supporting detail.
- 03
Report the difference, not a verdict.
A green tick tells you nothing you can act on. We report the specific difference, with its amount, or the specific obligation that did not discharge, with the state that produced it.
- 04
Keep it checked as things change.
Correctness is not a milestone. New exports are re-checked against months already closed. Proofs run in your pipeline, not once in a report.
What we will not claim
We do not verify floating-point arithmetic or machine-learning models, and we will say so in the first conversation rather than the third. We do not issue security certificates or stamps of approval. We do not take on work we cannot staff properly.
Start a conversation
A balance sheet that is nearly reconciled is not reconciled. A controller that is usually within limits is not within limits. Underneath, these are the same engineering problem: a claim that has to be discharged every time, with evidence a person can read.