k-induction

Here are 5 public repositories matching this topic...

esbmc / esbmc

The efficient SMT-based context-bounded model checker (ESBMC)

kotlin python c cpp smt-solver k-induction automated-testing incremental-learning bmc solidity-contracts cheri automated-verification cp-solver

Updated Oct 4, 2026
C++

SRI-CSL / sally

Star

SRI Sally: A model checker for infinite-state systems.

verification ic3 model-checker transition-systems k-induction bounded-model-checking

Updated Jul 31, 2025
C++

Saikoushik1423 / formal-verification-sva

Star

Formal proof of an arbiter, a FIFO and an AXI4-Lite slave with SymbiYosys: 25 assertions proved unbounded, 13/13 covers reached, and a broken arbiter that passes every safety property.

assertions verilog formal-verification k-induction yosys sva symbiyosys

Updated Aug 26, 2026
SystemVerilog

Rivoryxa-Technologies / formal-fsm-verification

Star

Formal verification reference flow: an FSM safety property proven unbounded by k-induction with SymbiYosys, Yosys, and z3. The same toolchain we use to prove coverage holes unreachable on real cores.

fsm hardware verification riscv rtl z3 model-checking systemverilog formal-verification k-induction yosys sva symbiyosys coverage-closure riscv-verification

Updated Oct 2, 2026
SystemVerilog

nickharris808 / equiv-receipt

Star

Portable, independently re-derivable logic-equivalence receipts — DRAT checking with zero dependencies

sat-solver formal-verification k-induction drat equivalence-checking

Updated Aug 18, 2026
Python

Add this topic to your repo

To associate your repository with the k-induction topic, visit your repo's landing page and select "manage topics."

Learn more