This archive contains the complete research artifact for the paper "Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-Window 3-CNF with Application to Structured Formulas" (2026). CONTENTS -------- - theories/ — Coq/Rocq formalization (17 .v files, 427 lemmas and theorems, 0 admits) * Theorem 1 (weak & compat), Theorem 2 (systemic aligned) * Algorithm.v — verified path-building and effective procedure * FormulaTranslation.v — CNF ↔ CTF soundness * Complexity.v — polynomial cost model (O(n⁴) generic, O(n²) single-forbidden) * Structured.v — verified grouped sliding CNF solver * Counterexample.v — formalized incompleteness proofs - OCaml extraction — vfr_solver (JSON bridge to verified code) - Swansea RUP checker — Coq/Rocq-extracted UNSAT proof verifier - Python reference implementation — solver, CTF/CTS, hyperstructures, tests - Docker — fully reproducible multi-stage build - 175 pytest tests + 3 empirical verification scripts - TLA+ specifications (17 modules) VERIFIED COMPONENTS ------------------- - Sliding-window CNF → OCaml vfr_solver (extracted) - Grouped sliding CNF → OCaml solve_grouped_sliding (extracted) - Overlapping single-group CNF → OCaml solve_overlapping_single_group (extracted) - UNSAT proofs → Swansea RUP checker (Coq-extracted) REPRODUCIBILITY --------------- See DEPLOY.md for artifact evaluation instructions: docker build -t vfr . && docker run --rm vfr THIRD-PARTY COMPONENTS ---------------------- The Docker image includes third-party tools and libraries (Z3, Rocq/Coq, OCaml, Python packages, Ubuntu system packages, and the Swansea RUP checker). Their licenses are summarized in THIRD_PARTY_LICENSES.md. The VFR project itself is released under the MIT License.