update DO-178C messaging — witness ships v0.14 MC/DC chain tracking

.github/workflows/ci.yml

@@ -1,5 +1,9 @@
 name: CI
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.ref }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
 on:
   pull_request:
     branches: [main]

.github/workflows/deploy.yml

@@ -1,5 +1,17 @@
 name: Deploy
 
+# Release variant — never cancel a deploy mid-flight. A cancelled deploy
+# can leave the Netcup site in a half-deleted state (the script does
+# `find . -delete && tar -xzf`). Group by ref so two parallel pushes to
+# the same branch serialize cleanly without race-deleting each other.
+#
+# Security note: this concurrency block uses only server-controlled
+# context vars (github.ref, github.workflow) — no PR-author-controlled
+# input flows into the group key.
+concurrency:
+  group: release-${{ github.ref }}
+  cancel-in-progress: false
+
 on:
   push:
     branches: [main]

content/about.md

@@ -0,0 +1,5 @@
++++
+title = "About"
+description = "Open source. Pre-1.0. Each tool tests a thesis about AI-velocity verification for safety-critical software. Here's the bench, here's what it produced, here's what we don't yet know."
+template = "about.html"
++++

content/blog/2026-03-15-formal-verification-ai-agents.md

@@ -112,11 +112,13 @@ A single `bazel test //...` runs all proof tracks. No local tool installation re
 
 I want to be honest about what this approach does not yet solve.
 
-**MC/DC and structural coverage.** ISO 26262 recommends MC/DC for the highest ASIL levels. MC/DC was designed for C — measure which boolean conditions affect decision outcomes. A [joint paper by the German Aerospace Center and Ferrous Systems](https://arxiv.org/abs/2409.08708) investigated how MC/DC applies to Rust and found that it *is* applicable, but needs modification. Rust's pattern matching compiles to decisions that contain implicit conditions not visible in source code. The `?` operator desugars to hidden match expressions. Refutable patterns need to be treated as decisions with sub-conditions.
+**MC/DC and structural coverage.** ISO 26262 recommends MC/DC for the highest ASIL levels. MC/DC was designed for C — measure which boolean conditions affect decision outcomes. The historical reading of MC/DC-for-Rust as an open problem — Rust's pattern matching does not decompose into the boolean decisions MC/DC was designed for; the `?` operator desugars to hidden match expressions — has two answers now, working at different chain layers.
 
-The [Safety-Critical Rust Consortium](https://rustfoundation.org/safety-critical-rust-consortium/) — which includes Ferrous Systems, Arm, AdaCore, Toyota, and others — is [working on MC/DC support as a 2026 Rust Project Goal](https://blog.rust-lang.org/2026/01/14/what-does-it-take-to-ship-rust-in-safety-critical/). An earlier compiler implementation was removed due to maintenance concerns. The consortium is approaching it again with shared ownership between industry and the Rust project. This is an active area of work, not a solved problem.
+**witness** measures MC/DC structurally on the *post-rustc WebAssembly*, where pattern matching has already lowered to `br_if` and `br_table` and DWARF carries the source-line mapping back. v0.14 ships today with v3 MC/DC envelopes carrying DWARF inline-chain tracking up to 8 levels deep on real Rust (httparse). This is the same move DO-178C accepted in 1992 for "post-preprocessor C": measure what the compiler emits, not what the engineer typed. See [the variant-pruning argument](/blog/variant-pruning-rust-mcdc/) for why pattern matching, `?`, and cfg expansion are non-problems at the wasm level.
 
-I believe mathematical proofs of functional correctness provide strictly stronger evidence than any coverage metric — a proof covers all inputs, MC/DC covers only tested inputs. But this is a direction I am working toward, not a claim I can make today. The standards community and certification bodies have not yet accepted formal proofs as a replacement for structural coverage. That conversation is starting.
+The complementary **Rust-source MC/DC** work — the [joint paper by the German Aerospace Center and Ferrous Systems](https://arxiv.org/abs/2409.08708) and the [Safety-Critical Rust Consortium](https://rustfoundation.org/safety-critical-rust-consortium/) [2026 Rust Project Goal](https://blog.rust-lang.org/2026/01/14/what-does-it-take-to-ship-rust-in-safety-critical/) (Ferrous Systems, Arm, AdaCore, Toyota and others) — operates at the rustc-frontend layer. Different chain layers, different blind spots, additive evidence. Both are wanted in a full dossier; neither is a blocker for the other.
+
+I still believe mathematical proofs of functional correctness provide strictly stronger evidence than any coverage metric — a proof covers all inputs, MC/DC covers only tested inputs. But for the certification artefacts the standards community currently asks for, witness now ships the structural-coverage half today; proofs and witness layer additively, not as substitutes.
 
 **Tool qualification.** Three independent proof systems (Verus, Rocq, Lean) checking the same properties gives high confidence that no single tool's bug can cause a false positive. This supports a TCL1 (Tool Confidence Level 1) argument — but no assessor has evaluated this specific combination yet. The argument is sound in principle; it has not been tested in a certification audit.
 

sass/_blog.scss

@@ -236,6 +236,24 @@
     }
   }
 
+}
+
+// Mermaid light-mode color override is handled in JS, not CSS.
+//
+// Why: each post's `classDef` lines compile to CSS rules INSIDE the
+// rendered SVG's `<style>` tag, scoped by a dynamic id (`#mermaid-NNN`)
+// and marked `!important`. That combination of (ID selector +
+// !important + later source order than main.css) means outer CSS
+// cannot override them, regardless of attribute / class selectors or
+// added !importants.
+//
+// The fix lives in `templates/blog-page.html`: after mermaid renders,
+// the script walks each `.mermaid svg style` element and rewrites the
+// hardcoded dark hex values to their cream-mode equivalents. See the
+// `applyMermaidLightFix` function there.
+
+.blog-post__content {
+
   // Tables
   table {
     width: 100%;