All issues

Search results

Autoharness: make --bounded-arguments bounds configurable and surface them in the output

Status: Open.

#4751 In model-checking/kani;

· feliperodri opened on Aug 23, 2026

Autoharness: model caller-controlled aliasing between reference/pointer arguments

Status: Open.

#4750 In model-checking/kani;

· feliperodri opened on Aug 22, 2026

Verified function contract stubs fail compilation on slice references

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Z-ContractsIssue related to code contractsIssue related to code contracts

Status: Open.

Bug

#4748 In model-checking/kani;

· Trantorian1 opened on Aug 20, 2026

·  

Contracts

CBMC 6.8.0 + CaDiCaL 2.0.0 via Kani 0.67.0: SIGSEGV under ulimit -v where a lower limit gives a clean Out of memory

Status: Open.

Bug

#4747 In model-checking/kani;

· HumanaChain opened on Aug 19, 2026

CBMC 6.8.0 via Kani 0.67.0: deterministic SIGFPE (exit 136) during symex unwinding of core u128::pow

Status: Open.

Bug

#4746 In model-checking/kani;

· HumanaChain opened on Aug 19, 2026

not sure if issue, more a question, is this expected or not: --quiet makes a failing verification run exit 0

Status: Open.

#4745 In model-checking/kani;

· ivmat opened on Aug 18, 2026

Toolchain upgrade to nightly-2026-03-03 failed

Status: Open.

#4737 In model-checking/kani;

· github-actions opened on Aug 15, 2026

tracking issue for algebraic_ float functions in kani

[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.

Status: Open.

Feature

#4736 In model-checking/kani;

· xd009642 opened on Aug 14, 2026

--export-json: a failed, empty, or partial run can serialize as a clean pass

Status: Open.

#4731 In model-checking/kani;

· ivmat opened on Aug 12, 2026

--fail-fast discards results for harnesses that already completed

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Status: Open.

#4729 In model-checking/kani;

· feliperodri opened on Aug 12, 2026

Performance: symbolic array index plus carry chain does not close (34-limb fixed-point accumulator)

Status: Open.

#4720 In model-checking/kani;

· KyleClouthier opened on Aug 6, 2026

Field reads through Err(Box<T>) of a Result<f64, Box<T>> function report invalid-pointer/misalignment failures and garbage values (f32 same shape verifies)

[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.

Status: Open.

Bug

#4690 In model-checking/kani;

· malisper opened on Jul 29, 2026