Explore
naja-scope
MCP server: drivers, loads, logic cones and source lines, for any MCP client.
17 design questions on CVA6 (RISC-V core)
Input tokens: 182k vs 888k, about 5x fewer
Open EDA tools, built for AI agents and engineers
We don't build the brain. We build the tools any brain connects to.
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.
pip install najaeda
Why now
Agentic AI brings new power and new responsibilities to EDA tools
New power
- Navigate designs far larger than any context window
- Propose and apply design edits autonomously
- Iterate much faster than a manual loop
New responsibilities
- Every agent edit must be proven correct
- Tools must return exact, structured, bounded answers
- Results must stay reviewable by an engineer
What KeplerTech builds
A new kind of open EDA tools, designed to be driven by AI agents and engineers
Open source
- Public on GitHub and PyPI
- Transparent code: nothing hidden
- Auditable by your own team
Agent-ready
- High performance: the agent loop never stalls
- Multi-threaded; multi-machine extension possible
- Built on our EDA veteran culture
No AI inside
- We don't build the brain: we build the tools any brain connects to
- Fully deterministic: same question, same answer, every time
The agent loop
Explore, edit, verify, show
Our tools give any agent a precise view, a strict checker and a way to show its work.
Your agent
Any AI agent
Any model, any MCP client. It decides; the tools answer.
-
1 · Explore
naja-scope
Exact, token-bounded answers on RTL and netlists.
-
2 · Edit
najaeda
The agent applies its RTL or netlist edits through the Python API.
-
3 · Verify
kepler-formal
The policeman: proves each RTL or netlist edit keeps the same behavior.
-
4 · Show
naja-schematic
Renders the design and formal diagnoses.
↻ Loop until equivalence is proven
RTL→Synthesis→Netlist→P&R
The agent edits RTL or netlists (refactor, optimize, fix); each change is proven before it is kept.
Lego pieces on one common API
Each tool works on its own, for engineers as well as for agents
Verify
kepler-formal
Formal proof that two design versions behave identically.
RTL SEC checks the sequential behavior of SystemVerilog before vs after a change. Also gate-level LEC and SEC.
Used by OpenROAD for flow regression, and in hardware CI/CD flows.
Show
naja-schematic
Schematic viewer for netlists and formal diagnoses. Makes results reviewable by humans.
Opens in the browser and in VS Code.
Build
Your own tool
Scripts on the same API: analyze and transform your designs, automate your flow.
pip install najaeda
The common API: naja + najaeda
naja is our open-source C++ netlist engine; najaeda is its Python package. Every tool above is built on them.
najaeda: downloaded tens of times every day, worldwide
Demos
The tools at work
Two short recordings from real sessions: an AI agent exploring a design with naja-scope, and a schematic traced step by step in naja-schematic. Click a recording to open it full size.
Focus: formal verification
kepler-formal: proof that an edit keeps the same behavior
kepler-formal is an equivalence checking tool for digital designs. It takes two versions of a design, before and after a change, and returns a proof or a counterexample.
RTL SECSequential equivalence checking between two RTL versions: Verilog or SystemVerilog, including file lists with explicit tops. Checks that the sequential behavior is the same before and after a change.
RTL to gate SECSystemVerilog RTL against a Verilog gate-level netlist, with Liberty libraries.
Gate-level SECSequential gate-level netlists, with Liberty libraries.
Gate-level LECCombinational logic equivalence checking on post-synthesis or implementation netlists, with Liberty libraries.
One command
kepler-formal -sv -v sec \ --sv_design1_flist before.f --sv_design1_top top \ --sv_design2_flist after.f --sv_design2_top top
RTL SEC on two SystemVerilog file lists. The same run can be described in a YAML file.
One verdict
0Proved. All checked outputs were proved equivalent.1Partially proved. Some outputs were proved; the others are inconclusive.2Inconclusive. Neither a proof nor a counterexample.3Counterexample found. A definitive mismatch.
SEC exit codes: a script or an agent reads the result without parsing a log.
For agents
kepler-formal-mcp is a local MCP server with three tools: gate_lec, gate_sec and rtl_sec. Each call runs one check and returns a structured result.
The checker only reads design files. It never edits them.
For engineers and CI
Command line or YAML configuration. Liberty libraries, and custom technology primitives written in Python.
The prepared SEC problem can be exported as BTOR2.
In use
Used by OpenROAD for flow regression, and in hardware companies' CI/CD flows.
Apache-2.0 licensed. Supported and funded by NLnet through the NGI0 Entrust fund.
Ecosystem
From design formats to tools
Formats
- SystemVerilog
- VHDL
- Gate-level Verilog
- Liberty
- Python libraries
- naja-ifInterchange
Frontends
- slangSystemVerilog · third-party
- naja-vhdlVHDL · beta
- naja-verilogGate-level Verilog parser
Core
naja
Open-source C++ netlist engine
- RTL and gate-level designs
- Hierarchy and bit-level connectivity
- Primitive functional models
- Optimization and editing
API
- najaedaPython API
Tools
- kepler-formalFormal verification
- kepler-formal-mcpMCP server
- naja-schematicSchematic viewer
- naja-scopenajaeda MCP server
All open source · dashed outline: third-party component
Business model
Free open-source tools, paid services and specialization
Integration
Our tools plugged into your flows and CI.
Specialization
Custom tools and agent workflows on the naja APIs.
Support
Maintenance, priority fixes and training.
Build your own independent, autonomous EDA with us.
The team
Two technical co-founders, EDA veterans
Leadership at major EDA vendorsChief software architect and R&D managers. Years spent designing commercial EDA software, leading engineering teams and shipping tools used on production designs.
Core expertiseIndustrial-grade open source: the engineering standards of commercial EDA, applied to public code. Experts at solving complex problems on large designs, from netlist engines and compilers to formal verification, with performance and multi-threading as first concerns.