Search results

The wps method should include a wp_pre step

cleanup

proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofs

Status: Open.

#1019 In seL4/l4v;

· lsf37 opened on Jun 12, 2026

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

proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofs

proof toolsconvenience, automation, productivity toolsconvenience, automation, productivity tools

Status: Open.

#1007 In seL4/l4v;

· Xaphiosis opened on Jun 2, 2026

detect and handle attribute packed

C-parseranything about the C/Simpl parseranything about the C/Simpl parser

Status: Open.

#994 In seL4/l4v;

· lsf37 opened on May 21, 2026

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

Status: Open.

#990 In seL4/l4v;

· michaelmcinerney opened on Apr 30, 2026

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

Status: Open.

#988 In seL4/l4v;

· michaelmcinerney opened on Apr 17, 2026

A place for folded machine_word_len lemmas

arch-splitsplitting proofs into generic and architecture dependentsplitting proofs into generic and architecture dependent

proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofs

Status: Open.

#984 In seL4/l4v;

· Xaphiosis opened on Mar 30, 2026

Treatment of local uninitialised variables in AutoCorres and C Parser

question

Status: Open.

#955 In seL4/l4v;

· AntanasKal opened on Jan 22, 2026

stating multiple lemmas simultaneously

Status: Open.

#954 In seL4/l4v;

· lsf37 opened on Jan 22, 2026

crunch bundles

proof engineeringnicer, shorter, more maintainable etc proofsnicer, shorter, more maintainable etc proofs

proof toolsconvenience, automation, productivity toolsconvenience, automation, productivity tools

Status: Open.

Feature

#953 In seL4/l4v;

· lsf37 opened on Jan 22, 2026

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

arch-splitsplitting proofs into generic and architecture dependentsplitting proofs into generic and architecture dependent

enhancement

Status: Open.

#929 In seL4/l4v;

· Xaphiosis opened on Oct 23, 2025

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

arch-splitsplitting proofs into generic and architecture dependentsplitting proofs into generic and architecture dependent

docsDocumentation, READMEs, etcDocumentation, READMEs, etc

Status: Open.

#926 In seL4/l4v;

· Xaphiosis opened on Sep 26, 2025

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

arch-splitsplitting proofs into generic and architecture dependentsplitting proofs into generic and architecture dependent

cleanup

Status: Open.

#920 In seL4/l4v;

· Xaphiosis opened on Aug 22, 2025