Why a CFO can trust every number
Harbor does not predict tax answers — it proves them. Every determination in this engagement is a machine-checked mathematical proof, derived from the encoded statute and Hearthstone's own data, and re-checkable independently. This is what makes the output audit-defensible rather than merely a CPA opinion.
Probabilistic in.
Deterministic out.
Frontier language models are right most of the time and confidently wrong the rest — a coin-flip you cannot stake a $3M audit position on. Harbor encodes the actual statute into formal logic and proves the answer follows from it. When it can't prove, it says so.
Accuracy on the standard SALT benchmark
Held-out determinations, scored against ground truth
Frontier and probabilistic tax models predict an answer and attach a confidence. Harbor returns a proof — or abstains. The gap is the difference between “likely right” and “provably correct.”
The four-stage verification pipeline
From raw statute to a proof a CFO can read
Formalise the domain
Every relevant sales-tax statute and regulation is encoded once, by jurisdiction, into Catala (a formal language purpose-built for legal rules) and compiled to Lean 4. Laws become machine-checkable axioms. A CPA reviews the back-translation of each encoded rule against the original statutory text before it enters the corpus.
Auto-formalise the problem
Hearthstone's raw data — NetSuite GL, Shopify orders, Amazon settlements, ADP payroll, fixed-asset register, Concur T&E — is auto-formalised into structured facts. A human-in-the-loop edit layer lets the CPA ratify that each extracted fact matches the source. Nothing displayed is invented: every figure grounds to a fact in the Lean file or a raw input the client provided.
Prove or solve
The question becomes a theorem; the facts and assumptions are its hypotheses. Harbor's prover discharges the goal — roughly 90% via SMT solvers, the remainder with Lean tactics. If the answer cannot be derived from the corpus, Harbor returns 'cannot prove' rather than guessing.
De-formalise (back-translate)
The machine-checked proof is back-translated, line by line, into the language a VP of Tax or CFO reads — every step tied to a statutory citation. This is the audit-defensible determination trail: not a CPA's opinion, but a verifiable chain from statute to conclusion.
A proof, end to end
Idaho nexus — physical presence via a single remote employee. The same artifact a CFO reads in English, the kernel checks in Lean.
We are determining whether Hearthstone has nexus — a tax-collection obligation — in Idaho. Under U.S. law (post-Wayfair 2018), nexus arises through either (1) physical presence in the state, or (2) economic activity exceeding the state's statutory threshold.
Physical-presence test — SATISFIED. Hearthstone employs a remote worker physically located in Idaho (Senior UX designer (e-commerce team) working remotely from Boise — W-2 coded to ID since hire). Physical presence of property, payroll, or inventory creates nexus on its own and is dispositive: once present, the dollar and transaction thresholds need not be reached.
Economic-nexus test — SATISFIED. Idaho sets a single threshold of $100,000 in gross sales, measured over the previous or current calendar year. Hearthstone's peak rolling-12-month remote gross sales into the state reached $10,274,416, which exceeds the threshold. (Idaho Code § 63-3611(3)(b))
Conclusion: Hearthstone HAS nexus in Idaho on both physical and economic grounds. A registration and collection obligation exists.
-- Harbor ASI · Nexus formalisation
-- Jurisdiction: Idaho (ID)
-- Statute (economic): Idaho Code § 63-3611(3)(b)
-- Corpus: salt-us-2026.06 · grounding: Hearthstone facts (autoformalised)
namespace Harbor.Nexus.ID
/-- FACTS (autoformalised from client source systems) -/
def Fact_physicalPresence : Prop := True -- remote-employee
def Fact_remoteSales_rolling12 : ℝ := 10274416 -- USD, peak preceding-period gross
def Fact_remoteTxns_rolling12 : ℕ := 107416 -- retail transaction count, same period
/-- STATUTORY THRESHOLDS (axioms — Idaho Code § 63-3611(3)(b)) -/
axiom Threshold_amount : ℝ
axiom Threshold_amount_eq : Threshold_amount = 100000
/-- NEXUS PREDICATES -/
def hasPhysicalNexus : Prop := Fact_physicalPresence
def hasEconomicNexus : Prop := Fact_remoteSales_rolling12 ≥ Threshold_amount
def hasNexus : Prop := hasPhysicalNexus ∨ hasEconomicNexus
/-- DETERMINATION -/
theorem nexus_established : hasNexus := by
unfold hasNexus hasPhysicalNexus hasEconomicNexus
left -- physical presence is dispositive
simp [Fact_physicalPresence]
#check @nexus_established
end Harbor.Nexus.IDFive principles behind the trust
Grounded, not generated
Every number on screen traces to either a fact in the Lean formalisation or a raw input the client provided. There is no intermediate, unverifiable layer.
Statute as axiom
Encoded law is treated as axiomatic. Conclusions are theorems proven from those axioms plus the client's facts — the same discipline used to verify aerospace and chip-design systems.
It says when it doesn't know
Where the corpus contains no controlling authority, Harbor reports 'cannot prove' and recommends a documented protective position — it never fabricates certainty.
Adversarially complete
Each judgment-call determination carries the strongest counter-argument an auditor could raise and Hearthstone's rebuttal — the memo is built to survive challenge, not just to state a position.
Human-in-the-loop on facts, machine-checked on logic
A CPA ratifies the extracted facts and assumptions. The reasoning from facts to conclusion is machine-verified and needs no trust — it can be re-checked independently.