Every design RTLPreCheck has analyzed, with full metrics.
SmallBoomV3 from Chipyard
268 modules received automated formal analysis. Every proof ran on an open-source formal solver. The generated properties are standard SVA, portable to any commercial formal tool.
We injected a 3-line microarchitectural bug into BOOM's reorder buffer. When an exception and a branch mispredict arrive on the exact same cycle, a latch permanently blocks the commit pointer. The processor hangs. Simulation never triggers it.
Caught in 17 seconds with a concrete counterexample trace. The formal solver explores every reachable state — no random stimulus, no directed tests needed. This class of bug sits at the intersection of two independent recovery paths in the microarchitecture and is vanishingly rare in simulation across billions of cycles.
9,084 contract edges automatically discharged across 266 modules. Guarantees extracted from proven probes, matched to downstream assumptions via geometry-based port matching over RTL wiring topology. Transitive propagation through combinational paths. Zero manual pairs.