The RISC-V ecosystem is expanding rapidly, with many open hardware projects now developed collaboratively on platforms such as GitHub. Yet while software enjoys mature continuous integration and deployment (CI/CD) practices, hardware design lacks equivalent automated verification: formal tools such as logic equivalence checking (LEC) stay confined to proprietary EDA solutions whose per-run license costs make them impractical to run on every pull request. This gap is now acute, as AI-assisted agents that modify RTL are emerging without fast, open tools to verify their output, sharpening the need for automated formal verification inside the development loop.
We present kepler-formal, an open-source formal equivalence checking tool that runs efficiently in CI for RISC-V projects. Built on a high-performance C++ netlist engine with a Python interface, it checks equivalence between RTL transformations and synthesized netlists. It is evolving from combinational LEC toward Sequential Equivalence Checking (SEC): since RTL contains registers, pipelines, and state machines, SEC's cycle-by-cycle modeling is the sound method for proving equivalence at the RTL level.
On open RISC-V designs (CVA6, BlackParrot, MegaBoom, up to ~3.9M primitives), checks complete within typical pull request budgets, from under two to under ten minutes. Running license-free and fast enough for per-commit use, kepler-formal delivers both the inner-loop verification AI agents need and a practical first formal gate before commercial sign-off.