Archway is the top deterministic type-inference tool on TypeEvalPy.

The lead isn't a tuned margin. Archway works differently from the tools it beats: we treat type inference as abstract interpretation, computing what each expression evaluates to and following those types through the program — across function calls, and into parameters that were never annotated.

The strongest existing checkers reason about types too, narrowing them along control flow; what they don't do is carry a value across a function's boundary, and that's where most of our lead lives.

We're building fast.

Two weeks ago, type inference didn't exist on this representation. Twelve days later it led every deterministic tool on the benchmark. Most of that climb didn't come from making the inference itself more complex — it came from the engine extending its coverage of Python's core operations: lambdas, decorators, comprehensions, classes. The inference came along for the ride.

Inference techniques of this kind have been understood for decades, but they've been hard to bring to Python because the structure they need isn't spelled out before the program runs. Our translation makes that structure available.

Each new analysis builds on the same translation work. The cost of adding the next one falls as the foundation deepens. That's the bet: not type inference, not any single benchmark, but the representation that makes the next analysis cheap.

A different kind of analysis.

The tools on this benchmark sit on a spectrum. At one end are the annotation-and-name-resolution checkers: they work out which object a name refers to (which class, function, or module) and read the type off it. That works until the type you need isn't written on any name. Given max([3, 1, 2]), such a tool resolves max to the built-in function and, with no rule for what it returns, reports the best name it has — sometimes max, sometimes NoneType. The strongest checkers go further. Meta's Pyrefly — the tool structurally closest to our analysis — genuinely infers unannotated locals and return types and narrows them along control flow, reasoning about types, not just names. But even Pyrefly's inference stops at the function signature: an unannotated parameter is Any, because nothing in local scope says what flows in.

Archway computes the type each expression evaluates to and follows it through the program. This is abstract interpretation: we model what each operation does to the types flowing through it, worked out for Python's semantics. We narrow types along control flow the way the strong checkers do. But we also carry types across call boundaries, so the reasoning doesn't stop at a function's edge. An unannotated parameter takes its type from the arguments that reach it. That puts a range of harder cases within reach: return types threaded through higher-order functions, generator and comprehension element types, instance attributes set in a constructor (the self.x family, which most tools handle poorly), and the types inside dicts and lists.

We also checked it against Python itself.

TypeEvalPy tells us our answers match its ground truth. We wanted a second check that doesn't depend on the benchmark at all, so we compared Archway's analysis against the reference implementation of Python.

We took eleven modules from CPython's standard library (fractions, statistics, csv, colorsys, posixpath, textwrap, random, bisect, datetime, decimal, collections), ran 1,675 operations through Archway, and compared each inferred type against the type CPython produces at runtime.

Where Archway commits to a concrete answer, it agrees with CPython 98.9% of the time: 1,236 exact matches, 14 disagreements. That's the analysis checked on real standard-library code, not only on the benchmark.

Where Archway isn't sure, it declines rather than guesses. Roughly a quarter of operations decline today, the coverage frontier we're working on.

Reproducibility.

TypeEvalPy published a leaderboard in January 2024, but we couldn't compare against those numbers directly. The ground truth has been corrected in several places since (for example, an MRO fix in PR #14), and a 2025 change to the scorer's matching semantics (commit 2f7c6056) now requires column-offset information that several of the original tool runners don't emit.

So we re-ran every deterministic baseline ourselves under the exact matcher. For each tool we could run, we repaired the runner to emit the column-offset information the exact scorer requires. Our fork of TypeEvalPy and our scoring code live inside our public benchmarks repo, and every benchmark number in this post is scored with that same exact matcher.

Two tools didn't reproduce cleanly on our setup and were left out: HiTyper and Type4Py.

What's next.

Two next steps. Scaling — from standard-library modules to the codebases engineers actually run. And the harder step: pairing this analysis with the agent layer that turns proofs into pull requests. That's where the deterministic foundation meets the workflow engineers already have, and it's where we're heading.

Thanks to the TypeEvalPy authors (Venkatesh, Bodden, and collaborators) for building a benchmark clean enough to measure ourselves against.

If you work on Python type inference, formal methods, or program analysis and want to talk about what's underneath, we'd love to hear from you.

If you lead engineering at a company shipping AI-generated Python at scale, we're starting design-partner conversations now.