All pull requests

Pull requests

• Stop a SIMD comparison with float mask lanes from aborting the crate

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4951·feliperodri opened Oct 2, 2026Member·

  ·
  1

  5

  

• Handle let-chain conditions in #[kani::loop_invariant]

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4948·kasimte opened Oct 2, 2026Contributor·

  ·
  1

  2

  

• Keep loop attributes on rewritten for loops and add loop-only locals to loop_modifies

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4947·Talha-Dmr opened Oct 2, 2026Contributor·

  ·
  2

  7

  

• Check #[kani::loop_decreases] clauses whose measure is a variable

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4946·Talha-Dmr opened Oct 2, 2026Contributor·

  ·
  1

  1

  

• Fix compiletest help commands panicking after printing usage

  #4945·wodex1nhaoIeng opened Oct 2, 2026Contributor·

  ·
  1

  2

  

• Fix missing thread prefixes in parallel verification output

  #4944·wodex1nhaoIeng opened Oct 2, 2026Contributor·

  ·
  1

  1

  

• Migrate --export-json to the RFC 0015 document shape

  Z-EndToEndBenchCI
  #4941·ivmat opened Oct 1, 2026Contributor·

  ·
  7

  

• Augment explicit loop_modifies with loop-body-local temporaries

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4938·kasimte opened Oct 1, 2026Contributor·

  ·
  1

  14

  

• Only rewrite the jumps that leave a prev loop's body

  [F] SoundnessZ-CompilerBenchCIZ-ContractsZ-EndToEndBenchCI
  #4937·tautschnig opened Oct 1, 2026Member·

  ·

  · Contracts
  3

  

• Fix coverage region parsing for filenames with spaces

  #4936·wodex1nhaoIeng opened Oct 1, 2026Contributor·

  ·
  1

  4

  

• Support simd_reduce_max and simd_reduce_min on integer lanes

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4934·srivatsansamraj opened Sep 30, 2026Contributor·

  ·
  8

  

• Keep loop attributes and labels when rewriting while let and for loops with a loop invariant

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4930·Talha-Dmr opened Sep 30, 2026Contributor·

  ·
  12

  

• Add an unstable --target option and a riscv64 machine model

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4913·calef opened Sep 30, 2026·

  ·
  6

• Let alloc define the Kani models for its own types

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4871·feliperodri opened Sep 25, 2026Member·

  ·
  1

  

• Add 'kani verify-artifacts' subcommand

  [C] Feature / EnhancementZ-UnstableFeature
  #4600·lovesegfault opened May 20, 2026Contributor·

  ·
  10

  

• Add panics_if precondition to express panic-freedom

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4230·tautschnig opened Jul 16, 2025Member·

  ·
  1

  

• Re-enable debug_assert in our standard library build

  #4207·tautschnig opened Jul 5, 2025Member·

  ·
  1

  

• Document demonic non-determinism

  #3895·tautschnig opened Feb 18, 2025Member·

  ·
  13

  

• RFC: Attribute to distinguish safety preconditions from panic freedom

  T-RFC
  #3893·tautschnig opened Feb 17, 2025Member·

  ·
  37

  

• Reduce CBMC verbosity to CBMC's default

  #3398·tautschnig opened Jul 31, 2024Member·

  ·
  2

  

• Override std::ptr::align_offset

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #2396·tautschnig opened Apr 20, 2023Member·

  ·
  12

  

• Avoid global path conditions in Kani's library

  Z-EndToEndBenchCI
  #2394·tautschnig opened Apr 20, 2023Member·3 tasks done·

  ·
  10