Does it not sit right with you either when people say bugs are inevitable and every system has its 0-day eventually? Let's meet up and talk about the options to never have that happen.
Turns out that systems for which mathematical proof that can never happen have made it out of academia and into production. An open source tooling ecosystem is also coming up at the moment.
Let's meet up and talk about what is possible already, what can be done and what should be done from the point of view of community-made software - there are a bunch of interesting implications with EU product liability and standards bodies may to require verification eventually.
I can give a short conceptual introduction about how proof works, what it covers, what else you need to fully trust your whole stack (by stealing shamelessly from talks people have given in the seL4 community) and give pointers to some documentation you can use to run a proven secure seL4 microkernel on your Raspberry Pi - the technical/mathematical detail beyond that is also still beyond me.
Get/Stay in touch: https://signal.group/#CjQKIIwPr-1D84DcrKdEcDEUjnDGWLLKhI9iM_NqRfSMbmQmEhCW30zKOq-nsiaT_afkyQyK
If after this you're itching to go prove something there is a workshop at the Nix assembly at 20:00 (unrelated to this), https://events.ccc.de/congress/2025/hub/en/event/detail/careful-whispers-of-proof-assistants-lean4-nix-nvi