All pull requests

Pull requests

• Disable cargo_autoharness_multichareq_searcher until #5162 is fixed

  [I] CI / InfrastructureZ-Autoharness
  #5163·feliperodri opened Nov 13, 2026Member·

  ·

• Build kissat for macOS 11.0 and check the bundle's minimum macOS

  [I] CI / Infrastructure
  #5161·feliperodri opened Nov 13, 2026Member·

  ·
  

• Avoid dereferencing volatile loads of zero-sized types

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #5159·Tiramisu-Cake opened Nov 12, 2026Contributor·

  ·
  1

• Upgrade Charon to nightly-2026.11.12

  [C] InternaldependenciesZ-CompilerBenchCIZ-EndToEndBenchCI
  #5158·feliperodri opened Nov 12, 2026Member·

  ·
  1

• Upgrade the Rust toolchain to nightly-2026-11-11

  [C] InternalZ-CompilerBenchCIZ-EndToEndBenchCI
  #5157·feliperodri opened Nov 12, 2026Member·

  ·
  1

  4

  

• Reuse the verify-std build when its inputs are unchanged

  [C] Feature / Enhancement[E] PerformanceT-High PriorityZ-CompilerBenchCIZ-EndToEndBenchCI
  #5133·srivatsansamraj opened Nov 6, 2026Contributor·

  ·
  1

  15

  

• Aliasing checks: Tree Borrows monitor and its Verus proof

  Z-Aliasing-modelZ-CompilerBenchCIZ-EndToEndBenchCI
  #5120·feliperodri opened Nov 5, 2026Member·

  ·
  3

  

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

  [C] Bug[F] CrashZ-CompilerBenchCIZ-EndToEndBenchCI
  #5113·acearyanarun opened Nov 3, 2026Contributor·

  ·
  4

  

• Scope autoharness default bounds to automatic harnesses

  [C] Bug[F] Spurious FailureT-High PriorityZ-AutoharnessZ-EndToEndBenchCI
  #5112·acearyanarun opened Nov 3, 2026Contributor·

  ·

  · Autoharness
  1

  3

  

• 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·

  ·
  1

• Disable MIR inlining when stubbing is enabled

  [F] SoundnessZ-CompilerBenchCIZ-ContractsZ-EndToEndBenchCI
  #5095·r-near opened Oct 28, 2026Contributor·

  ·
  1

  2

  

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

  [C] Bug[F] SoundnessZ-CompilerBenchCIZ-EndToEndBenchCI
  #5089·r-near opened Oct 28, 2026Contributor·

  ·
  1

  2

  

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

  [C] Bug[F] SoundnessZ-CompilerBenchCIZ-EndToEndBenchCI
  #5073·kasimte opened Oct 27, 2026Contributor·

  ·
  1

  9

  

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

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

  ·

  · Contracts
  28

  

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

  [C] Bug[F] SoundnessZ-AutoharnessZ-CompilerBenchCIZ-EndToEndBenchCI
  #5070·acearyanarun opened Oct 27, 2026Contributor·

  ·

  · Autoharness
  6

  

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

  [C] Bug[F] SoundnessZ-CompilerBenchCIZ-EndToEndBenchCI
  #5069·kasimte opened Oct 27, 2026Contributor·

  ·
  1

  3

  

• Keep the kani_loop_modifies binding alive through MIR optimization

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

  ·

  · Contracts
  1

  4

  

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

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

  ·
  1

  

• 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)
  7

  

• Respect explicit stubs when detecting contract-generation cycles

  [C] Bug[F] Spurious FailureZ-CompilerBenchCIZ-EndToEndBenchCI
  #5008·Kieran-Hulsman opened Oct 14, 2026·

  ·

  · Contracts
  1

  4

  

• Add check for vtable metadata of a different trait

  [C] Feature / Enhancement[E] Unsupported UBZ-CompilerBenchCIZ-EndToEndBenchCI
  #5001·miguelcorderopamphile opened Oct 14, 2026·

  ·

  · Soundness
  9

  

• Reject const-generic self types at trait resolution instead of panicking

  Z-CompilerBenchCIZ-EndToEndBenchCI
  #4999·kasimte opened Oct 12, 2026Contributor·

  ·

  · Contracts
  1

  7

  

• Resolve trait-object type arguments in contract target paths

  [C] Bug[C] Feature / Enhancement[F] CrashZ-CompilerBenchCIZ-EndToEndBenchCI
  #4986·kasimte opened Oct 7, 2026Contributor·

  ·

  · Contracts
  17

  

• Autoharness: skip fns whose const {} blocks depend on a substituted type

  [C] Bug[F] CrashZ-AutoharnessZ-CompilerBenchCIZ-EndToEndBenchCI
  #4981·acearyanarun opened Oct 6, 2026Contributor·

  ·

  · Autoharness
  1

  4