-
Notifications
You must be signed in to change notification settings - Fork 157
OpenJul 21, 2026
No due date
•Last updated Tracking soundness issues for Kani.
41% complete
List view
0 of 17 selected 0 issues of 17 selected
Feature request: check for possible UB due to non-determinstic layouts
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[F] SoundnessKani failed to detect an issueKani failed to detect an issueStatus: Open.#297 In model-checking/kani;Feature request: detect when Rustc hides UB (undefined behavior) when generating MIR
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[F] SoundnessKani failed to detect an issueKani failed to detect an issueStatus: Open.#298 In model-checking/kani;Audit Vtable generation for dynamic traits
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.[F] SoundnessKani failed to detect an issueKani failed to detect an issueStatus: Open.#299 In model-checking/kani;Correctness of CBMC Serialization
[F] SoundnessKani failed to detect an issueKani failed to detect an issueT-CBMCIssue related to an existing CBMC issueIssue related to an existing CBMC issueStatus: Open.#302 In model-checking/kani;Linking may not follow Rust rules
[F] SoundnessKani failed to detect an issueKani failed to detect an issueT-CBMCIssue related to an existing CBMC issueIssue related to an existing CBMC issueStatus: Open.#303 In model-checking/kani;Audit Correctness of CBMC backend
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.[F] SoundnessKani failed to detect an issueKani failed to detect an issueStatus: Open.#310 In model-checking/kani;Object aliasing violations are not detected
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[E] Unsupported UBUndefined behavior that Kani does not detectUndefined behavior that Kani does not detect[F] SoundnessKani failed to detect an issueKani failed to detect an issueStatus: Open.#314 In model-checking/kani;Global ASM is not supported
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[E] Unsupported ConstructAdd support to an unsupported constructAdd support to an unsupported construct[F] SoundnessKani failed to detect an issueKani failed to detect an issueStatus: Open.#316 In model-checking/kani;Kani compilation fails when running cargo kani in a proc macro crate with
crate-typespecified.[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.Status: Open.Spurious failure on Prost check_duration_roundtrip
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.T-UserTag user issues / requestsTag user issues / requestsZ-Kani CompilerIssues that require some changes to the compilerIssues that require some changes to the compilerStatus: Open.Kani doesn't handle system calls
[E] Unsupported ConstructAdd support to an unsupported constructAdd support to an unsupported construct[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.T-CBMCIssue related to an existing CBMC issueIssue related to an existing CBMC issueT-UserTag user issues / requestsTag user issues / requestsStatus: Open.Mutable static variables usage in contract verification trigger UB
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.Z-ContractsIssue related to code contractsIssue related to code contractsStatus: Open.Confusing coverage result: Uncovered end of block on
ifstatement[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.Z-UnstableFeatureIssues that only occur if a unstable feature is enabledIssues that only occur if a unstable feature is enabledStatus: Open.Confusing coverage result: Uncovered argument for
match[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.Z-UnstableFeatureIssues that only occur if a unstable feature is enabledIssues that only occur if a unstable feature is enabledStatus: Open.Some coverage results point to non-existing regions
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.Z-UnstableFeatureIssues that only occur if a unstable feature is enabledIssues that only occur if a unstable feature is enabledStatus: Open.Tracking Issue: Disabling CBMC's NaN checks
[F] Spurious FailureIssues that cause Kani verification to fail despite the code being correct.Issues that cause Kani verification to fail despite the code being correct.Status: Open.#3875 In model-checking/kani;Fix unsound f128 -> i128 lower bound in float-to-int range check
[F] SoundnessKani failed to detect an issueKani failed to detect an issueZ-CompilerBenchCITag a PR to run benchmark CITag a PR to run benchmark CIZ-EndToEndBenchCITag a PR to run benchmark CITag a PR to run benchmark CIStatus: Open (in progress).