Six-stage workflow: codebase ingestion (AST as facts), goal translation
(LLM, 10%), Screamer constraint satisfaction (80%), ACL2 plan verification,
incremental execution with Merkle snapshots per step and rollback on test
failure, final re-verification.
Key limit: ACL2 cannot prove semantic equivalence of arbitrary programs.
Gap filled by: tests as empirical verification, API contract checking
(structural equivalence of public interfaces), human review with full
provenance of semantic changes.
Comparison with Claude Code: Passepartout trades higher up-front planning
overhead for zero-token constraint checks, ACL2-verified scope control,
instant per-step rollback, and a Merkle chain from before to after.
852fcae4a6