Skip to content

Pull requests: model-checking/kani

New pull request New
16 Open 2,373 Closed
16 Open 2,373 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Ensuring that MIR constants are marked as static consts Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4233 opened Jul 23, 2025 by vonaka Loading…
2
Fix bug: Kani unwinds loops with contract in generic function (with -Z loop-contracts) Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4232 opened Jul 22, 2025 by thanhnguyen-aws Loading…
2
Add panics_if precondition to express panic-freedom Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4230 opened Jul 16, 2025 by tautschnig • Draft
@tautschnig
1
RFC: Partitioned proofs
#4228 opened Jul 15, 2025 by AlexanderPortland Loading…
@AlexanderPortland
39
[DRAFT] Use arena allocator when exporting goto binaries Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4210 opened Jul 7, 2025 by AlexanderPortland • Draft
Re-enable debug_assert in our standard library build
#4207 opened Jul 5, 2025 by tautschnig • Draft
1
@tautschnig
Make kani::assert non-fatal Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4206 opened Jul 5, 2025 by tautschnig • Draft
@tautschnig
Add loop-contracts support for for loop Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4143 opened Jun 6, 2025 by thanhnguyen-aws Loading…
@tautschnig @carolynzech @zhassan-aws
37
[DRAFT] Resolve stubs and contracts in trait implementations Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4130 opened Jun 4, 2025 by carolynzech • Draft
2
@carolynzech
Prefix property descriptions of panics with "Panic:" Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4045 opened Apr 25, 2025 by tautschnig • Draft
5
set kani default value to 1
#3912 opened Feb 27, 2025 by rajath-mk • Draft
@rajath-mk
Document demonic non-determinism
#3895 opened Feb 18, 2025 by tautschnig • Draft
@tautschnig
13
RFC: Attribute to distinguish safety preconditions from panic freedom
#3893 opened Feb 17, 2025 by tautschnig • Draft
@tautschnig
37
Reduce CBMC verbosity to CBMC's default
#3398 opened Jul 31, 2024 by tautschnig • Draft
@tautschnig
2
Override std::ptr::align_offset Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#2396 opened Apr 20, 2023 by tautschnig Loading…
1
@zhassan-aws
6
Avoid global path conditions in Kani's library Z-EndToEndBenchCI Tag a PR to run benchmark CI
#2394 opened Apr 20, 2023 by tautschnig • Draft
3 tasks done
@tautschnig
10
ProTip! Follow long discussions with comments:>50.