Alongside our commercial safety-critical systems work, we contribute to the community that shaped us. These projects embody the same principles as our commercial work: mathematical rigour, minimal dependencies, and code that proves its own correctness.
C-Sentinel
Semantic Observability for UNIX Systems
A lightweight system prober written in C that captures "system fingerprints" for AI-assisted analysis of non-obvious risks. Features auditd integration, explainable risk scoring, and a live web dashboard with multi-user authentication and role-based access control.
Key Features
- Multi-user authentication with role-based access control
- Two-factor authentication (TOTP) with QR code setup
- Explainable risk scoring — know why the score is what it is
- Auditd integration with process chain attribution
- Email and Slack alerts with rich formatting
- Security posture summary in plain English
- Public demo mode for showcasing
C-From-Scratch
Learn to Build Safety-Critical Systems in C
Not "Hello World". Real kernels. Mathematical rigour. A complete course teaching the methodology behind safety-critical software: prove first, code second.
"Sensors report. The Captain decides."
The Safety Stack
Seven modules that build from simple monitors to a complete safety-critical system:
Mode
The Captain — what do we DO about it?
Pressure
The Buffer — handle overflow
Consensus
The Judge — which sensor to trust?
Drift
Trending toward failure?
Timing
Is the rhythm healthy?
Baseline
Is the signal normal?
Pulse
Is the signal alive?
Sensors (1-4) → Judge (5) → Buffer (6) → Captain (7)The Approach
Math → Structs → Code Problem → Math Model → Proof → Structs → Code → Verification │ │ │ │ │ │ │ │ │ │ │ └── Does code match math? │ │ │ │ └── Direct transcription │ │ │ └── Every field justified │ │ └── Contracts proven │ └── State machine defined └── Failure modes analysed
What You'll Learn
- Analyse failure modes before writing code
- Define state machines that cover all cases
- Prove properties about your design
- Design data structures where every field is justified
- Implement Triple Modular Redundancy (TMR) voting
- Handle backpressure in bounded queues
- Orchestrate system modes with permission matrices
- Compose simple components into complex behaviour
"The open source outlives us."
— William Murray