All pull requests

Pull requests

• Fix atomic store reads and initialization tracking

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5115·v3risec opened Nov 3, 2026·

  ·
  1

• Fix -Z uninit-checks crash on cross-crate constructors used as functions

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5113·acearyanarun opened Nov 3, 2026Contributor·

  ·
  1

• Scope autoharness default bounds to automatic harnesses

  Z-EndToEndBenchCI
  #5112·acearyanarun opened Nov 3, 2026Contributor·

  ·
  1

  1

• RFC: Aliasing checks

  T-RFCZ-Aliasing-model
  #5111·feliperodri opened Nov 3, 2026Member·

  ·
  

• Add a Nix flake: Kani releases, version selection and a development shell reproducible

  #5098·lalvesl opened Oct 30, 2026·

  ·

• Disable MIR inlining when stubbing is enabled

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5095·r-near opened Oct 28, 2026·

  ·
  1

  1

• Avoid saturating method calls in contract clause depth helpers

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5093·r-near opened Oct 28, 2026·

  ·
  1

• Parse CBMC --show-properties output

  #5092·r-near opened Oct 28, 2026·

  ·
  1

• Do not reuse a static's storage for an equal-bytes constant

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5089·r-near opened Oct 28, 2026·

  ·
  1

  1

• Rebase mined getter invariants onto the receiver's field path

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5087·wodex1nhaoIeng opened Oct 28, 2026Contributor·

  ·
  1

• Check slice element reads under -Z valid-value-checks

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5073·kasimte opened Oct 27, 2026Contributor·

  ·
  1

  5

• Add a loop's dead temporaries and loop-body variables to an explicit loop_modifies

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5071·hung1962003 opened Oct 27, 2026·

  ·
  1

  

• Autoharness: report bounded Rc/Arc reference-count models

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5070·acearyanarun opened Oct 27, 2026Contributor·

  ·
  1

• Check aggregate-layout enum discriminants under -Z valid-value-checks

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5069·kasimte opened Oct 27, 2026Contributor·

  ·
  1

  1

• Keep the kani_loop_modifies binding alive through MIR optimization

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5068·kasimte opened Oct 26, 2026Contributor·

  ·
  1

• Fix ICE reading the discriminant of an enum whose niche starts above u64::MAX

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5066·frederickjjoubert opened Oct 26, 2026·

  ·
  1

• Autoharness: support MultiCharEq searcher arguments under --bounded-arguments

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5064·CYJ904 opened Oct 26, 2026Contributor·

  ·
  1

• Fix debug assertion in determine_targets for autoharness with --harness

  #5063·ivmat opened Oct 25, 2026Contributor·

  ·
  1

• Write the RFC 0015 INCOMPLETE marker before --export-json verification

  #5062·ivmat opened Oct 25, 2026Contributor·

  ·
  1

• Add the Kani agent plugin: verify-rust skill, helper scripts, and kani-mcp

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5059·feliperodri opened Oct 23, 2026Member·

  ·
  1

• Fix aliasing UB in the async executor and in a copy test

  Z-Aliasing-modelZ-CompilerBenchCIZ-EndToEndBenchCI
  #5058·feliperodri opened Oct 23, 2026Member·

  ·
  

• Fix value-validity checks for initialization stores and field projections

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5057·v3risec opened Oct 23, 2026·

  ·
  1

  2

• LLBC: translate MIR without rustc's optimizations, so Aeneas accepts generic code

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5045·feliperodri opened Oct 22, 2026Member·

  ·

  · Charon front end (LLBC)
  5

• Report simd_reduce_max/min with a result type other than the lane type as unsupported

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5044·srivatsansamraj opened Oct 22, 2026Contributor·

  ·
  1

• Pin Z3 in kani-dependencies and bump it automatically

  [I] CI / InfrastructureZ-EndToEndBenchCI
  #5039·feliperodri opened Oct 21, 2026Member·

  ·