Skip to content

AGENTS.md

Latest commit

 

History

History
82 lines (60 loc) · 4.71 KB

AGENTS.md

File metadata and controls

82 lines (60 loc) · 4.71 KB
Raw

Agent Instructions: MathTrace Development

This document governs coding agents working on MathTrace.

1. What MathTrace Is

MathTrace is an AI-powered mathematical problem-solving workflow and formal verification runtime. It features an append-only state ledger, scoped inference and cycle-free witness evaluation, nonparty challenge adjudication, Lean 4 proof verification with optional sandbox isolation, adaptive coordination frontiers, and an advisory learning layer.

Repository Layout

  • mathtrace/: Authoritative Python runtime, CLI commands, and Lean semantic inspector.
  • tests/: Deterministic regression test suite (313 tests).
  • tools/: Reusable validation, native installer, and toolchain setup utilities.
  • docs/: Operational documentation, workspace navigation guide, and architectural decisions.
  • openspec/: OpenSpec capability specifications (specs/), change proposals (changes/), and configuration (config.yaml).
  • .agents/: Generated native agent projection (roles, protocol, skills) and installed OpenSpec workflow skills.
  • .math/: Runtime campaign state (created per mathematical research campaign).
  • work/: Retained validation runs, toolchains, archives, and historical provenance.

2. Change Management via OpenSpec

OpenSpec is the sole development and change-management system for MathTrace. Do not establish alternative planning systems, custom schemas, or ad-hoc task trackers.

Standard OpenSpec Workflow

All substantive enhancements, bug fixes, and architectural adjustments follow standard OpenSpec practices:

  1. Propose: Create a change with openspec new change <name> or use the openspec-propose skill.
  2. Specify: Author or modify requirements in the change's delta specs (specs/<capability>/spec.md) conforming to OpenSpec schema.
  3. Design & Tasks: Detail the design decisions and break implementation into verifiable tasks (tasks.md).
  4. Implement: Apply code and test changes (openspec-apply-change skill).
  5. Verify: Ensure the test suite passes (pytest tests), package builds cleanly (python tools/validate_package.py), and specs validate (openspec validate --all).
  6. Archive: Sync delta specs to main specs and archive the change (openspec-archive-change skill or openspec archive <name>).

Specification Authority

The authoritative specifications of verified system behavior live under:

openspec/specs/

Always check existing specifications before modifying runtime capabilities.

3. Core Architectural Invariants

Agents modifying MathTrace must strictly preserve the following invariants:

  1. State Immutability: All campaign data resides in transactional SQLite with append-only events. Projections are dynamically derived; historical events are never mutated in place. State integrity is verified via SHA-256 state digests.
  2. Formal Checking Integrity: Formal verification requires pinned Lean 4 fresh-context checked-target replay, retained compiled semantic evidence and independent target-fidelity review. Direct Execution is the default; explicitly selected Bubblewrap retains its original isolation requirements. Standalone checks retain leanchecker --fresh. Never fabricate sandbox attestation or source-to-object correspondence; preserve historical protocols and all mathematical gates.
  3. Sound Scoped Evaluation: Support and refutation propagation use conservative antitone bounds and selected witness forests (scoped-selected-forest-v3). Circular reasoning is detected and rejected.
  4. Independent Nonparty Adjudication: Objections, counterexamples, and findings require independent nonparty adjudication. Historical audit witnesses cannot be silently substituted under old certificates.
  5. Advisory Boundary: Advisory heuristics and research lessons are curated against immutable event lineage and must never become mathematical dependencies in proof trees or audit gates.
  6. Native Isolation & Preservation: Roles in .agents/ are managed via mathtrace.native and generated by tools/install_native.py. The installer strictly preserves external assets, including OpenSpec skills and workflows.
  7. Model & Effort Inheritance: Autonomous subagents inherit the parent agent's foundation model and reasoning effort settings by default; automatic model routing or degradation is prohibited.

4. Verification and Developer Commands

Run from the repository root:

  • Run Test Suite: 
    python -m pytest tests
  • Validate OpenSpec Specs and Changes: 
    openspec validate --all
  • Verify Package Build and CLI Identity: 
    python tools/validate_package.py
  • Update Native Projection: 
    python tools/install_native.py