Open Source

30 years of UNIX. Time to give some back.

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.

104KB
Binary Size
Zero
Dependencies
v0.6
Current Release
MIT
License

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.

7
Modules
42
Lessons
98
Tests
MIT
License

"Sensors report. The Captain decides."

The Safety Stack

Seven modules that build from simple monitors to a complete safety-critical system:

7

Mode

The Captain — what do we DO about it?

NEW
6

Pressure

The Buffer — handle overflow

NEW
5

Consensus

The Judge — which sensor to trust?

NEW
4

Drift

Trending toward failure?

NEW
3

Timing

Is the rhythm healthy?

2

Baseline

Is the signal normal?

1

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