Skip to content

Formal Verification

Mathematical proof, satisfiability solving, and counterexample-guided synthesis -- the components that let G6 verify rather than just test.

Overview

This cluster contains only two components, but they pack significant capability. formal_methods provides 405 tools across 18 MCP sub-packages (16 active, 2 reference-only shells) covering propositional logic (DPLL), SMT solving (Z3), Prolog-style inference, and Lean-style theorem proving; mermaid_mcp and pics_to_latex_mcp are the two reference-only shells and do not register active tools. cegis implements the Counterexample-Guided Inductive Synthesis loop with progressive LLM agency reduction.

The design philosophy is "always-available verification." The propositional DPLL solver runs in pure Python with no external dependencies. Z3, Prolog, and Lean backends are lazily imported and gracefully degrade when unavailable. This means every G6 deployment -- even minimal ones -- can perform basic formal reasoning.

Backend results are not interchangeable

Missing or timed-out Z3, NuSMV, Prolog, or Lean checks are reported as unavailable/degraded results, not as proof failures and not as proof successes. For CSF bridge calls this appears as verified=None with an error message. Use pure-Python or CSF hazard gates as the fallback decision path, and reserve claims such as "formally verified by Z3/Lean/NuSMV" for runs where that backend explicitly returned verified=True.

Lean prover production checks

For direct lean_prover use, run lean_prover_lean_status first and require readiness.ga_ready=true with no remediation actions before treating Lean as a production-critical gate. verification_status="generated" and verified=false are unverified source, even when the generated Lean text looks plausible. verification_status="proved" is not enough on its own for policy approval; require verified=true or a stored verified theorem record. Use lean_prover_check_proof, lean_prover_replay_artifact, and lean_prover_enforce_policy before allowing results into medium, high, regulated, or safety-critical workflows.

Lean proving is valuable for audit trails and high-stakes reliability claims, but it is not a first-run onboarding feature for most non-technical users. In launch-pilot flows, surface it through guided recipes or templates rather than raw Lean/Lake/Mathlib setup.

CEGIS extends this by synthesizing small programs from specifications. Given a sketch with ?? holes and an oracle function, it iteratively fills holes, checks against the oracle, and refines using counterexamples. Agency levels (0-5) control how much LLM assistance the synthesizer uses, decaying each iteration toward purely programmatic strategies.

CEGIS scope

The CEGIS component is narrow by design. It works best for simple deterministic Python functions, explicit sketches, bounded hole values, and oracle/test-case validation. It should not be presented as a general-purpose production code synthesizer; a successful run means no counterexample was found under the configured validation strategy, not that arbitrary generated software is universally correct.

Components

Component Description MCP Tools
formal_methods SAT, SMT, DPLL, Z3, Prolog, Lean dispatch 405
cegis Narrow CEGIS loop for simple sketch specs, agency levels, and LLM-assisted hole filling --

Architecture

graph TD
    FM[formal_methods] --> DPLL[Propositional DPLL]
    FM --> Z3[Z3 SMT Solver]
    FM --> PROLOG[Prolog Engine]
    FM --> LEAN[Lean Backend]
    CEGIS[cegis] --> FM
    CEGIS --> SKETCH[SketchSpec]
    CEGIS --> ORACLE[Oracle Function]
    CEGIS --> AGENCY[AgencyLevel 0-5]
    CEGIS --> LLM_SYNTH[LLM Synthesizer]
    LLM_SYNTH -->|fallback| PROG[Programmatic Synth]

Key Patterns

Lazy Backend Dispatch. FormalMethodsBlock accepts a backend parameter (z3, propositional, prolog, lean) and dispatches accordingly. The propositional backend is always available; others use try/except imports. This lets the same MCP tool surface work across minimal and full installations.

Progressive Agency Decay. CEGIS starts at a configured AgencyLevel (e.g., CODE_AGENT=5) and decays each iteration via agency_for_iteration(start, iter, decay). By the final iterations, the synthesizer operates in fully programmatic mode (PROCESSOR=0), reducing LLM cost and increasing determinism.

Spec Format Convention. CEGIS uses the string format "f(x) == x * 2" for simple specifications. The engine parses the left-hand side for function name and arguments, the right-hand side for the target expression, and generates test inputs to verify candidate solutions.