Verification scope

This chapter is the contract for what the bridge verifies and what it only records. Translating a requirement is not the same as proving it. A witness becomes a proof property only when its response resolves to a vocabulary predicate.

What is verified

The bridge verifies a requirement when all of these hold:

• The requirement parses and classifies as ubiquitous, WHEN, WHILE, IF ... THEN, WHERE, or a Complex combination.
• Its response maps to one of the pure-boolean predicates in CEarchin.Vocabulary.
• The emitted witness carries canonical Chelis property metadata: chelis_role, property_source_kind, property_quantifiers, property_preconditions, and property_source_id.

chelis prove then runs those witnesses, and the .spans.json manifest resolves any failure back to the EARS requirement line.

Use c-earchin translate --strict to produce verification artifacts. Strict mode fails if any requirement response has no vocabulary predicate, so a clean strict run is the guarantee that every requirement became a real property.

The vocabulary

A resolved response maps to one of a fixed set of pure-boolean predicates over f32 values. They are the predicates c-earchin knows how to turn into a checkable property:

Predicate	Meaning
is_non_negative	a value is at least zero
is_positive	a value is greater than zero
within_tolerance	two values differ by at most a tolerance
is_monotone_increasing	output does not decrease as input increases
is_bounded_above	a value is at most a bound
is_bounded_below	a value is at least a bound
is_equal	two values are equal
converges_to	a value is within tolerance of a target
is_error_rejection	an unwanted condition is rejected

A response whose meaning is one of these resolves; anything else is a vocabulary miss.

What is recorded but not verified

Non-strict translation accepts vocabulary misses, so a team can keep a complete EARS corpus in Chelis-adjacent form even where a response has no matching predicate. Those witnesses are marked:

c_earchin_role: "recorded_only"
c_earchin_verification_status: "recorded_only"
c_earchin_vocabulary_target: "unresolved"

A recorded-only witness deliberately does not carry chelis_role: "property", so chelis prove does not report a vacuous pass for it. Read 0 passed, 0 failed on a recorded-only file as "nothing was verified", not as evidence of correctness.

For example, MISS-001 The engine shall make users happy. parses and classifies as ubiquitous, but make users happy resolves to no predicate. In non-strict mode it is emitted as recorded-only; in strict mode the translation fails.

What is outside the bridge

The bridge accepts the EARS text and preserves provenance. Verification fires only for resolved pure-boolean property witnesses. Responses that would need quantified binders over EARS variables, stateful or temporal or effectful properties, or predicates beyond the fixed vocabulary are not synthesized into checkable properties. They can still be carried as recorded-only artifacts.