Google Announces KataOS and Sparrow

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

InfluxDB - Purpose built for real-time analytics at any scale.
InfluxDB Platform is powered by columnar analytics, optimized for cost-efficient storage, and built with open data standards.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured
  • sparrow-kernel

    Discontinued The seL4 microkernel

    Yes, especially 'logically impossible' when you dig into the details. From the blogpost:

    > and the kernel modifications to seL4 that can reclaim the memory used by the rootserver.

    MMMMMMMMMMMkkkkkk. So you then have to ask: were these changes also formally verified? There's a metric ton of kernel 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 ignore almost the entire OS part of the OS (the kernel and the minimal seL4 runtime).

  • InfluxDB

    Purpose built for real-time analytics at any scale. InfluxDB Platform is powered by columnar analytics, optimized for cost-efficient storage, and built with open data standards.

    InfluxDB logo
  • l4v

    seL4 specification and proofs

    Yes, especially 'logically impossible' when you dig into the details. From the blogpost:

    > and the kernel modifications to seL4 that can reclaim the memory used by the rootserver.

    MMMMMMMMMMMkkkkkk. So you then have to ask: were these changes also formally verified? There's a metric ton of kernel 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 ignore almost the entire OS part of the OS (the kernel and the minimal seL4 runtime).

  • camkes-tool

    The main CAmkES tool

    Those names come from the existing seL4 project that these googlers are merely using/forking.

    (CAmkES is a hot mess, and "unpleasantly too much C" if you ask me. https://docs.sel4.systems/projects/camkes/ & https://github.com/seL4/camkes-tool/blob/master/docs/index.m...)

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts

  • SeL4 Specification and Proofs

    1 project | news.ycombinator.com | 20 Aug 2023
  • Proofs and specifications

    1 project | /r/RISCV | 13 Mar 2022
  • Proofs and specifications

    1 project | /r/kernel | 13 Mar 2022
  • Proofs and specifications

    1 project | /r/computerscience | 13 Mar 2022
  • Proofs and specifications

    1 project | /r/seL4 | 13 Mar 2022