Formal Methods¶

Formal Methods — mvp.formal_methods

Cluster: Formal Verification | Type: component | MCP Tools: 437

Overview¶

formal_methods dispatches formal verification queries to solver backends (Z3, Lean, Prolog, TLA+, DPLL, SageMath, Catlab, and more) for propositional logic, SMT solving, theorem proving, and model checking. It exposes 405 tools across 18 MCP sub-packages (16 active, 2 reference-only shells). mermaid_mcp and pics_to_latex_mcp are the deprecated reference-only shells and do not register active tools.

When to use:

• Verifying safety invariants and pipeline correctness properties
• SAT/SMT solving for constraint satisfaction problems
• Formal proofs via Lean, Curry-Howard, or Prolog-style reasoning
• Checking that an NL->formal translation captured intent before trusting a verified result (intent_fidelity.check_translation_fidelity / autoformalization translation_fidelity field): emits a plain-language back-translation + a risk-tiered, solver-grounded translation-confidence that floors completion_state fail-closed.

Example:

from mvp.formal_methods import FormalMethodsBlock, LogicalQuery

block = FormalMethodsBlock(name="fm")
result = block.infer(LogicalQuery(solver="propositional", formula="(A | B) & ~A"))
# result.ok → True; result.value → FormalResult with satisfiable=True

Works well with: core, align_csf, cegis, meta_programming

Public API¶

FormalMethodsBlock(AIBlock[LogicalQuery, FormalResult, None])¶

Dispatches formal verification queries to the appropriate solver.

Methods:

infer(data: LogicalQuery) -> Result[FormalResult]¶

capability_plan(op: str, params: dict) -> CapabilityResolution¶

heavy_dependency_status() -> list[dict]¶

list_patterns() -> dict[str, object]¶

Return the applied deterministic-reliability pattern catalog.

FormalMethodsPatternRuntime¶

Deterministic assurance re-derivation + result self-check (no LLM, no I/O).

Methods:

classify_assurance(solver_used: str, verified: bool, toolchain_available: bool, conclusive: bool, failed: bool = False) -> tuple[str, bool]¶

Re-derive (assurance_level, review_required) from first principles.

validate_result(result: Any) -> list[str]¶

Return internal-consistency violations of an emitted FormalResult.

assert_consistent(result: Any) -> Any¶

Live-path guard: raise if the emitted result is internally inconsistent.

LogicalQuery(BaseModel)¶

Input for FormalMethodsBlock.

FormalResult(BaseModel)¶

Result from FormalMethodsBlock.

FormalMethodsSkill¶

Methods:

compact() -> dict[str, Any]¶

FormalMethodsSkillCatalog¶

Maps each applied pattern slug to a formal_methods deterministic-reliability skill.

Methods:

list_skills() -> list[FormalMethodsSkill]¶

executable_skills() -> list[FormalMethodsSkill]¶

get(slug: str) -> FormalMethodsSkill | None¶

Functions¶

applied_agentic_patterns() -> list[dict[str, Any]]¶

Return compact metadata for formal_methods-applied vendored patterns.

dpll_solve(formula: str, extra_vars: set[str] | None = None) -> dict[str, bool] | None¶

DPLL SAT solver for simple propositional formulas.

get_skill_catalog() -> FormalMethodsSkillCatalog¶

solver_support_matrix() -> dict[str, dict[str, Any]]¶

Return honest availability/version metadata for supported solvers.

MCP Tools¶