All pull requests

Pull requests

• prove: verify AtomicCpuId exec methods

  AI-assistexec code
  #812·Marsman1996 opened Oct 1, 2026Collaborator·

  ·

• WIP: refactor pagetable permissions and change FrameRef perms

  #811·rikosellic opened Sep 28, 2026Collaborator·

  ·

• Rcu typed root history

  #805·hiroki-chen opened Sep 23, 2026Collaborator·

  ·
  1

• prove: EarlyFrameAllocator::alloc

  AI-assistexec code
  #802·Marsman1996 opened Sep 23, 2026Collaborator·

  ·
  7

• prove: memory region constructors and normalization

  AI-assistexec code
  #797·DID-Lab-SZU opened Sep 21, 2026Collaborator·

  ·
  8

• prove: arch/x86/kernel/acpi

  AI-assistexec code
  #789·Marsman1996 opened Sep 20, 2026Collaborator·

  ·
  20

• TypeId in Verus to support Any

  #720·SNoAnd opened Aug 23, 2026Collaborator·

  ·
  4

• feat: introduce generic multi-architecture paging/address-space model

  #710·DID-Lab-SZU opened Aug 17, 2026Collaborator·

  ·
  19

• Any-style dynamic downcasts

  #707·SNoAnd opened Aug 12, 2026Collaborator·

  ·

• prove: arch::pci (x86) & io

  AI-assistexec code
  #706·Marsman1996 opened Aug 12, 2026Collaborator·2 tasks done·

  ·
  71

• Prove tlb flush functions

  AI-assist
  #677·DID-Lab-SZU opened Jul 30, 2026Collaborator·

  ·
  10

• Align dma_stream helper structure with mainline

  #617·Je5s1e opened Jul 7, 2026Collaborator·

  ·
  2

• prove axiom fn in tlb.rs

  AI-assistplatform-issue
  #570·Je5s1e opened Jun 29, 2026Collaborator·

  ·
  4

• prove: mm/heap

  #505·Marsman1996 opened Jun 5, 2026Collaborator·

  ·
  7

• WIP: Weak memory support

  AI-assistenhancementexec codemodel design
  #487·hiroki-chen opened Jun 1, 2026Collaborator·3 tasks done·

  ·
  42

  

• Try to use dyn InAtomicMode

  #474·rikosellic opened May 24, 2026Collaborator·

  ·
  6

• Make PageTableConfig::TOP_LEVEL_CAN_UNMAP be associated const

  verus-toolchain
  #408·rikosellic opened Apr 14, 2026Collaborator·

  ·
  2