Issues

• Support Naja's VECTOR_SELECT semantic model for indexed slice reads

  keplertech/kepler-formal#294 · Filter by author xtofalex opened on Oct 25, 2026

• Support Naja's VECTOR_UPDATE semantic model in formal encoding

  keplertech/kepler-formal#293 · Filter by author xtofalex opened on Oct 25, 2026

• -vhdl: load all design files together (multi-file loading)

  keplertech/kepler-formal#291 · Filter by author xtofalex opened on Oct 24, 2026

• SEC aborts on read-only naja_mem (constant lookup tables): "Missing SEC variable for memory read-output state"

  keplertech/kepler-formal#286 · Filter by author xtofalex opened on Oct 17, 2026

• SEC --sec-encoding binary with reset bootstrap reports a counterexample on a design compared with itself (registers without reset are not skipped)

  keplertech/kepler-formal#285 · Filter by author xtofalex opened on Oct 17, 2026

• SEC: Quine-McCluskey prime-implicant reduction makes SAT solver timeout

  keplertech/kepler-formal#284 · Filter by author xinfred opened on Oct 17, 2026
  

• SEC: treat undriven nets as X by default (reference side) instead of skipping dependent outputs

  keplertech/kepler-formal#283 · Filter by author xtofalex opened on Oct 15, 2026

• SEC: a design is not proven equivalent to itself, non-monotonically in the number of unrelated outputs

  keplertech/kepler-formal#250 · Filter by author ovebryne opened on Sep 17, 2026
  8

• Feature request: treat a cell with no Liberty function as an uninterpreted function when it appears on both sides, instead of skipping the cone

  keplertech/kepler-formal#245 · Filter by author ovebryne opened on Sep 15, 2026
  1

• kepler-formal links naja's Python bindings, so the binary is not relocatable and cannot be built as a dependency without PIC everywhere

  keplertech/kepler-formal#244 · Filter by author ovebryne opened on Sep 15, 2026
  1

  

• SEC skips every output in a cone containing an x/z literal

  keplertech/kepler-formal#214 · Filter by author ovebryne opened on Aug 26, 2026
  13

  

• Comparing post-synth netlists fails sec

  keplertech/kepler-formal#204 · Filter by author jeffng-or opened on Aug 13, 2026
  3

• kepler-formal 9dd032c breaks liberty cell

  keplertech/kepler-formal#195 · Filter by author jeffng-or opened on Aug 10, 2026
  4

• Cannot verify a design with sec that lec says is equivalent

  keplertech/kepler-formal#192 · Filter by author jeffng-or opened on Aug 6, 2026
  1

• No option to specify verilog top module?

  keplertech/kepler-formal#174 · Filter by author jeffng-or opened on Jul 28, 2026
  7

  

• Feature request - Publish kepler-formal on bazel bcr

  keplertech/kepler-formal#165 · Filter by author oharboe opened on Jul 16, 2026
  1