doubleAI Introduces Maxwell: A Code Execution Model Using Formal Verification for Runtime Binary Optimization

• doubleAI announced Maxwell, a Code Execution Model (CEM) available in early access, which analyzes hardware and data flow during program execution to rewrite binaries in real time.
• The system uses formal verification to prove semantic equivalence between the original source and optimized binary, ensuring correctness without relying on testing.
• Benchmarks show a 1.86x speedup for LTX-2.5 4K video generation (reducing time from 249.4s to 133.9s on 2 B200 GPUs).
• Maxwell achieves formalization of dynamic Python features, allowing optimization of general-purpose Python code into low-level SIMD or GPU-specific kernels.

Technical Mechanism

• Operates between code and silicon, reconfiguring algorithms and instructions at the function level rather than just instruction level.
• Utilizes reusable 'proof gadgets' to construct proofs of equivalence for all possible inputs and scenarios.
• Includes a guard mechanism that returns control to the original code if runtime context assumptions change.

Performance Details

• On Blackwell architecture, Maxwell exceeded the NVIDIA PyTorch baseline in 90% of SOL-ExecBench kernels after one day of exploration.
• Independently generated and verified a hyper-optimized drop-in version of NVIDIA cuGraph, achieving an average 3.6x speedup.
• For LTX-2.5, GPU communication was reduced from 262 MB to 1 MB of partial outputs, and decoder kernel launch counts were halved while maintaining identical visual quality.