Problem
The OWL export (gds-owl) handles semantic web representability. A proof assistant export would enable formally certified verification results — machine-checked proofs that structural properties hold.
Type
[MATH] [CODE]
Prioritization
- Criteria: C3 (Production readiness)
- Tier: 3 — Research Frontier
- Phase: 5 — Triggered, not scheduled
- Dependencies: T0-1, T0-2
- Triggered by: Safety-critical application requiring machine-checked proof
Pre-condition
T0-1 (check specifications as formal propositions) must be complete. Check specifications must be stated as formal propositions before they can be exported as proof obligations. Do not pursue formal verification until informal verification is well-specified and traceable.
Related
Part of the GDS-Core Improvement Roadmap
Scientific Context
Evidence level: Beyond Level 4 — machine-checked proofs that structural properties hold. This is the strongest possible evidence for correctness claims but requires significant proof engineering investment.
Verification Strategy
The exported proof obligations must correspond 1:1 to the check specifications from T0-1. Each exported lemma/theorem in Lean 4 or Coq must be traceable to a check ID (G-xxx, SC-xxx). The proof assistant's type checker IS the verification — if it compiles, the property holds.
Problem
The OWL export (gds-owl) handles semantic web representability. A proof assistant export would enable formally certified verification results — machine-checked proofs that structural properties hold.
Type
[MATH] [CODE]
Prioritization
Pre-condition
T0-1 (check specifications as formal propositions) must be complete. Check specifications must be stated as formal propositions before they can be exported as proof obligations. Do not pursue formal verification until informal verification is well-specified and traceable.
Related
Part of the GDS-Core Improvement Roadmap
Scientific Context
Evidence level: Beyond Level 4 — machine-checked proofs that structural properties hold. This is the strongest possible evidence for correctness claims but requires significant proof engineering investment.
Verification Strategy
The exported proof obligations must correspond 1:1 to the check specifications from T0-1. Each exported lemma/theorem in Lean 4 or Coq must be traceable to a check ID (G-xxx, SC-xxx). The proof assistant's type checker IS the verification — if it compiles, the property holds.