News · 2026-10-20

doubleAI introduces Maxwell to rewrite running programs, with proof claims still under scrutiny

doubleAI says its Maxwell system observes running software and replaces selected binary code with faster versions while leaving source files untouched. In one company-reported demonstration, a five-second 4K video pipeline fell from 250 seconds to 134 seconds. The central claim is that each replacement is formally proven equivalent, although the public product material does not fully document the proof framework or independently validate the timings.

Key facts

• Maxwell is made by doubleAI, whose founders include Amnon Shashua and Shai Shalev-Shwartz.
• The LTX-2.5 demonstration reports 250 seconds before optimization and 134 seconds afterward on two B200 processors.
• The product watches runtime behavior and swaps selected code in memory, according to the company.
• The primary source is Maxwell's product page, with a detailed LTX case study.

Maxwell's pitch moves the optimization target below the source code that a developer normally edits. A program's written instructions may be general, but the machine running them has a particular processor, memory arrangement and workload. Observing that combination can reveal work that can be moved, combined or expressed differently.

Think of a restaurant that keeps the same menu but changes its kitchen layout after watching where the cooks spend time. The promise is identical dishes with less wasted movement. In software, however, apparently harmless shortcuts can change edge cases, numerical behavior or interactions with other parts of the program. That makes the correctness claim at least as important as the speed claim.

doubleAI calls Maxwell a “Code Execution Model.” Its team page identifies the company behind the system. The product description says it uses traces, profiling information and data to adapt selected machine code to the observed workload and hardware. In the launch discussion, a representative clarified that the substitutions occur in memory rather than rewriting files on disk, and said optimizations are cached.

Formal equivalence is a stronger proposition than passing a collection of tests. In principle, a proof can establish that a replacement satisfies a specified relationship to the original across the conditions covered by the formal model. But the relationship, assumptions and scope must be inspectable. A proof of one local transformation does not automatically explain an entire production system's reproducibility or operational behavior. Readers can compare this distinction with our proof-assistant lesson.

The company says it externalizes equivalence proofs. The accessible product material does not fully explain the framework, and the launch thread includes requests for that detail. Those requests are consequential: developers need to know what the proof covers, how assumptions are checked and what evidence remains when diagnosing a failure. A runtime optimizer also raises practical questions about debugging a program whose actual machine-code implementation differs from the usual build artifact.

The LTX case study supplies a more concrete mechanism than a generic claim of smarter code. doubleAI describes moving processor work to the graphics processor, combining small launches and changing a two-device attention exchange. Instead of passing 262 megabytes of video keys and values, its account says the revised path transfers about one megabyte of partial attention results. These are targeted changes to data movement and execution overhead, not evidence that every mathematical operation became dramatically faster.

Another demonstration on the product page compares 180 Whisper-small transcriptions, with displayed runtime falling from 106.23 seconds to 49.82 seconds on an RTX 4090. The company says the transcripts were identical. No independent reproduction of either the Whisper or video timings was established in the dossier. These examples describe measured configurations, rather than minimum graphics-memory requirements for a newly downloadable model; Maxwell itself is the optimization product under discussion.

The company also publishes cuGraph optimization work and results on NVIDIA's SOL-ExecBench. Public code and an external benchmark create routes for scrutiny, but doubleAI conducted those evaluations. Their existence does not turn the reported speedups into independently audited results.

The strongest skeptical response is that developers still need complete observability and repeatability even if local replacements are correct. Caching, debugging support, control over optimization and a clear record of the code actually executed all affect deployability. The favorable case is that specialization can recover performance without demanding a source rewrite from every application team. Maxwell makes that case tangible; the next evidence should be reproducible workloads and a sufficiently detailed proof story for engineers to inspect its limits.

Primary source, verified: read the paper →

Ground Truth. (2026, October 20). doubleAI introduces Maxwell to rewrite running programs, with proof claims still under scrutiny. Ground Truth. https://groundtruth.day/news/maxwell-doubleai-runtime-binary-optimization.html

@misc{groundtruth:maxwell-doubleai-runtime-binary-optimization,
  title  = {doubleAI introduces Maxwell to rewrite running programs, with proof claims still under scrutiny},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {oct},
  url    = {https://groundtruth.day/news/maxwell-doubleai-runtime-binary-optimization.html}
}

Topics: doubleai · developer-tools · optimization · formal-verification · inference