# Verification **URL:** https://sel4.discourse.group/c/verification/5.md [Latest](https://sel4.discourse.group/latest.md) · [Categories](https://sel4.discourse.group/categories.md) · [Tags](https://sel4.discourse.group/tags.md) --- ## [About the Verification category](https://sel4.discourse.group/t/about-the-verification-category/12)
**Author:** [@anna.lyons](https://sel4.discourse.group/u/anna.lyons)\ **Replies:** 0
Questions around seL4 verification. What guarantees do the proofs provide? What are the limitations and assumptions? Use this category if you have questions about seL4 verification, including specific questions about is… --- ## [Refinement proof of the CapDL initialiser?](https://sel4.discourse.group/t/refinement-proof-of-the-capdl-initialiser/1065)
**Author:** [@Whatever314](https://sel4.discourse.group/u/Whatever314)\ **Replies:** 0\ **Last updated:** [July 15, 2026, 2:32am UTC](https://sel4.discourse.group/t/refinement-proof-of-the-capdl-initialiser/1065 "2026-07-15T02:32:59Z")
Hello everyone: I noticed an abstract specification of the CapDL initialiser in the SysInit proofs, however i could not find a refinement proof between the abstract specification and the provided c implementation in seL… --- ## [Reasoning about a sequentially-verified C component inside an seL4 partition — confinement vs. a more structured model?](https://sel4.discourse.group/t/reasoning-about-a-sequentially-verified-c-component-inside-an-sel4-partition-confinement-vs-a-more-structured-model/1060)
**Author:** [@Fikoko](https://sel4.discourse.group/u/Fikoko)\ **Replies:** 7\ **Last updated:** [July 13, 2026, 11:55am UTC](https://sel4.discourse.group/t/reasoning-about-a-sequentially-verified-c-component-inside-an-sel4-partition-confinement-vs-a-more-structured-model/1060 "2026-07-13T11:55:34Z")
Hello — I come at this from the formal-verification-of-C side and I’m still finding my feet with seL4, so a pointer from people who reason about the proof guarantees properly would be very welcome. I maintain a formally… --- ## [Does seL4's verification story guarantee the integrity of the kernel itself at runtime?](https://sel4.discourse.group/t/does-sel4s-verification-story-guarantee-the-integrity-of-the-kernel-itself-at-runtime/1047)
**Author:** [@Whatever314](https://sel4.discourse.group/u/Whatever314)\ **Replies:** 4\ **Last updated:** [April 29, 2026, 9:04am UTC](https://sel4.discourse.group/t/does-sel4s-verification-story-guarantee-the-integrity-of-the-kernel-itself-at-runtime/1047 "2026-04-29T09:04:29Z")
I know that the integrity proof guarantees a policy of integrity. But I wonder whether malicious calls of the kernel’s interfaces (i.e. vspace) that could interpolate the kernel’s code is allowed, though those callsalso … --- ## [Why Not a High Assurance Deliverable First?](https://sel4.discourse.group/t/why-not-a-high-assurance-deliverable-first/1012)
**Author:** [@indolering](https://sel4.discourse.group/u/indolering)\ **Replies:** 2\ **Last updated:** [September 11, 2025, 11:46pm UTC](https://sel4.discourse.group/t/why-not-a-high-assurance-deliverable-first/1012 "2025-09-11T23:46:18Z")
When SeL4 came out, the proofs were much more limited. IIRC we are now largely waiting for advancements on mixed criticality and multicore proofs. Is the proof process expected to force API changes? Is there no value … --- ## [Verification process in a commercial project](https://sel4.discourse.group/t/verification-process-in-a-commercial-project/775)
**Author:** [@dvd2792](https://sel4.discourse.group/u/dvd2792)\ **Replies:** 1\ **Last updated:** [July 11, 2024, 7:29am UTC](https://sel4.discourse.group/t/verification-process-in-a-commercial-project/775 "2024-07-11T07:29:29Z")
Hello, I’m having a hard time finding the answer to my question. In a real life & commercial system that needs to be accredited, how can the seL4 proofs by used by the accreditors? I have problems understanding what’s … --- ## [How to verify C functions with array parameters using Isabelle](https://sel4.discourse.group/t/how-to-verify-c-functions-with-array-parameters-using-isabelle/806)
**Author:** [@riyuejiuzhaoaaa](https://sel4.discourse.group/u/riyuejiuzhaoaaa)\ **Replies:** 3\ **Last updated:** [January 18, 2024, 4:20am UTC](https://sel4.discourse.group/t/how-to-verify-c-functions-with-array-parameters-using-isabelle/806 "2024-01-18T04:20:47Z")
I am using Isabelle to verify a C program. During the verification process, I used the c-parser install-C-file to load the code, but the following issue occurred： “attempt to cause decay to pointer on array without an a… --- ## [How to understand the role of Haskell model in seL4 verification](https://sel4.discourse.group/t/how-to-understand-the-role-of-haskell-model-in-sel4-verification/804)
**Author:** [@riyuejiuzhaoaaa](https://sel4.discourse.group/u/riyuejiuzhaoaaa)\ **Replies:** 1\ **Last updated:** [December 29, 2023, 12:31am UTC](https://sel4.discourse.group/t/how-to-understand-the-role-of-haskell-model-in-sel4-verification/804 "2023-12-29T00:31:38Z")
Hello everyone, I just started working on the verification of operating system kernels. During the process of learning seL4 verification, I don’t understand the role of Haskell models in the verification process. The c c… --- ## [Secure Access Controller Artifacts \[MILS Architecture\]](https://sel4.discourse.group/t/secure-access-controller-artifacts-mils-architecture/798)
**Author:** [@dara](https://sel4.discourse.group/u/dara)\ **Replies:** 3\ **Last updated:** [November 30, 2023, 11:40pm UTC](https://sel4.discourse.group/t/secure-access-controller-artifacts-mils-architecture/798 "2023-11-30T23:40:38Z")
Hello, I am looking at the (perhaps dated?) paper “Towards Proving Security in the Presence of Large Untrusted Components” and am interested in studying the Isabelle/HOL formalization thereof. However I cannot find it. … --- ## [Can the seL4 proofs handle recursive functions?](https://sel4.discourse.group/t/can-the-sel4-proofs-handle-recursive-functions/96)
**Author:** [@robert.vanvossen](https://sel4.discourse.group/u/robert.vanvossen)\ **Replies:** 3\ **Last updated:** [June 28, 2023, 8:06am UTC](https://sel4.discourse.group/t/can-the-sel4-proofs-handle-recursive-functions/96 "2023-06-28T08:06:32Z")
We are writing some code for the seL4\_libs where a recursive function makes the most sense. I know that part of the code is not verified, but it got me curious as to whether the seL4 proofs could handle recursive functio… --- ## [Formal security properties](https://sel4.discourse.group/t/formal-security-properties/678)
**Author:** [@AviShaked](https://sel4.discourse.group/u/AviShaked)\ **Replies:** 6\ **Last updated:** [March 24, 2023, 12:18pm UTC](https://sel4.discourse.group/t/formal-security-properties/678 "2023-03-24T12:18:21Z")
Hi, I am currently researching formal verification of systems from a security perspective. I found some interesting and relevant papers about seL4, but could not find the actual properties which seL4 was verified to sa… --- ## [The semantics style of the definition of data types](https://sel4.discourse.group/t/the-semantics-style-of-the-definition-of-data-types/594)
**Author:** [@amw\_zero](https://sel4.discourse.group/u/amw_zero)\ **Replies:** 7\ **Last updated:** [September 27, 2022, 9:06pm UTC](https://sel4.discourse.group/t/the-semantics-style-of-the-definition-of-data-types/594 "2022-09-27T21:06:04Z")
As we know, there are multiple style of program semantics: operational, axiomatic, denotational, etc. I’m wondering if data\_type forms its own kind of semantics for the programs that it represents. Let me expand. In the… --- ## [Why does the refinement proof require that the internal states of processes be related to one another?](https://sel4.discourse.group/t/why-does-the-refinement-proof-require-that-the-internal-states-of-processes-be-related-to-one-another/489)
**Author:** [@amw\_zero](https://sel4.discourse.group/u/amw_zero)\ **Replies:** 2\ **Last updated:** [March 7, 2022, 12:05am UTC](https://sel4.discourse.group/t/why-does-the-refinement-proof-require-that-the-internal-states-of-processes-be-related-to-one-another/489 "2022-03-07T00:05:27Z")
Hello, I’m trying to get a better understanding of the refinement proof strategy taken in sel4. In Section 2.1: Forward Simulation, the fw-sim statement contains the following clause: ∧ (∀event. Step C event O SR ⊆ SR O… --- ## [Forward vs. Backward Simulation in the Refinement Proof](https://sel4.discourse.group/t/forward-vs-backward-simulation-in-the-refinement-proof/490)
**Author:** [@amw\_zero](https://sel4.discourse.group/u/amw_zero)\ **Replies:** 2\ **Last updated:** [March 7, 2022, 12:01am UTC](https://sel4.discourse.group/t/forward-vs-backward-simulation-in-the-refinement-proof/490 "2022-03-07T00:01:52Z")
I have heard refinement, forward simulation, and backward simulation all mentioned in the broader context of semantic preservation between two processes. The distinction confuses me a bit. For example, in A formally ver… --- ## [State of tooling for formal verification](https://sel4.discourse.group/t/state-of-tooling-for-formal-verification/483)
**Author:** [@lazycandle55](https://sel4.discourse.group/u/lazycandle55)\ **Replies:** 1\ **Last updated:** [February 21, 2022, 3:41am UTC](https://sel4.discourse.group/t/state-of-tooling-for-formal-verification/483 "2022-02-21T03:41:01Z")
How do you think the tooling for performing proof engineering compares to all the tooling that exists for software development – code editors and IDE’s, language servers enabling code completion and refactoring, debugger… --- ## [L4v CRefine Failures Caused by Kernel Code Modifications](https://sel4.discourse.group/t/l4v-crefine-failures-caused-by-kernel-code-modifications/461)
**Author:** [@Jack.Chen](https://sel4.discourse.group/u/Jack.Chen)\ **Replies:** 5\ **Last updated:** [January 30, 2022, 10:41pm UTC](https://sel4.discourse.group/t/l4v-crefine-failures-caused-by-kernel-code-modifications/461 "2022-01-30T22:41:01Z")
In order to make it comply with certain industry software standards/guidelines, the seL4 kernel C code has to be slightly modified. In some cases, the modification causes l4v failures at CRefine. Example: The origina… --- ## [AutoCorres and Memory Safety](https://sel4.discourse.group/t/autocorres-and-memory-safety/445)
**Author:** [@amw\_zero](https://sel4.discourse.group/u/amw_zero)\ **Replies:** 3\ **Last updated:** [January 4, 2022, 10:29pm UTC](https://sel4.discourse.group/t/autocorres-and-memory-safety/445 "2022-01-04T22:29:29Z")
I’m using AutoCorres, and one thing that just crossed my mind is: how do I check for memory safety (specifically the absence of a buffer overflow) in the heap model? Let’s say I have an array of 3 unsigned ints in C, i.e… --- ## [SiFive Board Model Changes](https://sel4.discourse.group/t/sifive-board-model-changes/414)
**Author:** [@NonSecwitter](https://sel4.discourse.group/u/NonSecwitter)\ **Replies:** 1\ **Last updated:** [September 26, 2021, 10:36pm UTC](https://sel4.discourse.group/t/sifive-board-model-changes/414 "2021-09-26T22:36:34Z")
What changes between the HiFive Unleashed and HiFive Unmatched would effect the verification’s validity? How intensive is it to reverify for boards that are presumably somewhat similar? --- ## [Are you collaborating with RISC-V on the formal ISA spec?](https://sel4.discourse.group/t/are-you-collaborating-with-risc-v-on-the-formal-isa-spec/350)
**Author:** [@lazycandle55](https://sel4.discourse.group/u/lazycandle55)\ **Replies:** 2\ **Last updated:** [May 6, 2021, 3:53am UTC](https://sel4.discourse.group/t/are-you-collaborating-with-risc-v-on-the-formal-isa-spec/350 "2021-05-06T03:53:14Z")
Hello, First of all, congratulations on extending the RISC-V verification down to the binary level! :tada: I see seL4 and RISC-V have formed an alliance of sorts, and I was just curious if you are cooperatively working… --- ## [Multiple Domains Per Thread Proof Impact](https://sel4.discourse.group/t/multiple-domains-per-thread-proof-impact/292)
**Author:** [@nate.studer](https://sel4.discourse.group/u/nate.studer)\ **Replies:** 7\ **Last updated:** [February 26, 2021, 9:45pm UTC](https://sel4.discourse.group/t/multiple-domains-per-thread-proof-impact/292 "2021-02-26T21:45:21Z")
The first level time-sliced domain scheduler is a nice fit for some real-time applications, but the limitation of having each thread belong to only one domain complicates the system when a server cannot belong to multipl… --- ## [X86-64 verification roadmap](https://sel4.discourse.group/t/x86-64-verification-roadmap/312)
**Author:** [@ANogin](https://sel4.discourse.group/u/ANogin)\ **Replies:** 1\ **Last updated:** [February 23, 2021, 10:42pm UTC](https://sel4.discourse.group/t/x86-64-verification-roadmap/312 "2021-02-23T22:42:13Z")
Are you currently working on a more complete verification for x86-64 (multicore, hypervisor, beyond just FC)? If so, any guesstimates on when any of that might happen? Thanks! --- ## [How do you keep from introducing tautologies into the specification?](https://sel4.discourse.group/t/how-do-you-keep-from-introducing-tautologies-into-the-specification/142)
**Author:** [@lazycandle55](https://sel4.discourse.group/u/lazycandle55)\ **Replies:** 8\ **Last updated:** [November 9, 2020, 4:47am UTC](https://sel4.discourse.group/t/how-do-you-keep-from-introducing-tautologies-into-the-specification/142 "2020-11-09T04:47:19Z")
From what little I understand about formal specifications and proofs, I think it can be possible to write some logic in such a way that it unintentionally can be used to prove that anything as true. This seems like it w… --- ## [Compiling seL4 with CompCert](https://sel4.discourse.group/t/compiling-sel4-with-compcert/115)
**Author:** [@Kai](https://sel4.discourse.group/u/Kai)\ **Replies:** 5\ **Last updated:** [February 28, 2020, 3:36am UTC](https://sel4.discourse.group/t/compiling-sel4-with-compcert/115 "2020-02-28T03:36:47Z")
With gcc being part of the trusted base for all but ARMv7-A, have there been efforts to compile seL4 with CompCert? If so, what are the results? If not, why not? (Half expected this to be an FAQ, but didn’t find it.) --- ## [Which code is verified?](https://sel4.discourse.group/t/which-code-is-verified/17)
**Author:** [@anna.lyons](https://sel4.discourse.group/u/anna.lyons)\ **Replies:** 3\ **Last updated:** [April 15, 2019, 11:49pm UTC](https://sel4.discourse.group/t/which-code-is-verified/17 "2019-04-15T23:49:16Z")
The verification sees the entire C code for one particular combination of configuration options. Currently this is the imx6 platform, Cortex A9 processor, ARMv7-a architecture, all other config options unset (in particul…