We built a non-LLM reasoning engine for binary analysis. It didn't work.

By The Rutken team

755,842 claims produced on real binaries; zero survived ablation. The terminal reading was B: the engine generates claims, and not one holds up once the analyst’s authored seed is removed. We measured that and parked the engine. What follows is how it failed. The failure is the interesting part.

This is a post-mortem of a thing we built and then parked. Not a product announcement, not a "lessons learned" that secretly sells you the lessons. We spent a long run of phases building a reasoning layer over our static-analysis IR (no model, no embedding, no learned scorer) to see whether an analyst's "huh, that's odd" could be produced mechanically. The terminal reading was B: claims are produced, none survives ablation. We parked it. The engine is still in the tree, still green, and not wired into anything you can buy.

We think the way it failed is more interesting than most things that work, because the architecture was built to diagnose its own failure and it did: it located the limit in one named lattice property, against the outcome we wanted. Here is the whole thing.

The premise: no model anywhere in the core

The brief was a constraint before it was a feature. The brief, in the words of the person who set it:

"Don't try to make Rutken 'think like an expert.' Make it notice the things an expert notices because they're mechanically detectable."

No LLM anywhere in the core. No model, no embedding, no learned scorer.

So the model (we called it "mechanical intelligence") is a product of five typed factors, and the output is a derivation, not a score:

Mechanical Intelligence
  = Typed Primitives
  × Typed Operators
  × Abstraction Functions
  × Bounded Search
  × Corpus Priors          (optional, maturity-dependent)

A Lead carries no confidence field, on purpose: the derivation is the explanation. An analyst who disagrees challenges a node or an edge in the chain, not a number. It all lives in one crate, which depends on ir and nothing else: it holds opaque ProgramPoint handles and never names a MethodId, a Cfg, or a TaintPath. A layering test enforces that by source scan. The point of that discipline is that whatever the graph concludes, it concluded from typed, inspectable facts and nothing smuggled in.

The killer property: ablation

The whole program hinges on one question: did the engine derive a relationship, or did it retrieve one a human had already authored into the catalogue? The evidence graph tags every fact and every edge with its provenance (Authored, Extracted, Derived), and ablate_authored() deletes everything authored, then transitively deletes anything that depended on it, by fixpoint:

pub fn ablate_authored(&self) -> EvidenceGraph {
    // seed the deleted set: every authored fact, every authored edge
    let mut deleted_facts: BTreeSet<FactId> = self.facts.iter()
        .filter(|f| matches!(f.provenance, FactProvenance::Authored { .. }))
        .map(|f| f.id).collect();
    let mut deleted_derivs: BTreeSet<DerivId> = self.derivations.iter()
        .filter(|d| matches!(d.provenance, EdgeProvenance::Authored { .. }))
        .map(|d| d.id).collect();

    loop {                                        // transitive deletion to fixpoint
        let mut changed = false;
        for deriv in &self.derivations {         // consumes a deleted fact -> deleted
            if !deleted_derivs.contains(&deriv.id)
                && deriv.inputs.iter().any(|i| deleted_facts.contains(i)) {
                deleted_derivs.insert(deriv.id);
                changed = true;
            }
        }
        for deriv in &self.derivations {         // output of a deleted edge -> deleted
            if deleted_derivs.contains(&deriv.id) && deleted_facts.insert(deriv.output) {
                changed = true;
            }
        }
        if !changed { break; }
    }

    // replay each SURVIVING derivation through apply() against its
    // remapped (surviving) inputs -- recomputed via combine_attrs, never copied,
    // so the output's invariants hold by construction rather than by re-checking
    let mut out = EvidenceGraph::new();
    let mut fact_map: BTreeMap<FactId, FactId> = BTreeMap::new();
    for fact in &self.facts {
        if deleted_facts.contains(&fact.id) { continue; }
        if let FactProvenance::Extracted { extractor } = &fact.provenance {
            let new_id = out.add_extracted_fact(fact.kind, fact.subject.clone(),
                fact.location.clone(), fact.attrs.clone(), extractor.clone());
            fact_map.insert(fact.id, new_id);
        }
        // Derived facts are re-minted below, alongside their replayed edge
    }
    for deriv in &self.derivations {
        if deleted_derivs.contains(&deriv.id) { continue; }
        let Some(mapped_inputs) = deriv.inputs.iter()
            .map(|i| fact_map.get(i).copied()).collect::<Option<Vec<_>>>()
        else { continue };                        // fixpoint guarantees inputs survived
        let Some(output_fact) = self.fact(deriv.output) else { continue };
        if let Ok((new_output, _)) = out.apply(deriv.operator, &mapped_inputs,
            output_fact.kind, output_fact.subject.clone(), output_fact.location.clone(),
            deriv.provenance.clone(), deriv.status.clone(), deriv.evidence.clone()) {
            fact_map.insert(deriv.output, new_output);
        }
    }
    out
}

