research lead: autoformalize NL requirements → Lean with proved ↔-equivalence as cert evidence

[avrabe]

From a focused web-research pass — a lead where rivet is plausibly ahead of the literature.

The technique: translate an NL requirement → Lean proposition, then prove the biconditional PA ↔ PB to decide requirement equivalence/consistency (DeepSeek-Prover-V2 on automotive safety reqs — https://arxiv.org/html/2511.11829).

rivet's edge: that work's single biggest manual bottleneck is variable grounding (establishing that differently-named symbols mean the same thing). rivet's typed, pre-grounded requirements largely solve that — turning their POC bottleneck into an automated step.

The open gap (publishable): no one packages autoformalized requirements as DO-178C/ISO 26262 traceability/certification evidence with a machine-checkable artifact (https://arxiv.org/html/2507.14330v1). rivet + gale/scry's Lean could be first.

Guardrails to adopt regardless: round-trip back-translation + symbolic equivalence checks; never trust an LLM-judge equivalence score (autoformalization survey: 97%→67% on manual check — https://arxiv.org/html/2505.23486v1). DeepSeek-Prover-V2 7B is locally runnable as the proving backend.

(Tracking issue from research; not scoped to a release yet.)

[avrabe]

Triaged from the dogfooding loop — interesting and well-sourced, but the "rivet's edge" claim needs one important qualification before it's load-bearing.

The technique is real and cited correctly. NL → Lean prop → prove PA ↔ PB for equivalence/consistency (the DeepSeek-Prover-V2 automotive-reqs work) is a sound framing, and the "package autoformalized reqs as machine-checkable cert evidence" gap looks genuinely open. The guardrails (round-trip back-translation, symbolic equivalence, never trust an LLM-judge score — the 97%→67% drop) should be adopted regardless; agreed.

The qualification — what rivet actually grounds today (verified against the schemas + the artifact model):

• rivet's typing covers artifacts and links: a requirement is id + title + description + typed links (traces-to/satisfies/refines/verifies/…) + schema-defined fields. That gives you requirement-level identity and relationships for free — which requirement is which, and how they connect.
• BUT the requirement's actual proposition lives in description as free natural-language prose. There is no glossary / vocabulary / ontology / typed-term artifact type in any shipped schema (grep across schemas/*.yaml: none), and no typed in-text entity references.

The cited paper's "variable grounding" bottleneck is precisely symbol/entity-level grounding inside the requirement text — establishing that "vehicle speed" in req A and "v_ego" in req B denote the same quantity. rivet does not model that today. So the honest statement is:

rivet solves requirement-identity grounding (and so removes the "which formalized props should we even compare?" ambiguity), but it does not yet solve in-text symbol grounding — which is the specific bottleneck the paper calls out.

Concrete path to actually earn the claimed edge (the publishable bit): add a typed glossary / domain-vocabulary artifact type whose terms are referenceable from requirement descriptions (a defines-term / references-term typed link). Then the LLM autoformalizer grounds each in-text symbol to a stable typed term id instead of re-grounding by name every time — that's the step that turns the paper's manual bottleneck into an automated one, and it's a natural fit for the existing references:-style link mechanism (no new directive needed, per the reuse-patterns convention).

There's already a schemas/research.yaml — if this graduates from tracking, a research-lead artifact there (with the arXiv links as cited-source external anchors) would dogfood the cert-evidence packaging this issue is about. Leaving open as a research lead; no code action this iteration.