dy-wcet

Worst-case response time for a fixed-priority task set, with release jitter, blocking and optimal priority assignment, computed in exact integer arithmetic that refuses rather than rounds. No floating point anywhere in the source, tests or proofs, zero dependencies, no_std with no allocator, so the same calls admit or refuse a task at run time on the device. When it cannot justify a figure it says why, through six named refusals, overflow among them. Eight Kani harnesses run on every push, results are cross-checked against a second computation of the busy period and against a simulated scheduler, and the examples in the README are compiled as tests. Funding pays for a year of maintenance, wider analysis models and an external review of the arithmetic.