Skip to main content

Formal Verification -- Technical Specification

Version: v1.1.9 | Status: Active | Last Updated: March 2026

Functional Requirements​

FR-1: Core Functionality​

  • The module shall provide formal verification capabilities as described in the module docstring.
  • The module shall export 15 public symbols via __all__.

FR-2: MCP Integration​

  • The module shall expose 9 MCP tools for agent consumption.

Interface Contracts​

MCP Tool Signatures​

  • clear_model()
  • add_item()
  • delete_item()
  • replace_item()
  • get_model()
  • solve_model()
  • push()
  • pop()
  • verify_code_change()

Non-Functional Requirements​

NFR-1: Zero-Mock Testing​

  • All tests follow the Zero-Mock policy -- no unittest.mock, MagicMock, or monkeypatch.

NFR-2: Explicit Failure​

  • All failures shall raise exceptions; no silent fallbacks or placeholder returns.