A claim survives ablation operationally: after you remove every authored seed and everything causally downstream of a seed, the claim's endpoint facts are still connected by at least one relational edge carrying a non-empty evidence witness. That is the definition of ClaimOrigin::Derived: "the claim's endpoint facts have no common authored ancestor, and the DAG contains at least one relational edge with a non-empty evidence witness connecting them." If a single authored fact dominates every relation edge, the claim is Retrieved, and ablation deletes it. There is no public constructor for the origin tag; it is computed from DAG shape by the graph's own walk, so you cannot hand-assemble a claim that lies about where it came from.

The walk is a real dominator check, not a flag. The leaves are the provenance DAG's own sources; fact_reaches_excluding asks whether a leaf can still reach the claim's terminal fact with one authored point removed. If every leaf is cut off by removing a single authored point, that point dominates and the claim is Retrieved; otherwise it is Derived. The predicate reads only provenance and reachability (never an Operator discriminant), so a future operator that carries a witness classifies correctly with no change here:

// compute_claim_origin(ancestry, terminal)
// a witness = a Provenance edge carrying non-empty evidence
let witnesses = ancestry.iter().filter_map(|id| self.derivation(*id))
    .filter(|d| d.class == EdgeClass::Provenance && !d.evidence.is_none())
    .count();

// an authored point DOMINATES iff removing it disconnects every
// leaf of the provenance DAG from the claim's terminal fact
let dominator = authored.iter().find(|&(&point, _)| {
    leaves.iter().all(|&leaf|
        leaf == point
        || !self.fact_reaches_excluding(leaf, terminal, &deriv_set, point))
});

match dominator {
    Some((_, catalogue)) => ClaimOrigin::Retrieved { authored: catalogue.clone() },
    // authored material is present but does not dominate: some leaf
    // still reaches `terminal` without passing through it
    None if !authored.is_empty() && witnesses >= 1 =>
        ClaimOrigin::Mixed { authored: /* any participating catalogue */, witnesses },
    // no authored point dominates (or none exists at all)
    None => ClaimOrigin::Derived { witnesses },
}

We pre-registered the readings before the first corpus run

The failure mode we were most afraid of is the one where you run the search, look at the output, and then decide what counts as success. So the readings were fixed in writing first, verbatim, before any measurement:

A  claims ≈ every eligible pair  -> discriminates nothing.
                                       The search is a cross-product. Not MI.
B  claims are selective, but none survives ablation
                                    -> the composition is authored;
                                       the graph retrieved it. Not MI.
C  selective AND some survive ablation, but every provenance link is
     Assumed/CoLocation           -> a real result and a weak one.
                                       correlation, not derivation.
D  selective, survives ablation, AND at least one claim's relation rests
     on an Established provenance link                 -> this is the thing.

Only D is MI as claimed. C is worth having and must not be reported as D.

The pre-registered expectation, also written before the run, was A or C, because the search composed facts only via co-location (Correlate over things that occur together), and no search operator chained through the Trace/Propagate provenance edges that would make D reachable. Naming the weak relation up front ("co-location across a domain difference, not the same value flows from one to the other") is what stops it being described later as something stronger.

The result: 755,842 claims, zero survivors

We measured at a deliberately absurd budget (1000× the shipped default) on a subset chosen so two tiny apps could run to complete, uncapped search exhaustion (exhausted_max_hops = true, truncated_by_max_generated = false). The numbers:

Correlate-rooted claims, subset-wide              755,842
  surviving ablate_authored()                           0
  per-app survivors                             0/6 apps

claims with ≥1 Established provenance link anywhere   0 / 755,842
chained_via_witness (both sides carry a real
   Trace/Propagate witness of differing OriginKind)     0  (across 828,920 derivations)

This is reading B, unambiguous. Selective (about 0.4 of eligible pairs subset-wide, not a cross-product, rules out A), but nothing survives ablation (rules out C and D). The thing that makes it decisive rather than another underpowered zero: on the two apps searched to exhaustion, the zero is at 100% coverage. As the adjudication put it:

Every previous zero in this programme was qualified by coverage. This one is not. At complete search exhaustion, the chained route never fires and no claim carries an established provenance link. The limiting factor is not search budget. That hypothesis is now excluded on evidence rather than argument: the search was allowed to run to completion and found nothing.

An independent agent, working the same question from scratch and unaware the branch had advanced, re-ran it over 26 of 27 apps with independently written witness walkers: 23,571 eligible facts, 11 with any witness (0.047%), zero pairs with a witness on both sides, corpus-wide. Same verdict, forty times the sample. Witness density fell with scale (0.37% → 0.047%), which is the opposite of what a small-sample artifact would do. The search budget was never the limiter; the witness supply was.

Why the witnesses were not there: a lattice tells you no

