IronCI
A checked proof is the one judge an agent cannot talk into saying yes.
Mission. Make trustworthy software scale as fast as software creation: assurance that travels with the software, and less exposure to its authors.
A codex of every attempt to bind a made mind, from clay and bronze to English and test suites, and of the binding we build: independently checkable proofs of compatibility and specified security properties for dependency rewrites, under explicit assumptions. What cannot be proven stays Unknown.
welcome to the desert of the real
An attack needs one witness. A defense must show there are none.
Every security claim has a logical shape, and the shape decides who wins. Scanners, evals, red teams and LLM judges hunt for ∃. When a non-exhaustive search finds nothing, that is evidence, sometimes good statistical evidence, but it does not establish the universal claim. Runtime monitors that block forbidden operations are different: they enforce a policy, and they complement proof.
Offense. One input, one path, one stolen token. Right once, anywhere.
Defense. No witness exists, on every admitted execution, and the claim can be re-checked by anyone.
Program testing can be used to show the presence of bugs, but never to show their absence!E. W. Dijkstra · Notes on Structured Programming · 1970
Even a strong finder leaves known holes. Aikido's Altar, an open-weight security model released September 21, 2026, was scored on 32 known vulnerabilities across 30 repositories and found 23 of them at least once. Compressed for on-premises use, it kept 23 of the 25 its parent model found, with average recall 5.2 points lower. 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. Better models are supply, not competition.
Aikido · “Altar” · Sept 21, 2026 · internal benchmark · three runs per casenine witnesses walked past the hunt.
the territory no longer precedes the map
Nearly four thousand years of trying to bind what we build.
Each entry is tagged by how it tried to constrain its creature. Words, tests and judges are ∃: they fail to one counterexample. Proof is ∀. Some texts mark the edge of proof itself, and those we tag Unknown, because not-knowing never becomes a pass. Open any entry.
the shoggoth may wear any mask. the checker reads no faces.
The whole safety case of the creature was one character wide.
In golem legends written down from the seventeenth century on, the creature was animated by a word on its forehead: emet, truth. (The best-known golem, attached later to Rabbi Judah Loew of Prague, was usually animated by a name placed in its mouth.) Erase the first letter and it reads met, dead. Its spec was a single glyph, and anyone who could reach its face could edit it.
A constraint the creature can reach is a suggestion. IronCI keeps the proposer away from the tests, the credentials and the deploy key, and puts no model in the trusted base, ours included.
Model provenance is now a security question, and regulated buyers want security AI that keeps their code inside. There are two ways to answer them.
Host the model
Aikido's answer for banks, hospitals and industrial operators is Altar, a 328 GB security model that runs inside the customer's own infrastructure, air-gapped if need be. That controls where the code goes. It cannot show the weights deserve trust: Altar's base model, GLM-5.3, comes from Z.ai, on the U.S. Entity List since January 2025 and named in the September 8, 2026 NSA/CISA/FBI advisory on distillation. At 60% recall, a planted blind spot looks like an ordinary miss.
Run the checker
Ours needs no custody of your code. The package being replaced is already public, reachability runs on your side, and only the list of reachable entry points leaves. You re-check each certificate with a small checker inside your own network, and never host our prover or trust our model. Whoever trained the proposer, the proof checks or it does not. The checker protects the output, not the license, so for procurement and pedigree we still propose with U.S.-origin open weights: gpt-oss, Inkling, Nemotron. This is a product rule before customer one.
Aikido, Sept 21, 2026 · Federal Register, Jan 16, 2025 · NSA/CISA/FBI AA26-251A, Sept 8, 2026 · after Chaum, 1985, and Necula & Lee, 1996
the bitter lesson, footnote: someone has to grade the search
Nine candidate rewrites of left-pad. One weak test suite approves all of them.
Each candidate imitates the way agents write, including the ways they cheat. The three-case test suite is deliberately weak: every case has n equal to the string length, so none tests padding. One ordinary case, ("a", 3, " "), would catch three of the candidates. The point is narrower than “tests fail”: passing a suite certifies only the suite. The reference P is leftPad, the eleven-line package whose removal from npm broke builds across the ecosystem in March 2016; P here is a simplified equivalent. The domain I is every string over {a, b} up to length 3, every width 0 to 5, fill " " or "0": 180 inputs, checked exhaustively. Equivalence here is a real proof by exhaustion over that finite domain, assuming the JavaScript runtime behaves as specified. Security is not proven here: the φ column is a keyword scan, and one candidate shows how easily a scan is fooled.
Test suite · 3 cases · deliberately weak
Equivalence · ∀ i ∈ I
Policy scan · illustrative, not a proof
Proof is expensive, so it is spent last. The pipeline runs in the order the alchemists ran theirs: dissolve what is false, purify what repeats, and only then fix what remains.
Disproof
Every candidate runs differentially against the original. One mismatch kills it. This is an ∃ question, and it costs about as much as running tests.
Group
Candidates that behave identically on the differential tests T are grouped, and proof effort goes to one of each group. This is a heuristic, not a proof of equivalence: it can discard a correct candidate and keep a wrong one. That can cost success, never soundness, because acceptance still requires the proof. In Bad Theory Labs' code experiment, 83% of generated programs were merged this way, on test behavior.
30 MBPP problems · Qwen3-1.7B · solved 9/30 vs 8/30 for best-of-N, which the authors call within noise · our rate will differProof
Only the survivor gets ∀ effort, over a domain I backed by a sound reachability argument, not just the calls observed in testing. The stone is a certificate anyone can re-check.
cost(check π) ≪ cost(find π) · a hypothesis the pilot measures, not a theorem
Unknown routes to a human. Not-knowing never becomes a pass. We never say “unhackable.”
A sound proof establishes its formal property under its assumptions, and nothing more. A certificate is only as good as the four things it names.
- SpecificationCompatibility on the stated domain I, and each security property φ. A reference reduces the work of specifying compatibility; φ, the permitted inputs, the observable effects and the environment are still written down. If the reference itself does something φ forbids, the two conflict, and the answer is Reject or Unknown, never a quiet pass.
- CoverageHow I was derived. A sound reachability argument, not calls observed during testing, which say nothing about other production executions.
- Trusted baseThe proof checker, the model of the runtime and environment, the compiler and build. Side channels and anything the model omits are out of scope and listed as such.
- BindingThe hash of the exact artifact the proof covers, so the certificate cannot be attached to a different build. Compare the seL4 project's published proof assumptions.
well-typed programs can't be blamed.
Everyone else verifies programs. We verify boundaries.
A boundary is the surface where code you didn't write meets code you did. The insight that a reference supplies the specification is not unique to us: Theorem already sells equivalence proofs for refactors and translations. A target can be copied. What separates IronCI is an approach.
Boundaries, not whole programs.
A whole-program guarantee arrives only when the whole program is specified and proven. We prove the part of a dependency that a sound reachability argument says your code can reach, and leave the rest of the codebase as it is. Proven and unproven code coexist, and proof arrives one dependency at a time, the way types entered real codebases through gradual typing. Everything outside the boundary is named Unknown, and the boundary is exactly where chalk and axios came in.
Adversaries, not just intent.
Equivalence preserves whatever the original does, including what an attacker wants. If the reference has a prototype-pollution bug, or 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.
Checkers, not bigger models.
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 never make an accepted certificate more trustworthy, because the model was never in the trusted base.
Racket's 2018 SIGPLAN Software Award citation credits it with generalizing software contracts to higher-order settings and helping launch gradual typing. Jay McCarthy is one of its seven named recipients, with Robert Bruce Findler, Matthias Felleisen and Sam Tobin-Hochstadt.
- 2002Higher-order contracts · Findler & Felleisen, ICFP. Behavior is checked where one component meets another, and blame goes to the side that broke the contract.
- 2006Gradual typing · Tobin-Hochstadt & Felleisen; Siek & Taha. Checked and unchecked code coexist in one program.
- 2009The blame theorem · Wadler & Findler, ESOP.
when a program integrating less-typed and more-typed components goes wrong the blame must lie with the less-typed component.
- 2018Gradual program verification · Bader, Aldrich & Tanter, VMCAI. The same idea, carried from types to proofs. We apply it to machine-written changes.
Two limits, stated first: 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 the pilot measures.
as above, so below
Every mechanism in the machine has an older name.
The Hermetic doctrine of correspondences held that each thing below mirrors something above. Read each row two ways: on the left, what IronCI does; on the right, the idea it echoes.
a theory that can't be wrong isn't one. K.P.
Seven things we take as given, one we are testing, and where each comes from.
there is no spoon. there is only ⊢
Ask the checker something.
Type help. The help text is an ∃ claim: it lists some commands, and never proves it lists all of them.