We have updated our open source formal verification tool, kepler-formal, to support full sequential equivalence checking at both RTL and gate level. What is our goal? An infinite license open source equivalence checking tool that can be used in scale for AI agents and CICD flows and can support industrial grade designs. Don't hesitate to reach out to us with issues you found and suggestions you have. We want to hear it! It will be a long journey to productize a project at this scale, and we acknowledge it, but we are up for the task.