Send us one critical execution path.We find where its timing actually fails.

For code that has to finish on time.

Brain–computer interfaces

Acquisition, timestamping, decode and feedback paths.

Robotics

Control loops, runtimes and schedulers, sensor fusion.

Medical and safety-relevant devices

The path a timing claim in your documentation depends on.

Embedded Rust and C

no_std, RTIC, Embassy, FreeRTOS, Zephyr, bare metal.

Real-time Linux

PREEMPT_RT control paths, lock-free queues, isolated cores.

Industrial edge

Controllers, fieldbus timing, deterministic gateways.

The usual trigger: a timing number is about to reach a customer, an auditor, an investor or a regulator, and nobody outside the team has checked where it stops holding.

The boundary is a number. It is rarely the obvious one.

Two tasks, fixed priority, preemptive. How far can the lower-priority task’s execution time grow before it misses its deadline?

task A   C 100 µs   T  400 µs   D  400 µs   higher priority
task B   C   ?      T 1000 µs   D 1000 µs   lower priority

  C(B) µs    R(B) µs    slack µs
      200        300        +700    holds
      400        600        +400    holds
      600        800        +200    holds
      601        901         +99    holds    +1 µs of work, −101 µs of slack
      700       1000           0    holds    ← the boundary
      701       1001          −1    misses

Task set from the public worked example in dy-wcet. Rows recomputed with the response-time recurrence and cross-checked against an independent schedule simulator in the same repository. Your path gets the same treatment with your numbers.

Eight questions, one path.

Timing claims

WCET and response-time figures, checked against the code and the task model they rely on.

Scheduling assumptions

Priorities, periods, preemption, blocking and release jitter, written down and tested.

Concurrency

Locks, lock-free structures, ISR-to-task sharing, priority-inversion windows.

Jitter

Where variation enters the path, and how much it can add in the worst case.

Determinism

Allocation, unbounded loops, retries, time sources, run-to-run variance.

Unsafe boundaries

Every unsafe block on the path and the invariant it depends on. Bounded proofs with Kani where the code allows.

Evidence quality

What your current measurements and tests can show, and what they cannot.

Reproducibility

Whether someone outside the team can re-derive your numbers from what you publish.

A verdict you can check.

The verdict

Holds, holds under stated conditions, does not hold, or cannot be decided from the evidence supplied.

The boundary

The condition at which the claim stops holding, stated as a number wherever the analysis allows one.

The findings

Ranked by consequence, each tied to a file and line at the commit you sent.

The evidence

Inputs, derivations, Kani harnesses where used, and a measurement harness you can run on your own hardware.

The reproduction

One repository or patch. Every number in the verdict can be recomputed.

The line between analysis and measurement

Stated finding by finding. We do not report a measured WCET on silicon we did not measure.

Five steps, all in writing.

1. Email the intakeTo connect@axonos.org: the path, the claim, how we reach the code, and the target.
2. Scope confirmed within 12 hoursWhether the path can be examined as sent, the scope in one paragraph, and an invoice for $950. If it cannot be examined, you pay nothing.
3. PayBank transfer or DOGE. The details are on the invoice. Your NDA, if you need one, comes back signed with the scope.
4. The 72 hours startWhen payment is confirmed and the intake is complete. Questions, if any, arrive in writing.
5. Verdict deliveredBy email, with the evidence as a repository or archive. No meetings at any step.

Path: (name and entry point: function, ISR, task or loop)
Claim: (the timing or determinism claim to examine, e.g. "the control step completes within 250 µs at 1 kHz")
Code: (repository URL and commit, or how you will share it)
Target: (CPU or MCU and clock, RTOS or executor, toolchain, build profile)
Task set: (periods, priorities, deadlines, execution-time budgets or measurements, if any)
Evidence you already have: (measurements, traces, CI logs; optional)
Payment: (bank transfer / DOGE)
Invoice to: (legal name, address, tax ID if needed)
NDA: (attach yours if you need one)

Two ways to pay.

Payment details are sent with the invoice, after the scope is confirmed in writing.

• One fixed price. $950 for one path. Transfer fees are paid by the sender.
• Nothing invoiced before the scope is confirmed. If the path cannot be examined as sent, you pay nothing.
• If the verdict contains no concrete engineering finding, the fee is refunded in full, in the currency it was paid in.
• Your code and the results stay private. Nothing is published without your written consent.

Published, and checkable.

• dy-wcet

  Worst-case response time for fixed-priority task sets, in no_std Rust with integer arithmetic that refuses rather than rounds. Unsafe forbidden, no dependencies, eight Kani harnesses that verify and gate the build.

• The correction record

  When the Kani harnesses did not verify, the crate said so in public. The changelog records each release that removed one cause, until the harnesses closed and the job became a required gate.

• Embassy #6528, RP2350 lost alarm

  A source-level analysis of an open timing failure in embassy-time, where a quiet timer queue turns a short arming race into a stall of minutes. It separates what the report proves from what is still a hypothesis.

• Cross-check: AxonOS against dy-wcet

  Two implementations on one task set, and why the first agreement between them proved almost nothing.

Not a certification and not a safety case. One path per examination. Findings are analytical unless you supply hardware data or run the harness, and the verdict says which is which.