A Trace witness needs a value whose origin the taint analysis actually established. The diagnostic found that 100% of the "assumed" (un-witnessed) steps carried a single named gap: TaintAnalysis::matched_source seeds taint only at resolved Invoke targets, so a build-time constant can never be the origin of a traced value. The obvious rescue is "then let taint be seeded at a constant", which, if it worked, makes the chained route evaluable and D reachable for the first time. That became its own adjudication, handed to a blind author who did not know it was the convenient answer. The verdict was NO, on semantic grounds: not "not yet," not "yes behind a flag."

analysis::taint is a forward may-analysis over MapLattice<TaintKey, Powerset<TaintLabel>> with union join. The lattice bottom is the empty set:

impl<T: Ord + Clone> Lattice for Powerset<T> {
    fn bottom() -> Self { Powerset::new() }   // the empty set ∅
    fn join(&mut self, other: &Self) -> bool {
        if other.0.is_empty() { return false; }  // ∅ is join-identity
        /* ... union ... */
    }
}

And here is the load-bearing part. The transfer function does not merely fail to seed at a literal. It treats a literal as the canonical producer of bottom:

Instruction::Const { register, .. }
| Instruction::ConstString { register, .. } => {
    // A literal overwrites whatever taint was previously in this register.
    state.insert(TaintKey::Reg(*register), Powerset::new());
}

Const, ConstString, ConstWide, ConstClass, NewInstance and NewArray all write Powerset::new() (⊥) into their destination, and the module docs justify several of these as "precise, not approximate." The ConstWide comment is the sharpest: clearing only the low half "would leave stale taint on register + 1 … a false positive, which is not the direction this module is allowed to be wrong in." So the lattice's bottom element identifies "untainted" with "holds a literal." That identification is not an accident of implementation; it is the definition the whole kill discipline is built on. Constant-seeding asks the model to split a distinction its own bottom exists to merge.

The semantic argument underneath is about what the label denotes. TaintLabel is "which untrusted-input category tainted a value," and each variant names an adversary, not a provenance, straight from the enum's own doc comments:

pub enum TaintLabel {
    IntentExtra,   // data another app/component can control
    IpcInput,      // the Binder peer, a raw Parcel
    UserInput,     // "the attacker here is the person holding the device"
}

A build-time constant has no such party. The party who chose it is the developer, the same party whose code is the object of the analysis, not an input to it. A Constant label would name the absence of a channel, not a fourth channel. And it would be neither a sound under-approximation nor an unsound over-approximation, because direction-of-error is only meaningful against a predicate whose extension is a proper subset of runtime states. "This value's derivation includes some literal" is true of nearly every non-source-derived value by construction: const-family instructions are 10–11.6% of all instructions across the vuln corpus, versus a few hundred catalogue source sites. Measured, that is a 90–130× increase in taint origins, and because scan_sinks gates only on if !labels.is_empty(), the finding ceiling becomes the sink-argument count: 920 / 643 / 487 against today's real output of 7 / 3 / 2. An abstraction of a near-universally-true predicate is near-exact and near-informationless. Asking its error direction presupposes a discrimination it does not make.

The disposal clause is the clean kill: at every program point where constant-seeded taint would report its label, crate::constants already holds a strictly stronger fact on the same CFG, Flat::Val(ConstValue), which names which literal. There is no point at which the taint fact is the best available answer. The adjudicator accepted it precisely because the author reached it without knowing it was the answer the program wanted:

Outcome D is unreachable, and that is an expressiveness limitation of the taint model, documented, not bent around. … taint here means an adversary chose this value and a constant has no adversary. The capability MI needs is therefore not a taint extension: it is a different analysis, answering a different question.

The self-correction: one of the two operators never ran

A negative result is only honest if you keep auditing it after you like the answer. The conclusion that supply was thin rested on two figures: Trace established 2 of 272, and Propagate fired 0 of 0. The second figure was void:

// RuleContext::build()
return_summaries: false,          // documented: "Defaults to false"

// extract_propagate_return()
if !ctx.return_summaries { return; }

MI built its context with RuleContext::build(ir), which sets the flag false, so the extractor returned immediately. Propagate had never executed: not once, on any app, in any measurement in the whole program. "Propagate 0/0" was never evidence about witness supply; it was a flag being off. Flipping it on (an existing opt-in whose consumer was written for it, a legitimate switch, not a bending of the experiment, unlike the constant-taint proposal) made Propagate fire: three established derivations where there were zero, with a 100%-dense summary table. The thinness came from dispatch ambiguity and Top-dominated summaries, an ordinary precision ceiling, a different kind of bound from the constant exclusion, which is about meaning. This is recorded as a correction beside the original, never an edit over it: the Trace half of the conclusion stands; the Propagate half was measured with one hand tied.

The flip side of a negative result is that it sharpens the standard. The analysis that did ship (the taint pass, the const-prop, the rules) earns its place by discriminating: firing on the flows that matter and staying quiet on the ones that don't. That is the bar this engine was built to clear and couldn't, and it is the same bar every shipped pass is held to.