Creation Review

Hi Angelo, thanks for looking at the project this closely — all three questions land on real decisions, so let me answer each with the reasoning rather than just the state.

clang-tidy: partially intentional, and your point stands. The check set was committed, but it lived pinned inside the CI workflow (.github/workflows, static-analysis job) as an explicit list run with --warnings-as-errors on the same set — the idea being that CI is the single normative analysis configuration. What was missing, as you note, is a .clang-tidy file at the repo root, which cost IDE users the configuration. That's now fixed: .clang-tidy is committed at the root as the single source of truth, and the CI invocation consumes it instead of carrying an inline copy — same 19 correctness/UB-adjacent checks, same warnings-as-errors severity, byte-equivalent behavior.

TSan: not currently, and deliberately so at this stage. Canon-C today owns no threads: every module is single-threaded by construction, the test suite runs sequentially, and the deductive verification (Frama-C/WP) assumes sequential semantics — so TSan over the current suite would instrument no concurrent accesses. The honest gap your question exposes right now is documentation rather than tooling: the library does have mutable global state (the contract-handler pointer, the diag context) whose thread-safety contract — objects are single-owner; globals are configure-before-threads — should be stated explicitly rather than implied, and I'm adding a thread-safety section to the docs to that effect.

But concurrency is on the roadmap, not deferred indefinitely. The current structural work is an external-classifications repository for the project; once that structure is in place, concurrency work begins, and a dedicated threading/concurrency repository is planned to follow. I've also had exchanges on the forum with members of the seL4 team about verified threading and concurrency, which is informing how that work will be scoped — in particular, keeping the deductive story honest: WP has no concurrency model, so the concurrency tier will be runtime-verified first (its own test suite, TSan as a first-class CI job — necessarily a separate build, since TSan and ASan cannot share a binary), with the same discipline the sequential library uses: documented invariants, pinned baselines, and explicit records of what is and is not formally covered. When that repository lands, your TSan question gets answered in CI rather than in a comment.

C23: agreed it's where embedded should be heading, and there's one C23 feature that is almost poetic for this project: <stdckdint.h> standardizes exactly the checked-arithmetic surface Canon-C's checked.h provides and formally verifies. The plan is layered rather than a migration. C99 remains the Tier-1 baseline contract, because it's what certified embedded toolchains and the MISRA ecosystem reliably support today, and — decisive here — it's what Frama-C/WP verifies with mature semantics: the verified configuration is pinned to the exact preprocessed bodies the prover sees, so a language-mode change is a new verification configuration, not a compiler flag. Concretely, C23 will arrive as an additive, feature-detected mode (__STDC_VERSION__ >= 202311L) where it strengthens guarantees — ckd_* as a preferred checked.h backend with the verified C99 path remaining the semantic reference, plus the low-risk wins (bool/true/false as keywords, unreachable(), standard attributes). A fully C23-verified configuration follows when Frama-C's C23 front-end support matures enough to re-pin the proof baselines under it. I'll spell these stages out in the roadmap.

Thanks again for the careful read — the thread-safety docs section and the C23 roadmap staging are the two remaining items from this exchange, and both will land in docs shortly.