Products
What we build.
Five products, two of them commercial. Each one exists because a specific claim needed checking and nothing available checked it.
Products compared with services
Products are things you install or subscribe to today. Services are engagements where our engineers work on your system alongside your team. The two are connected: the services use the same tools, and the tools exist because of the service work. You can buy either one without the other.
| Products | Services | |
|---|---|---|
| What it is | Software you install or subscribe to | Our engineers working on your system |
| How it starts | Download it, or subscribe | A scoped conversation |
| Who operates it | You | Us, with your team |
| Price | Published or free. Haruno is $300 per portfolio company per month | Quoted per engagement, scope fixed before we start |
Inference
A programming language that AI agents can mathematically reason about.
Inference is a strict, structurally simple programming language with formal verification built into the language rather than bolted on. You write the program and the properties it must satisfy, and the compiler emits one proof obligation per specification and discharges it in Rocq. The language is deliberately small so that a reviewer and a coding agent can both reason about a program without guessing: no garbage collector, no heap allocator, fixed-size arrays and structs in WebAssembly linear memory, and integer overflow that traps unless you ask for wrapping.
- Version 0.0.6, installable with one command
- VS Code extension, tree-sitter grammar, published specification and book
- One proof obligation per specification, discharged in Rocq
- Publishes its own boundary: integers and booleans, not floating point or ML models
- Formal verification
- Rocq
- WebAssembly
- AI-assisted development
.inf
Specification
WASM
Binary
✓ Proof
Verified
▶ Run
Execute
Haruno
The month-end close for fractional CFOs on QuickBooks Online.
Haruno turns your clients' QuickBooks exports into a finished close. It maps each account to a statement line once, then flags anything it has not seen before instead of guessing. It reconciles every balance-sheet account against supporting detail and shows each difference with its amount. It explains what moved a line by naming the vendors and invoices behind it, computes the investor metrics each close and reconciles deferred revenue back to QuickBooks. Each reported month is locked: if a later export changes it, Haruno shows the difference and keeps the month locked until a reason is recorded.
- Four deliverables per close: portfolio dashboard, statement package, reconciliations, investor report
- Works from exports — QuickBooks, Stripe, HubSpot, Excel. No general-ledger access required
- $300 per portfolio company, per month
- Names a missing input rather than estimating one
- Month-end close
- QuickBooks Online
- Reconciliation
- Investor reporting
“Draft this month’s management report.”
Stellar Security Portal
formerly Soroban Security
The security hub for the Soroban ecosystem.
Stellar Security Portal is the reference point for security work on Stellar's Soroban smart contract platform: audit history, tooling, and the reviewers who have put Soroban projects through their paces. We built it and we maintain it. It is the clearest answer we have to whether we ship and operate real systems rather than only writing about them.
- Audit history and findings across the Soroban ecosystem
- Security tooling and guidance for contract authors
- A directory of reviewers who have worked on Soroban projects
- Open source, around 50 stars on GitHub, built and maintained by Inferara
- Soroban
- Stellar
- Smart contract security
Audit history
Public
Soroban Decompiler
Read a deployed Soroban contract back as Rust.
soroban-ret is a reverse-engineering tool for Stellar Soroban smart contracts. It takes the compiled WebAssembly that is actually deployed and recovers readable Rust, so a reviewer can analyse what is running on the network rather than what the repository says should be running. Small, written in Rust, Apache 2.0, and used in our own review work.
- Recovers readable Rust from deployed WebAssembly
- For reviewing what is on-chain, not what is in the repository
- Rust, Apache 2.0, small enough to audit yourself
- Part of the toolchain we use on Soroban engagements
- WebAssembly
- Rust
- Reverse engineering
0061 736d 0100 0000
0107 0160 027f 7f01
7f03 0201 0007 0b01pub fn transfer(
env: Env,
from: Address,
amount: i128
) -> Result<(), Error>Inference Studio
Debug specifications and complete proofs.
Inference Studio is a working environment for the parts of verification that are still slow by hand: understanding why an obligation will not discharge, and finishing proofs that are nearly, but not quite, done. It is in development and we have not announced a release date. If this sits on your critical path, tell us what you are verifying and we will keep you informed.
- Inspect a failing proof obligation and the state that produced it
- Proof completion for obligations that are nearly discharged
- Built on the Inference toolchain
- In development. No release date announced
- Proof automation
- Debugger
Not sure which of these fits?
Tell us what you are working on and what has to be true about it.