Ironclad – formally verified, real-time capable, Unix-like OS kernel

Original Article ↗ Hacker News Discussion ↗

Landscape of New/Alt OS Projects

  • Commenters list many current efforts: SerenityOS, Asterinas (Linux‑compatible), Redox, Haiku, Plan 9, ReactOS, Managarm, Genode/Sculpt, LionsOS, Kirsch, TockOS, and other SPARK/Ada OSes like CuBit.
  • seL4 is repeatedly cited as the “gold standard” for a fast, formally verified microkernel and as a foundation for systems like LionsOS and Genode‑based Sculpt.
  • Some emphasize that whole‑system design matters more than raw IPC benchmarks; even a very fast microkernel can be slow if the ecosystem is poorly structured.

Ironclad’s Design, Scope, and Maturity

  • Ironclad is Unix‑like, POSIX‑compatible, written in SPARK/Ada, and currently targets x86_64 and riscv64. An earlier arm64 port existed but was removed due to bugs.
  • A user‑facing OS layer, Gloire, builds on Ironclad and uses GNU tooling, making it possible in principle to run Rust/Go/Java/Flutter apps as on any POSIX system.
  • Ironclad appears to be a monolithic kernel (drivers, FS, networking in kernel space), not a microkernel.
  • The project markets itself as (partially) formally verified and real‑time capable, but several commenters find the verification roadmap and existing specs thin, calling the “formally verified” label generous at this stage. Real‑time and hard‑RT claims are viewed as unproven without deeper artifacts.

Formal Verification: What It Is and Limits

  • Formal verification is contrasted with testing/fuzzing: it is machine‑checked proofs that code meets a specification for all inputs, often more lines of proof than kernel code.
  • SPARK/Ada’s strictness and executable semantics help, but commenters note that similar verification workflows exist for subsets of C, Lisps, Rust, etc.
  • Combining worst‑case execution time analysis, strong proofs, and POSIX compatibility is described as rare and difficult; Ironclad’s current proofs seem closer to “no obvious runtime errors” than deep OS theorems.

Security, RCE, and OS Design

  • One line of discussion argues that OS‑level RCEs are relatively cheap for state‑level actors and widely exploited against consumer devices and infrastructure; layered, capability‑based designs and formally verified isolation (e.g., seL4) are seen as crucial.
  • Others strongly dispute the claim that “any government can get RCE on any OS with pocket change,” stressing scarcity, high exploit value, defensive measures (air‑gapping, diodes, hardening), and the lack of visible “devastating” cyber‑effects in wars.
  • Some middle‑ground views note that systems thought to be air‑gapped often are not, and that social engineering plus local privilege escalation is often cheaper than exotic OS RCEs.

Licensing, Tools, and Ecosystem

  • There is a broad debate over GPL vs permissive licenses:
    • One side argues GPL’s “viral” nature forces corporate contributions and protects the commons.
    • The other claims GPL hinders adoption, complicates static linking, and that non‑scarce software doesn’t suffer from “bleeding the commons.”
  • SPARK itself is available under a free/open model with a commercial “Pro” tier, likened to Qt; tool pricing prompts some skepticism but not about Ironclad’s own code freedom.

Naming, Docs, and Miscellaneous

  • Some worry about name collisions with other “Ironclad” projects and potential trademark disputes; others clarify that overlapping trademarks are often legal if in different domains, though litigation risk exists.
  • Deepwiki’s AI‑generated “documentation” for Ironclad is controversial: some find it useful for code exploration; others criticize it as non‑wiki, potentially wrong, and misleadingly branded.
  • Questions about supported filesystems and full real‑time behavior remain unanswered in the thread and are thus unclear.