Passt es euch auch irgendwie nicht, wenn Leute sagen Bugs sind alternativlos und jedes System hat früher oder später seine 0-days? Wir treffen uns uns sprechen über die Möglickheiten, das nie passieren zu lassen.
Es stellt sich heraus, dass die ersten Systeme für die mathematisch bewiesen ist, dass das nicht passieren kann es aus der Forschung in den Produktivbetrieb geschafft haben. EIn open source Tooling-Ökosystem entsteht auch gerade.
Wir treffen uns, um darüber zu sprechen, was schon geht, was möglich gemacht werden kann und was aus Perspektive von community-getrragener Software getan werden sollte - es gibt interessante Implikationen der EU-Produkthaftung und Standardisierungsremien könnten auf kurz oder lang verifizierung einfordern.
Ich kann eine kurze konzeptionelle Einführung darein geben, wie das Beweisen funktioniert, was es abdeckt und was es noch braucht um dem ganzen Stack vertrauen zu können (indem ich schamlos von Vorträgen aus der seL4-community klaue) und auf Dokumentation verweisen, die man benutzen kann, um den als sicher bewiesenen seL4-Mikrokernel auf einem Raspberry Pi zu benutzen - technische/mathematische Details darüber hinaus sind aber auch mir auch immernoch unklar.
Get/Stay in touch: https://signal.group/#CjQKIIwPr-1D84DcrKdEcDEUjnDGWLLKhI9iM_NqRfSMbmQmEhCW30zKOq-nsiaT_afkyQyK
Wenn ihr danach Lust habt, gleich mal etwas zu beweisen gibt es um 20:00 bei der Nix-Assembly einen workshop (unabhängig von diesem Meetup): https://events.ccc.de/congress/2025/hub/en/event/detail/careful-whispers-of-proof-assistants-lean4-nix-nvi