-
Notifications
You must be signed in to change notification settings - Fork 176
OpenJul 23, 2026
No due date
•Last updated Tracking soundness issues for Kani.
44% complete
List view
0 of 13 selected 0 issues of 13 selected
Soundness documentation
[C] DocumentationAdditions and improvements to our documentationAdditions and improvements to our documentation[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: Closed (completed).#1495 In model-checking/kani;Fix floating-point remainder soundness and add soundness documentation
[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: Merged (completed).model-checking/kaninumber 4570#4570 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: Merged (completed).model-checking/kaninumber 4663#4663 In model-checking/kani;Compiler intrinsics
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Closed (completed).#312 In model-checking/kani;Add support verification of unbounded structures and loops
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.[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.Status: Closed (completed).#311 In model-checking/kani;RMC doesn't seem to handle stack unwind logic correctly
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Closed (completed).#545 In model-checking/kani;Soundness: Monomorphization
[F] SoundnessKani failed to detect an issueKani failed to detect an issueStatus: Closed (completed).#295 In model-checking/kani;Soundness: Type naming relies on pretty-printer
[F] SoundnessKani failed to detect an issueKani failed to detect an issueStatus: Closed (completed).#300 In model-checking/kani;Missing check for object correctness invariants
[E] Unsupported UBUndefined behavior that Kani does not detectUndefined behavior that Kani does not detectStatus: Closed (completed).#301 In model-checking/kani;Feature request: detect when object layouts may not faithfully follow Rustc layouts
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Closed (completed).#296 In model-checking/kani;Add support to concurrency
[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 constructStatus: Closed (completed).#313 In model-checking/kani;Representation of DSTs and fat pointers
[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.Status: Closed (completed).#315 In model-checking/kani;RMC should use rustc monomorphization as is
[F] SoundnessKani failed to detect an issueKani failed to detect an issueT-High PriorityTag issues that have high priorityTag issues that have high priorityStatus: Closed (completed).#485 In model-checking/kani;