Skip to content

Pull requests: model-checking/kani

New pull request New
17 Open 2,375 Closed
17 Open 2,375 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

Introduce thread pool for writing goto binaries in parallel Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4236 opened Jul 24, 2025 by AlexanderPortland • Draft
2
Autoharness: add support for references Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI
#4234 opened Jul 24, 2025 by tautschnig • Draft
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
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
60
[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…
@carolynzech @zhassan-aws @thanhnguyen-aws
67
[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! Mix and match filters to narrow down what you’re looking for.