Skip to content
@keplertech

keplertech

README.md

Open EDA tools. Agents drive, engineers decide.

KeplerTech builds open-source EDA tools designed to be driven by AI agents, and usable standalone by engineers. The tools contain no AI: the agent brings the reasoning, the tools bring exact, reproducible results.

  • Open source: public on GitHub and PyPI under Apache-2.0. Transparent code, auditable by your own team.
  • Agent-ready: exact, structured, bounded answers. High performance and multi-threaded, so the agent loop never stalls.
  • No AI inside: fully deterministic. Same question, same answer, every time.

The agent loop: explore, edit, verify, show

  1. Explore with naja-scope: exact, token-bounded answers on RTL and netlists.
  2. Edit with any AI agent (any model, any MCP client), which decides and edits through najaeda.
  3. Verify with kepler-formal: proves each RTL or netlist edit keeps the same behavior.
  4. Show with naja-schematic: renders the design and formal diagnoses, so an engineer can review every result.

Loop until equivalence is proven. The loop works on RTL and netlists, before place and route: the agent edits RTL or netlists (refactor, optimize, fix), and each change is proven before it is kept.

Ecosystem

Every tool is built on naja, our open-source C++ netlist engine, and najaeda, its Python package. Each tool works on its own, for engineers as well as for agents.

KeplerTech ecosystem: SystemVerilog, VHDL, gate-level Verilog, Liberty and Python inputs feed the naja netlist engine, which powers najaeda, naja-scope, kepler-formal, kepler-formal-mcp and naja-schematic

Tools

Tool What it does
naja-scope MCP server giving drivers, loads, logic cones and source lines to any MCP client. On CVA6 (RISC-V core): 17/17 correct answers vs 10/17 with grep, with about 5x fewer input tokens (182k vs 888k). Details in the naja-scope README.
kepler-formal Formal proof that two design versions behave identically, or a counterexample. RTL SEC, RTL-to-gate SEC, gate-level SEC and LEC, from SystemVerilog, gate-level Verilog and Liberty. Used by OpenROAD and in hardware CI/CD.
kepler-formal-mcp MCP server for kepler-formal with three tools (rtl_sec, gate_sec, gate_lec). It reads design files and never edits them.
kepler-formal-action GitHub Action running equivalence checks on RTL and gate-level design changes in CI.
naja-schematic Schematic viewer for netlists and formal diagnoses. Native, WebAssembly (browser) and VS Code builds.
naja + najaeda The common API. RTL and gate-level designs, hierarchy and bit-level connectivity, primitive functional models, optimization and editing.

Build your own tool

Write scripts on the same API to analyze and transform your designs and automate your flow:

pip install najaeda

Documentation: najaeda.readthedocs.io

Links

Pinned Loading

  1. naja naja Public

    Open-source EDA framework for RTL elaboration, netlist analysis, and transformation, with C++ and Python APIs

    Verilog 170 26

  2. kepler-formal kepler-formal Public

    Digital Design Equivalence Checking

    C++ 120 14

  3. naja-scope naja-scope Public

    MCP server for AI agents to explore SystemVerilog, Verilog and VHDL (beta) designs: trace connectivity, walk hierarchy, jump to source - without pasting RTL into context. Built on najaeda.

    Python 22 2

  4. naja-verilog naja-verilog Public

    A standalone structural (gate-level) verilog parser

    C++ 44 3

  5. naja-schematic naja-schematic Public

    Portable netlist schematic viewer for the naja data model

    Verilog 5

  6. naja-if naja-if Public

    C++ 4

Repositories

Showing 10 of 26 repositories
  • naja-schematic Public

    Portable netlist schematic viewer for the naja data model

    keplertech/naja-schematic's past year of commit activity
    Verilog 5 Apache-2.0 0 3 0 Updated Nov 12, 2026
  • naja Public

    Open-source EDA framework for RTL elaboration, netlist analysis, and transformation, with C++ and Python APIs

    keplertech/naja's past year of commit activity
    Verilog 170 Apache-2.0 26 1 1 Updated Nov 12, 2026
  • kepler-formal Public

    Digital Design Equivalence Checking

    keplertech/kepler-formal's past year of commit activity
    C++ 120 Apache-2.0 14 16 14 Updated Nov 11, 2026
  • py2hwsw Public Forked from IObundle/py2hwsw

    a Python framework for managing embedded HW/SW projects

    keplertech/py2hwsw's past year of commit activity
    Python 0 GPL-3.0 16 0 0 Updated Nov 10, 2026
  • naja-scope Public

    MCP server for AI agents to explore SystemVerilog, Verilog and VHDL (beta) designs: trace connectivity, walk hierarchy, jump to source - without pasting RTL into context. Built on najaeda.

    keplertech/naja-scope's past year of commit activity
    Python 22 Apache-2.0 2 2 1 Updated Nov 8, 2026
  • OpenROAD-flow-scripts-KF Public Forked from The-OpenROAD-Project/OpenROAD-flow-scripts

    OpenROAD's scripts implementing an RTL-to-GDS Flow. Documentation at https://openroad-flow-scripts.readthedocs.io/en/latest/

    keplertech/OpenROAD-flow-scripts-KF's past year of commit activity
    Verilog 0 562 0 0 Updated Nov 6, 2026
  • .github Public
    keplertech/.github's past year of commit activity
    Mermaid 0 Apache-2.0 0 0 0 Updated Oct 29, 2026
  • pavona Public Forked from pavona/pavona

    A library of modular, tapeout-proven, and secure-by-default open silicon blocks

    keplertech/pavona's past year of commit activity
    SystemVerilog 0 Apache-2.0 35 0 0 Updated Oct 28, 2026
  • microwatt Public Forked from antonblanchard/microwatt

    A tiny Open POWER ISA softcore written in VHDL 2008

    keplertech/microwatt's past year of commit activity
    Verilog 0 124 0 0 Updated Oct 25, 2026
  • ibex Public Forked from lowRISC/ibex

    Ibex is a small 32-bit RISC-V CPU core with high-level of verification (previously known as zero-riscy)

    keplertech/ibex's past year of commit activity
    SystemVerilog 0 Apache-2.0 840 0 0 Updated Oct 24, 2026
View all repositories

People

This organization has no public members. You must be a member to see who’s a part of this organization.