Hacker GitHub

← All repos

seL4/l4v

View on GitHub ↗ ★ 657 Isabelle

seL4 specification and proofs

20 mentions on Hacker News by 18 people: 1 story, 19 comments · first 2015-09-18 · latest 2025-11-09

Mentions per year 20 mentions · busiest year 2022 (3)
20082026
AllStoriesComments NewestTopOldest
  1. …it's difficult work. [0] https://codeberg.org/Ironclad/Ironclad/src/branch/main/sourc... [1] https://github.com/seL4/l4v
    comment by AlotOfReading · 2025-11-09 · in Ironclad – formally verified, real-time capable, Unix-like OS kernel
  2. …the commits fixing it and amending seL4's proof are public: https://github.com/seL4/seL4/pull/243 https://github.com/seL4/l4v/pull/453 You will find a number of other memory related bugs in its issue tracker:…
    comment by ryao · 2025-03-23 · in The SeL4 Microkernel: An Introduction [pdf]
  3. I guess https://github.com/seL4/l4v/tree/rt is the ongoing verification work for that
    comment by cmrx64 · 2024-09-16 · in Ask HN: What runs L4-related microkernels/hypervisors these days?
  4. …[1] as well, but that's just a small part of the full verification process (described in [2]). [0]: https://github.com/seL4/l4v [1]: https://docs.sel4.systems/processes/style-guide.html#verific... [2]:…
    comment by aw1621107 · 2024-09-08 · in Google says replacing C/C++ in firmware with Rust is easy
  5. …The safety is achieved by a large external theorem prover and a synced copy written in Haskell. https://github.com/seL4/l4v Typechecks are form of proof. It's easier to write provably safe Rust than provably safe C because the proofs and…
    comment by pjc50 · 2024-02-28 · in Rewrite the VP9 codec library in Rust
  6. …can be achieved is sel4, which while it is written in C has a separate proof of its correctness: https://github.com/seL4/l4v The proof is much, much more work than the microkernel itself. A proof for something as large as webP might take…
    comment by pjc50 · 2023-09-12 · in Chrome: Heap buffer overflow in WebP
  7. …the specification and proofs are written in Isabelle, a proof assistant. Specification and proofs: https://github.com/seL4/l4v The microkernel itself: https://github.com/seL4/seL4 The main practical difference between testing and formal…
    comment by trealira · 2023-08-01 · in Ask HN: Would you pay to have code verified?
  8. …changes here: https://github.com/AmbiML/sparrow-kernel/commits/sparrow but I don't see a fork of https://github.com/seL4/l4v anywhere inside AmbiML. I mean, it does also claim to be "almost entirely written in Rust", which is true if you…
    comment by zahllos · 2022-10-16 · in Announcing KataOS and Sparrow
  9. …to convince the verifier. [0] https://github.com/seL4/seL4 [1] https://github.com/seL4/sel4test [2] https://github.com/seL4/l4v
    comment by gizmo686 · 2022-10-15 · in Uncovering a 24-year-old bug in the Linux Kernel (2021)
  10. I mean, just look at the commits with "fix" in the specs folder: https://github.com/seL4/l4v/commits/master?after=4f0bbd4fcbc...
    comment by jcelerier · 2022-07-04 · in Hardening attack surfaces with formally proven binary format parsers
  11. …isn't C, its Isabelle 92.9% Standard ML 3.0% Haskell 1.5% C 0.8% TeX 0.7% Python 0.5% Other 0.6% https://github.com/seL4/l4v
    comment by mkj · 2021-12-05 · in On Hubris and Humility: developing an OS for robustness in Rust [video]
  12. …with TLC, which gives you a lot of the advantages of formal methods with much less proof work. [1] https://github.com/seL4/l4v [2] https://www.idris-lang.org/ [3] https://idris.readthedocs.io/en/latest/tutorial/typesfuns.ht... [4]…
    comment by strangecasts · 2021-03-08 · in TLA+
  13. …proved just a small part of a system in a general way. 1: https://docs.sel4.systems/Hardware/ 2: https://github.com/seL4/l4v
    comment by jesse_m · 2020-03-12 · in SeL4 Design Principles
  14. …these tools, or compared to CompCert. CompCert looks and feels like a compiler, AutoCorres isn't. https://github.com/seL4/l4v/tree/master/tools/autocorres
    comment by sanxiyn · 2019-01-22 · in CompCert – A formally verified C compiler
  15. Yeah, that's the basic idea of refinement based program verification. An example of that is: https://github.com/seL4/l4v There are many programs which can be nicely specified with logic, and which could thus be treated this way. That we…
    comment by auggierose · 2019-01-21 · in A Bridge Too Far: E.W. Dijkstra and Logic
  16. …Unikernels - https://github.com/GaloisInc/HaLVM The specification model of the sel4 microkernel - https://github.com/seL4/l4v/tree/master/spec/haskell There are many smaller examples of OS projects in Haskell, but for better examples of…
    comment by Oribi · 2017-05-04 · in I tried Haskell for 5 years
  17. Here is seL4 proof: https://github.com/seL4/l4v To quote, "Most proofs in this repository are conducted in the interactive proof assistant Isabelle/HOL".
    comment by sanxiyn · 2016-11-18 · in Kaspersky OS
  18. …tools I've overlooked? [1] https://github.com/Beatgodes/klibc_framac_wp/blob/master/src... [2] https://github.com/seL4/l4v/blob/master/lib/Monad_WP/Strengt...
    comment by michaelt · 2016-11-04 · in Rules for Writing Safety Critical Code (2006)
  19. …[pdf paper] http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf - l4v (seL4 proofs git repo) https://github.com/seL4/l4v
    comment by monopolemagnet · 2015-09-18 · in The seL4 microkernel