Maxwell: A new kind of model that sits between code and hardware

What it claims

Maxwell is doubleAI's first "code execution model" (CEM), announced for early access with no availability date. It superoptimises Python programs while they run. It does this by replacing whole functions, algorithms included, with native code for the exact CPU or GPU present. Each replacement must carry a machine-checked proof that it is semantically equivalent to the code it replaces. doubleAI says this rests on its own complete formalisation of Python. The claimed scope is ordinary, general-purpose Python, including code that does file I/O and communication, not only small pure functions.

How it works

On CPU, Maxwell swaps Python code for bare-metal code, including direct SIMD implementations. On GPU, it replaces PyTorch code with kernels tuned for the specific GPU on the machine. It specialises code to the shapes, types and data it has actually observed, and guards against those assumed preconditions changing.

Maxwell is trained to write each new piece of code together with its equivalence proof. Proofs are assembled mostly from reusable "proof gadgets", each proved once, and they compose from small units into whole-unit proofs. Each proved faster version becomes the starting point for the next attempt, so optimisation continues for as long as the program runs. Source code is never modified.

doubleAI positions Maxwell against three kinds of existing tool:

• JITs and compilers (torch.compile, PyPy) are limited to transformations their engineers wrote in advance.
• Superoptimisers such as STOKE handle only short, loop-free machine-code fragments, optimised once and statically.
• Maxwell rewrites entire functions at runtime and re-optimises them as the hardware or data changes.

Limits

The post gives no speedups, no benchmarks, and no overhead figures. It says Maxwell runs without slowing the "hot path" but defers the runtime engineering "for another day".

Several things an adopter would need are not stated: supported Python versions, which libraries beyond PyTorch are covered, which proof checker or formal system is used, and whether the Python formalisation is published. The post also gives no install method, pricing, licence, or deployment model.

The authors acknowledge that Rice's theorem rules out a general procedure for deciding equivalence. They argue that equivalence is provable in practice for "nearly any" pair of programs that matter. That leaves open what happens to code where no proof is found. "Python" is the only source language the post names.