Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas

Dmitry V. Alexandrov

cs.LOAug 19, 2026

Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas

Authors: Dmitry V. Alexandrov

Organizations: HSE University, Moscow, Russia.

Abstract

We present the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant. TLS is a combinatorial framework originally motivated by Boolean satisfiability, based on triplet structures and a filter that we call Simple Vertex Intersection (SVI). We formalise the core of TLS, including its translation from 3-CNF, the clearing procedure, and the SVI algorithm. For the well-formed sliding-window fragment, we prove explicit polynomial-time bounds for the filter stages and verify the translation and intersection operations. Our main contribution is a precise correctness boundary: for general formulas, SVI non-emptiness is necessary but not sufficient for satisfiability; for aligned structures, we prove a full bi-implication, extended to systems of structures. We also formalise the grouped-window translation and provide a formal counterexample to its completeness. We introduce VFR (Verified Filter for Romanov's triplet logic), an extracted OCaml prototype that implements a verified decision procedure for the sliding-window fragment and a sound filter for general 3-CNF, with a Python runtime and Docker packaging. Benchmarks corroborate the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises over 23,000 lines of code, with 424 proved lemmas and no unproved assumptions.

Figures & tables

Component	Status	Reference / Caveat	Extr.
CTF, CTS, clearing definitions	Verified	Rocq 9.1.1, no admitted proofs	No
SVI soundness (forward)	Verified	Theorem 4.1	No
Aligned intersection (bi-impl.)	Verified	Theorem 4.3	No
Systemic aligned ( $k$ structs)	Verified	Theorem 4.4	No
Polynomial complexity	Verified	$O(n^{4})$ clearing (generic), $O(n^{2})$ clearing (single-forbidden) and SVI; $n$ = CTS size (tiers+triplets). Full solver includes exponential post-check	No
CNF $\to$ CTF (clause-by-clause)	Verified	Sliding-window CNF only	Yes

Table 1: Trust boundary: verified components, trusted base, and heuristics. “Extr.” indicates whether the component is extracted to executable OCaml code.

Panel of Figure 1 — Figure 1: Top: the compatible-degree property for triplet $t=(0,1,1)$ . Exactly two triplets are compatible in each direction (2-regular relation). Bottom: a valid path $101\to 010\to 101$ through three tiers, inducing the assignment $x_{0}=1,x_{1}=0,x_{2}=1,x_{3}=0,x_{4}=1$ . Overlapping positions enforce consistency across adjacent triplets. The path is drawn in assignment order (increasing tier indices); build_paths_all stores paths in reverse order, prepending each new triplet ahead of the current head (Listing 2 ).

Panel of Figure 2 — Figure 2: Levels of abstraction in VFR. Each layer transforms the representation toward a concrete variable assignment; the dashed arrow shows the verified feedback loop (OCaml-extracted eval_cnf ).

Panel of Figure 3 — Figure 3: The VFR solving pipeline as a flowchart. Only the SVI filter is formally verified for the sliding-window fragment; decomposition and post-check are unverified heuristics for general 3-CNF.

Stage	Time bound	Provenance
Decomposition (heuristic)	$O(m\cdot\log m)$	Grouping clauses by variable triples
Tier construction	$O(k)$	$k$ tiers, at most 8 triplets each
Clearing (generic)	$\leq 100n^{4}+100$	Theorem 7.1
Clearing (single-forbidden)	$\leq 2000n^{2}+2000$	Theorem 7.2
SVI filter	$\leq 3n^{2}+7$	Theorem 7.3
Full pipeline	$\leq 200n^{4}+200$	Theorem 7.4

Table 2: Verified polynomial complexity bounds (mechanised in Complexity.v and GapClosure.v )

Explore similar work

VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline
Apr 11, 2026Xuan Liu, Dheeraj Kodakandla, Kushagra Srivastva +1LLM Reliability Neuro-Symbolic AI
The Pennsylvania State University, University Park, Pennsylvania, USA
Power Term Polynomial Algebra for Boolean Logic
Mar 14, 2026Emanuele Sansone, Armando Solar-LezamaSymbolic Reasoning
CSAIL, MIT, USA · ESAT, KU Leuven, Belgium
Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning
Oct 11, 2026Debargha Ganguly, Weicong Chen, Mohsen Hariri +13LLM Agent Training LLM Agent Reliability
Case Western Reserve University · UT Austin · Microsoft Research

Apr 11, 2026J/K move · Enter open · S save

VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline

Xuan Liu, Dheeraj Kodakandla, Kushagra Srivastva, Mahfuza Farooque

The Pennsylvania State University, University Park, Pennsylvania, USA

LLM Reliability Neuro-Symbolic AI

Open paper AskPDF arXiv

VeriTrans is a reliability-first ML system that compiles natural-language requirements into solver-ready logic with validator-gated reliability. The pipeline integrates an instruction-tuned NL

\!\to\!

PL translator, round-trip reconstruction (PL

\!\to\!

NL) used as a high-precision acceptance gate, and canonical PL

\!\to\!

CNF compilation, all executed via fixed API configuration (temperature

=0

; fine-tuning runs use seed

=42

) and per-item artifact logging (prompts, outputs, hashes) to support auditability and replay-driven debugging. On SatBench (2{,}100 specifications), VeriTrans achieves 94.46% SAT/UNSAT correctness and 87.73% median round-trip similarity. Compact fine-tuning on 100--150 curated examples improves fidelity by about 1--1.5,pp without increasing latency (mean 25.8,s/spec on our 201-spec runtime subset). A thresholded acceptance policy on the round-trip score exposes a reliability--coverage knob: at

τ{=}75

, roughly 68% of items are retained with

\sim

94% correctness on the accepted set. Validator overhead contributes

<15\%

of end-to-end runtime, and all prompts/responses and timing metadata are logged to enable replay-driven debugging and regression testing. By separating learned translation from symbolic verification and enforcing deterministic, validator-gated acceptance, VeriTrans turns NL

\!\to\!

logic front-ends into auditable, reproducible components for reliability-critical workflows.

Abstract

Explore similar work

VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline

Power Term Polynomial Algebra for Boolean Logic

Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning