Skip to content

Phase 6: Advanced Differential Testing #29

@quinn-dougherty

Description

@quinn-dougherty

Phase 6: Advanced Differential Testing

Run flagged candidates through multiple independent verification backends. Any disagreement between backends is a bug.

Status: ~25% (comparator in generator, not in scaffold)

Already done:

  • #print axioms soundness_check — verify no sorryAx, no unexpected axioms (in oracle)
  • comparator integrated in generator/src/bin/main.rs
  • ✅ Comparator binary path configured in .env
  • ✅ Comparator config in template/comparator_config.json
  • lean4export binary path configured in .env

Ref: docs/design-plan.md Phase 6


Additional checks for flagged candidates

  • lean4export → examine the exported declaration (path configured in .env, not wired into pipeline)
  • safeverify → independent re-verification
  • lean4lean → pure Lean kernel reimplementation check

Differential testing for NON-golden-signal cases

Even when the golden suffix fails, differential testing is valuable:

  • Run the prefix through Lean at --trust=0 and --trust=1
  • Export and re-import declarations
  • If any backend disagrees, flag it (maybe not soundness, but still interesting)

Integration gaps

  • Wire comparator into scaffold pipeline (currently only generator uses it)
  • Wire lean4export into pipeline (not called anywhere currently)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions