Issues

• remove readTPIDRURO_ccorres

  seL4/l4v#1105 · Filter by author lsf37 opened on Oct 29, 2026

• crefine: add a theory for Haskell/C constant equality

  seL4/l4v#1097 · Filter by author lsf37 opened on Oct 26, 2026

• Prove HDCR.TDE invariant

  enhancement
  seL4/l4v#1094 · Filter by author lsf37 opened on Oct 25, 2026

• prove an invariant that registers are always sanitised

  enhancement
  seL4/l4v#1087 · Filter by author lsf37 opened on Oct 22, 2026

• model kernel ELF window for AArch64

  Aarch64
  seL4/l4v#1045 · Filter by author lsf37 opened on Aug 7, 2026
  3

• Have only one Arch_assms per architecture, use it and new tech to bypass Arch interpretation during instantiation.

  arch-split
  seL4/l4v#1044 · Filter by author Xaphiosis opened on Jul 31, 2026
  2

  

• Adjust lemmas named Arch_ in Refine

  arch-split
  seL4/l4v#1042 · Filter by author Xaphiosis opened on Jul 31, 2026
  

• The wps method should include a wp_pre step

  cleanupproof engineering
  seL4/l4v#1019 · Filter by author lsf37 opened on Jun 12, 2026

• hoare_vcg_prop (in default wp set) throws away non-throw information

  proof engineeringproof tools
  seL4/l4v#1007 · Filter by author Xaphiosis opened on Jun 2, 2026
  5

• detect and handle attribute packed

  C-parser
  seL4/l4v#994 · Filter by author lsf37 opened on May 21, 2026
  4

• Align non-zombie object references for arch capabilities between AInvs and Refine

  seL4/l4v#990 · Filter by author michaelmcinerney opened on Apr 30, 2026

• Modify operator precedence of |> and |< for more sensical expressions

  seL4/l4v#988 · Filter by author michaelmcinerney opened on Apr 17, 2026

• A place for folded machine_word_len lemmas

  arch-splitproof engineering
  seL4/l4v#984 · Filter by author Xaphiosis opened on Mar 30, 2026

• Treatment of local uninitialised variables in AutoCorres and C Parser

  question
  seL4/l4v#955 · Filter by author AntanasKal opened on Jan 22, 2026
  4

• stating multiple lemmas simultaneously

  seL4/l4v#954 · Filter by author lsf37 opened on Jan 22, 2026
  1

• crunch bundles

  proof engineeringproof tools
  Feature

  seL4/l4v#953 · Filter by author lsf37 opened on Jan 22, 2026
  1

• Intelligently create a bundle that hides word lemmas which expose LENGTH('a)

  arch-splitenhancement
  seL4/l4v#929 · Filter by author Xaphiosis opened on Oct 23, 2025

• Document arch-split technique of using "common ancestor" for splitting up locales

  arch-splitdocs
  seL4/l4v#926 · Filter by author Xaphiosis opened on Sep 26, 2025
  

• After arch-split, generic ArchAcc_R.thy has very little in it

  arch-splitcleanup
  seL4/l4v#920 · Filter by author Xaphiosis opened on Aug 22, 2025

• Improve formalisation of the reply objects and the reply stack

  enhancementMCS
  seL4/l4v#877 · Filter by author michaelmcinerney opened on Mar 31, 2025
  8

• make defs take attributes?

  cleanupproof engineering
  seL4/l4v#872 · Filter by author lsf37 opened on Mar 21, 2025

• consolidate equations between ASpec/Haskell constants into one theory

  seL4/l4v#858 · Filter by author lsf37 opened on Feb 26, 2025

• eliminate get_tcb

  cleanupproof engineering
  Task

  seL4/l4v#854 · Filter by author lsf37 opened on Feb 17, 2025

• Consolidate the various approaches we have to projecting from the kernel heap

  cleanupenhancementMCSproof engineering
  Task

  seL4/l4v#841 · Filter by author michaelmcinerney opened on Dec 13, 2024
  6

• Change lemmas to be state_ext where possible instead of det_ext

  cleanup
  seL4/l4v#839 · Filter by author corlewis opened on Dec 12, 2024