Hi all,
I'm Fikret Güney Ersezer, and I'd like to introduce a new project proposal that has just been made public for community review:
Eclipse Canon-C.
Canon-C is a header-only semantic standard library for C99, designed around explicit ownership, predictable allocation, and formal verification. The goal is not to add new functionality to C, but to make program intent — ownership, lifetime, failure, and data
flow — visible directly at call sites, so that safety-critical C code is easier to read, reason about, and verify.
The project is targeted at the IoT and embedded space, with particular attention to RTOS and bare-metal environments.
What may interest this list specifically:
The substrate (core/primitives/ and some parts of core/) is formally verified using Frama-C WP with ACSL contracts. CI enforces named-residual invariants on every push to master — verification status is encoded as a contract, not a
soft target. Current state: 5 headers verified, ~4800 proof obligations, ~99% discharged automatically, with all unproved goals documented in a deviations record with manual proof arguments. The aim is to provide a reusable substrate that reduces the verification
burden for application code targeting DO-178C, ISO 26262, IEC 62304, and similar standards.
The proposal is now in community review (minimum 2 weeks per the EDP). Feedback, questions, and concerns from the ThreadX community would be very welcome — particularly from anyone with experience integrating verification-grade libraries into RTOS-based products,
or anyone who sees gaps where Canon-C's conventions wouldn't fit their workflow.
Best regards,
Fikret Güney Ersezer
_______________________________________________