{"data":{"kind":"file","path":"README.md","version_id":"dqcxapc8a6gk7r1tbn9c67g6","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":1718,"modified_at":"2026-08-25T01:21:27.573000","content_hash":"def2daead192ccbfc9f6a5d8e830913b4d28740b399fdf63816b028abaf95d11"},"entries":[],"content":"# Formal Verification Trainer\n\nA comprehensive environment for training and evaluating LLMs on formal verification and model checking tasks.\n\n## Overview\n\nThis environment covers the core concepts of formal verification:\n\n- **Temporal Logic**: LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) formula construction and evaluation\n- **Kripke Structures**: State transition systems, labeling functions, and path quantifiers\n- **Model Checking Algorithms**: CTL model checking (fixed-point), LTL model checking (automata-based), bounded model checking\n- **Counterexample Generation**: Finding witness paths that violate properties\n- **Abstraction & Refinement**: CEGAR (Counterexample-Guided Abstraction Refinement)\n- **Safety & Liveness Properties**: Distinguishing and verifying system guarantees\n\n## Task Types\n\n1. **Formula Translation**: Convert natural language specifications to CTL/LTL formulas\n2. **Model Evaluation**: Given a Kripke structure and formula, determine satisfaction\n3. **Counterexample Construction**: Find a path violating a given property\n4. **Algorithm Tracing**: Step through fixed-point or automata-based model checking\n5. **Property Classification**: Identify safety vs liveness, CTL vs LTL expressibility\n6. **Abstraction Design**: Design predicate abstractions for verification\n\n## Scoring\n\n- **Correctness** (weight 0.40): Formula/solution accuracy\n- **Reasoning Quality** (weight 0.30): Step-by-step logical justification\n- **Completeness** (weight 0.20): All cases covered, edge cases handled\n- **Notation Conventions** (weight 0.10): Proper use of temporal logic syntax\n\n## Usage\n\n```python\nimport verifiers as vf\nenv = vf.load_environment(\"formal-verification-trainer\")\n```\n","encoding":"utf-8","truncated":false,"total_bytes":1718},"status":null}