Soundness

Issues

• Feature request: check for possible UB due to non-determinstic layouts

  [C] Feature / Enhancement[F] Soundness
  model-checking/kani#297 · Filter by author danielsn opened on Jul 6, 2021 · Soundness
  1

• Feature request: detect when Rustc hides UB (undefined behavior) when generating MIR

  [C] Feature / Enhancement[F] Soundness
  model-checking/kani#298 · Filter by author danielsn opened on Jul 6, 2021 · Soundness
  1

• Audit Vtable generation for dynamic traits

  [C] Internal[F] Soundness
  model-checking/kani#299 · Filter by author danielsn opened on Jul 6, 2021 · Soundness
  5

• Correctness of CBMC Serialization

  [F] SoundnessT-CBMC
  model-checking/kani#302 · Filter by author danielsn opened on Jul 6, 2021 · Soundness

• Linking may not follow Rust rules

  [F] SoundnessT-CBMC
  model-checking/kani#303 · Filter by author danielsn opened on Jul 6, 2021 · Soundness
  2

• Audit Correctness of CBMC backend

  [C] Internal[F] Soundness
  model-checking/kani#310 · Filter by author danielsn opened on Jul 8, 2021 · Soundness

• Object aliasing violations are not detected

  [C] Feature / Enhancement[E] Unsupported UB[F] Soundness
  model-checking/kani#314 · Filter by author danielsn opened on Jul 8, 2021 · Soundness
  1

• Global ASM is not supported

  [C] Feature / Enhancement[E] Unsupported Construct[F] Soundness
  model-checking/kani#316 · Filter by author danielsn opened on Jul 8, 2021 · Soundness
  2

• Kani compilation fails when running cargo kani in a proc macro crate with crate-type specified.

  [C] Bug[F] Spurious Failure
  Bug

  model-checking/kani#2038 · Filter by author celinval opened on Dec 23, 2022 · Soundness
  1

• Kani doesn't handle system calls

  [E] Unsupported Construct[F] Spurious FailureT-CBMCT-User
  Bug

  model-checking/kani#2284 · Filter by author adpaco opened on Mar 8, 2023 · Soundness
  5

  

• Mutable static variables usage in contract verification trigger UB

  [C] Bug[F] Spurious FailureZ-Contracts
  Bug

  model-checking/kani#3298 · Filter by author celinval opened on Jun 27, 2024 · Soundness
  2

• Confusing coverage result: Uncovered end of block on if statement

  [C] Bug[E] User Experience[F] Spurious FailureZ-UnstableFeature
  Bug

  model-checking/kani#3455 · Filter by author adpaco opened on Aug 20, 2024 · Soundness

• Confusing coverage result: Uncovered argument for match

  [C] Bug[E] User Experience[F] Spurious FailureZ-UnstableFeature
  Bug

  model-checking/kani#3456 · Filter by author adpaco opened on Aug 20, 2024 · Soundness

• Some coverage results point to non-existing regions

  [C] Bug[E] User Experience[F] Spurious FailureZ-UnstableFeature
  Bug

  model-checking/kani#3543 · Filter by author adpaco opened on Sep 23, 2024 · Soundness
  2

  

• Tracking Issue: Disabling CBMC's NaN checks

  [F] Spurious Failure
  model-checking/kani#3875 · Filter by author rajath-mk opened on Feb 5, 2025 · Soundness