Skip to main content

Mathematically correct software for aerospace and finance.

Two products for work where a green tick is not evidence. Both publish the list of what they will not do.

Start a conversationSee what we build

“God made the integers; all else is the work of man.”

Leopold Kronecker · 1823–1891

Inference — a programming language
The proof is in the compiler, not a tool bolted on afterwards. What you keep is a machine-checked Rocq proof your own engineers can re-run, not a report saying someone looked.
Haruno — month-end close software
Every account reconciled against its supporting detail, every difference shown with its amount rather than a pass mark. A month you have reported cannot change quietly. $300 per company, per month.

Checkable facts

v0.0.6
Inference, installable today with one command
Rocq
One proof obligation per specification, discharged in Rocq
150+
Stars across our open-source tools on GitHub
23
Research papers and technical articles, published in the open

What we work on

Flight software, financial statements, and code already deployed.

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

How we work

What “mathematically correct” means here

Say what must be true.

Correctness starts as a written claim: an invariant, a reconciliation, a limit. A property that is not written down is not being checked, however carefully the code was reviewed.

Check every case, not some of them.

A test covers the inputs someone thought of. A proof covers all of them. Inference discharges one proof obligation per specification in Rocq. Haruno checks every balance-sheet account against its supporting detail rather than a sample, and reports each difference with its amount.

Fail loudly.

The failure we design against is silence. Inference traps integer overflow unless you ask for wrapping. Haruno names a missing input instead of estimating around it, and will not quietly restate a month that has already been reported.

Work with our engineers

Some problems are not a product. When a design decision is expensive to get wrong, our engineers work on your system alongside your team, on a scope fixed before we start.

  • Specification and verification review. Two weeks.
  • Verification sprint. Four to six weeks.
  • Embedded verification practice. Quarterly.
  • How we work

Evidence

How you can check us

We are not going to show you client logos. Our engagements are confidential and we are not going to invent references. What we can show you is the work itself: four research papers, nineteen technical articles, a published language specification, and every tool we have built, in the open, with its history.

Start a conversation

Tell us what you are working on and what has to be true about it. An engineer reads every message and replies.

Start a conversation
info@inferara.com