Add Kani verifier backend

README.md

@@ -18,6 +18,7 @@ The following backends are supported:
 - CBMC
 - Clang
 - PyTest
+- Kani
 
 ## Frontend
 
@@ -124,7 +125,8 @@ if not result.successful:
 
 ## Cite
 
-If you use formal-lib in your work, please cite it using the following BibTeX entry:
+If you use formal-lib in your work, please cite it using the following BibTeX
+entry:
 
 ```bib
 @misc{charalambous2026formallib,

formal_lib/__about__.py

@@ -1,3 +1,3 @@
 # Author: Yiannis Charalambous
 
-__version__ = "1.0.1"
+__version__ = "1.1.0"

formal_lib/specs/__init__.py

@@ -17,10 +17,14 @@
 from .cbmc import cbmc_spec
 from .clang import clang_spec
 from .esbmc import esbmc_spec
+from .kani import kani_spec
 from .pytest import pytest_spec
 
 SPECS: dict[str, IssueRegexSpec] = {
     "esbmc": esbmc_spec,
+    # kani must precede cbmc: Kani's `--output-format old` output also carries a
+    # `CBMC version` banner, so cbmc_spec.detect would otherwise claim it first.
+    "kani": kani_spec,
     "cbmc": cbmc_spec,
     "clang": clang_spec,
     "pytest": pytest_spec,
@@ -50,6 +54,7 @@ def detect_spec(output: str) -> IssueRegexSpec:
     "detect_spec",
     "esbmc_spec",
     "format_match",
+    "kani_spec",
     "missing_hint",
     "pytest_spec",
 ]

formal_lib/specs/cbmc.py

@@ -34,22 +34,26 @@
         # ensures no subsequent VP exists (CBMC accumulates VPs from previous traces).
         # _parse_traces uses re.MULTILINE only for stack traces (no DOTALL), so [\s\S]*
         # is used in the lookahead to span newlines.
-        block=r"Violated property:\n\s+file\s+\S+\s+function\s+\S+\s+line\s+\d+[^\n]*(?![\s\S]*Violated property:)",
+        block=r"Violated property:\n\s+file\s+\S+\s+function\s+.+?\s+line\s+\d+[^\n]*(?![\s\S]*Violated property:)",
         # Anchored to line start to avoid matching State header lines.
-        trace_entry=r"^\s+file\s+\S+\s+function\s+\S+\s+line\s+\d+[^\n]*",
+        trace_entry=r"^\s+file\s+\S+\s+function\s+.+?\s+line\s+\d+[^\n]*",
         trace_index=r"^",
         path=r"file\s+(\S+)",
-        name=r"function\s+(\S+)",
+        # Non-greedy up to " line " so names containing spaces are captured whole
+        # (CBMC C++ demangled templates; Rust generics like `foo::<'_, i32>` via Kani).
+        name=r"function\s+(.+?)\s+line",
         line_index=r"line\s+(\d+)",
     ),
     counterexample_spec=CounterexampleRegexSpec(
         # States between trace header and first "Violated property:".
         block=r"(?:Trace for [^\n]+|Counterexample):\n(.*?)(?=Violated property:|\Z)",
         # Each state entry: header + separator + assignment.
-        trace_entry=r"State\s+\d+\s+file\s+\S+\s+function\s+\S+\s+line\s+\d+[^\n]*thread\s+\d+\n[-]+\n.*?(?=\nState\s|\nViolated|\n\n|\Z)",
+        trace_entry=r"State\s+\d+\s+file\s+\S+\s+function\s+.+?\s+line\s+\d+[^\n]*thread\s+\d+\n[-]+\n.*?(?=\nState\s|\nViolated|\n\n|\Z)",
         trace_index=r"State\s+(\d+)",
         path=r"file\s+(\S+)",
-        name=r"function\s+(\S+)",
+        # Non-greedy up to " line " so names containing spaces are captured whole
+        # (CBMC C++ demangled templates; Rust generics like `foo::<'_, i32>` via Kani).
+        name=r"function\s+(.+?)\s+line",
         line_index=r"line\s+(\d+)",
         # Require at least one char so states with no assignment return None.
         assignment=r"\n[-]+\n(.+)",

formal_lib/specs/kani.py

@@ -0,0 +1,76 @@
+# Author: Yiannis Charalambous
+
+import re
+from dataclasses import replace
+
+from formal_lib.specs.base import format_match, missing_hint
+from formal_lib.specs.cbmc import cbmc_spec
+
+
+def _kani_message(value: str) -> str:
+    """CBMC's message formatting, then drop Kani's internal check-id marker.
+
+    Kani lowers every check into a CBMC assertion whose description is prefixed
+    with a ``[KANI_CHECK_ID_<crate>.<hash>::<name>]`` marker (e.g.
+    ``[KANI_CHECK_ID_overflow...] attempt to add with overflow``). Reuse CBMC's
+    "description. The Violated Property is: <condition>" formatting, then strip
+    the marker so the message reads like the rest of the library's output.
+    """
+    value = re.sub(r"\s*\n\s*", ". The Violated Property is: ", value)
+    return re.sub(r"\[KANI_CHECK_ID_[^\]]*\]\s*", "", value)
+
+
+# Kani drives CBMC under the hood, so `kani --output-format old --cbmc-args --trace`
+# emits CBMC's own output: the `Trace for <id>:` blocks, `State ... / assignment`
+# counterexample states, and `Violated property:` sections are byte-for-byte the CBMC
+# format. kani_spec is therefore cbmc_spec with only the handful of Kani-specific
+# differences overridden — the stack-trace, counterexample, and severity parsing are
+# reused verbatim. This keeps a single source of truth: fixing the CBMC trace parser
+# fixes it for Kani too. (Kani must be registered before cbmc in SPECS, because Kani's
+# output also contains a `CBMC version` banner that cbmc_spec.detect would match.)
+kani_spec = replace(
+    cbmc_spec,
+    # Kani prints its own banner above CBMC's; detect on that.
+    detect=r"^Kani Rust Verifier",
+    # Derive the verdict from the per-check statuses in CBMC's `** Results:` section,
+    # NOT the top-line `VERIFICATION` verdict. In old format Kani does not post-process
+    # its assertion-reachability probes, so a *passing* run still prints `VERIFICATION
+    # FAILED`: each `reachability_check` property "fails" precisely because the assertion
+    # is reachable (normal). Keying off the real per-check statuses lets Kani keep
+    # reachability checks enabled — they catch unreachable, vacuously-passing assertions,
+    # so disabling them would weaken verification — while still reporting correctly.
+    #
+    # negate_success: a match means FAILURE. A real failure is either a `** Results:`
+    # line for a non-`reachability_check` check with status FAILURE, or the native-format
+    # `VERIFICATION:- FAILED` line (native format has no such Results lines and is already
+    # correctly post-processed by Kani, so its verdict line is trustworthy).
+    success=(
+        r"^\[[^\]]*\.(?!reachability_check\.)[A-Za-z][\w-]*\.\d+\][^\n]*: FAILURE$"
+        r"|^VERIFICATION:- FAILED$"
+    ),
+    negate_success=True,
+    # Same trace-block boundaries as CBMC, with two Kani adjustments:
+    #  * skip the `reachability_check` properties Kani injects (its native format
+    #    hides them; they are not real bugs), and
+    #  * annotate the block so that when no trace is present — i.e. Kani was run in
+    #    its native format, or in old format without `--trace` — the parser surfaces
+    #    a hint telling the user which flags expose the counterexample, mirroring
+    #    CBMC's `--trace` hint.
+    block=missing_hint("Needs --output-format old --cbmc-args --trace")(
+        r"(?:Trace for (?!\S+\.reachability_check\.)[^\n]+|Counterexample):\n"
+        r".*?(?=Trace for [^\n]+:\n|Counterexample:\n|\*\* \d+ of \d+|\Z)"
+    ),
+    # Kani lowers every check to an assertion, so CBMC's first-word-of-description
+    # heuristic is unhelpful. The useful category is the property class at the end of
+    # the trace header, e.g. `Trace for check_overflow.assertion.1:` -> "assertion".
+    # Use a greedy `.+` (not `\S+`) so it spans function names that contain spaces and
+    # angle brackets, e.g. `Trace for kani::...::offset::<i32, *const i32,
+    # isize>.safety_check.1:` -> "safety_check". The class charset allows uppercase and
+    # hyphens for CBMC-style classes such as `NaN` and `division-by-zero`.
+    error_type=r"Trace for .+\.([A-Za-z][\w-]*)\.\d+:",
+    # Reuse CBMC's "last Violated property" capture (Kani emits a second, readable
+    # Violated property block per assertion), then strip the KANI_CHECK_ID marker.
+    message=format_match(_kani_message)(
+        r"(?s).*Violated property:\n\s+[^\n]+\n\s+(.+?(?:\n\s+.+?)?)$"
+    ),
+)

tests/regressions/samples/kani/arith_overflow.json

@@ -0,0 +1,21 @@
+{
+  "successful": false,
+  "issues": [
+    {
+      "error_type": "assertion",
+      "message": "attempt to subtract with overflow. The Violated Property is: !(var_12.1 != FALSE)",
+      "stack_trace": [
+        {
+          "trace_index": 0,
+          "path": "/home/user/kani/arith_checks.rs",
+          "name": "check_arith_overflow",
+          "line_idx": 10
+        }
+      ],
+      "severity": "error",
+      "error_location": null,
+      "counterexample": []
+    }
+  ],
+  "duration": 0.0
+}

tests/regressions/samples/kani/arith_overflow.log

@@ -0,0 +1,122 @@
+Kani Rust Verifier 0.67.0 (standalone)
+Checking harness check_arith_overflow...
+CBMC version 6.8.0 (cbmc-6.8.0) 64-bit x86_64 linux
+Reading GOTO program from file /home/user/kani/arith_checks__RNvCs1FqvJdxeI4h_12arith_checks20check_arith_overflow.out
+Generating GOTO Program
+Adding CPROVER library (x86_64)
+Removal of function pointers and virtual functions
+Generic Property Instrumentation
+Running with 16 object bits, 48 offset bits (user-specified)
+Starting Bounded Model Checking
+aborting path on assume(false) at file /home/user/kani/arith_checks.rs line 12 column 5 function check_arith_overflow thread 0
+Runtime Symex: 0.00154846s
+size of program expression: 71 steps
+slicing removed 50 assignments
+Generated 7 VCC(s), 5 remaining after simplification
+Runtime Postprocess Equation: 1.1833e-05s
+Passing problem to propositional reduction
+converting SSA
+Runtime Convert SSA: 6.7219e-05s
+Running propositional reduction
+Post-processing
+Runtime Post-process: 2.554e-06s
+Solving with CaDiCaL 2.0.0
+1 variables, 0 clauses
+SAT checker: instance is SATISFIABLE
+Runtime Solver: 2.3837e-05s
+Runtime decision procedure: 0.000108499s
+Building error trace
+Running propositional reduction
+Solving with CaDiCaL 2.0.0
+2 variables, 1 clauses
+SAT checker: instance is UNSATISFIABLE
+Runtime Solver: 5.463e-06s
+Runtime decision procedure: 9.97e-06s
+
+** Results:
+/home/user/kani/arith_checks.rs function check_arith_overflow
+[check_arith_overflow.assertion.1] line 9 [KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_0] index out of bounds: the length is less than or equal to the given index: SUCCESS
+[check_arith_overflow.reachability_check.1] line 9 KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_0: FAILURE
+[check_arith_overflow.assertion.2] line 10 [KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_1] index out of bounds: the length is less than or equal to the given index: SUCCESS
+[check_arith_overflow.reachability_check.2] line 10 KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_1: FAILURE
+[check_arith_overflow.assertion.3] line 11 [KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_2] attempt to subtract with overflow: FAILURE
+[check_arith_overflow.reachability_check.3] line 11 KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_2: FAILURE
+[check_arith_overflow.assertion.4] line 12 internal error: entered unreachable code: Previous statement should fail: SUCCESS
+
+Trace for check_arith_overflow.reachability_check.1:
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 9 thread 0
+  KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_0
+  FALSE
+
+
+
+Trace for check_arith_overflow.reachability_check.2:
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 9 thread 0
+  KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_0
+  FALSE
+
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 10 thread 0
+  KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_1
+  FALSE
+
+
+
+Trace for check_arith_overflow.assertion.3:
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 9 thread 0
+  KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_0
+  FALSE
+
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 10 thread 0
+  KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_1
+  FALSE
+
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 11 thread 0
+  KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_2
+  FALSE
+
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 11 thread 0
+  [KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_2] attempt to subtract with overflow
+  !(var_12.1 != FALSE)
+
+
+
+Trace for check_arith_overflow.reachability_check.3:
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 9 thread 0
+  KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_0
+  FALSE
+
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 10 thread 0
+  KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_1
+  FALSE
+
+
+Violated property:
+  file /home/user/kani/arith_checks.rs function check_arith_overflow line 11 thread 0
+  KANI_CHECK_ID_arith_checks.136e2f422fc5237b::arith_checks_2
+  FALSE
+
+
+
+** 4 of 7 failed (2 iterations)
+VERIFICATION FAILED
+Manual Harness Summary:
+Verification failed for - check_arith_overflow
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/regressions/samples/kani/array_success.json

@@ -0,0 +1,5 @@
+{
+  "successful": true,
+  "issues": [],
+  "duration": 0.0
+}