Certus is verification software. Its most serious defect class is not a crash or an injection — it is a bound that is optimistic. A bound that is too large by any amount can turn an unsafe conjunction into a PROVEN CLEAR result.

Please report privately, and treat as security-relevant:

• any case where the certified lower bound exceeds the true minimum separation of the declared set;
• any propagation step that under-approximates rather than over-approximates;
• any floating-point path that rounds inward where the proof requires outward;
• any acceptance gate that can pass while its stated property is violated;
• anything that causes a conditional claim to be presented as unconditional.

Ordinary bugs — a crash, a bad error message, a slow path — are not security issues. Open a normal issue for those.

Use GitHub's Report a vulnerability button under the Security tab of this repository, which opens a private advisory. Do not open a public issue for a suspected soundness defect.

Please include, where you can:

• the conjunction record or a minimal synthetic reproduction;
• the values you observed and the values you expected;
• which ADR or acceptance gate you believe the behaviour contradicts.

A reproduction that fails an existing acceptance assertion is the most useful form a report can take.

You should get an acknowledgement within a week. A confirmed soundness defect is treated as stop-the-line: the affected claim is withdrawn from the handover and the decision records before any fix is designed, so that no document continues to assert a property that no longer holds.

This repository is a pre-prototype and is not deployed as a service. There is no production endpoint, no authentication surface, and no user data. Reports about hosting infrastructure are out of scope.