KAIROS PROVE — Formally verify a spec or natural-language hypothesis

USAGE:
  kairos prove <spec.sv>
  kairos prove --nl "<hypothesis>" --target-file <file>

WHAT IT DOES:
  Runs formal verification against a SystemVerilog spec using EBMC
  bounded model checking or k-induction. Also supports natural-language
  mode: describe a property in English and kairos compiles it into a
  formal spec, then verifies it.

EXAMPLES:
  kairos prove my_design.sv
  kairos prove my_design.sv --bound 20 --with-cegar
  kairos prove --nl "cwnd never drops below MSS" --target-file reno.sv

COMMON OPTIONS:
  --top MODULE            Top module name (auto-detected if omitted)
  --bound K               BMC bound depth (default 10)
  --with-cegar            Use the CEGAR LLM loop instead of pure EBMC
  --nl "HYPOTHESIS"       Natural-language hypothesis to verify
  --target-file FILE      Source file for --nl mode
  --vertical {ebmc,lean}  Proof backend (default: ebmc)
  -v, --verbose           Show per-property verdict table

SEE ALSO:
  kairos sv-prove  Pure EBMC verification (no LLM)
  kairos doctor    Check your setup
  kairos helper    List all topics
