Our team contributes models, datasets, and tools for mathematical reasoning and chip design to the open-source community.
These contributions cover research relevant to our verified and physical intelligence stacks.
01 · Mathematical reasoning
An open-source theorem-proving agent built around Lean 4.
Lea formalizes mathematical statements into Lean and supports the theorem-proving process while keeping mathematicians in control. Developed through DARPA’s expMath program, it explores how AI can produce proofs that can be checked.
02 · Hardware generation
Models and datasets for Verilog generation, with formal verification in the training process.
VeriThoughts uses formal equivalence checking to move generated RTL from plausible code toward verified behavior. The release includes reasoning datasets, specialized models, and code for data generation, training, and evaluation.
03 · Logic synthesis
Reinforcement learning for optimizing logic synthesis.
ABC-RL learns from prior circuits and searches for sequences of synthesis transformations that improve area and delay. It uses retrieval to adapt what it has learned to new designs.
04 · Analog design
Tools and datasets for translating analog circuit schematics into SPICE netlists.
Masala-CHAI combines multimodal models, component detection, and verification to turn circuit diagrams into machine-readable representations. Its datasets support research in analog-circuit generation.