Per OQ-001's resolution (#56), verification/proofs/ is the canonical content of this repo's "verification host" role — but no CI workflow runs it, so the proofs are asserted, not enforced (the just proof-check-all recipe exists but is never invoked by CI).
Add a proof-CI job that builds each prover layer:
- idris2 —
verification/proofs/idris2/** (via just proof-check-idris2)
- agda — needs Agda 2.6.3+ + stdlib 2.3 and echo-types registered as an Agda library (
EchoTyping.agda/Verification.agda depend on it); see echo-types' own CI for the stdlib-2.3-from-source pattern
- lean4 —
ApiTypes.lean
- coq —
TypeSafety.v
- (optional) tlc —
StateMachine.tla
SHA-pin the setup actions. This makes the coordinator's verification-host identity enforced rather than asserted, and is the natural next step after the OQ-001 cleanup.
https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ
Per OQ-001's resolution (#56),
verification/proofs/is the canonical content of this repo's "verification host" role — but no CI workflow runs it, so the proofs are asserted, not enforced (thejust proof-check-allrecipe exists but is never invoked by CI).Add a proof-CI job that builds each prover layer:
verification/proofs/idris2/**(viajust proof-check-idris2)EchoTyping.agda/Verification.agdadepend on it); see echo-types' own CI for the stdlib-2.3-from-source patternApiTypes.leanTypeSafety.vStateMachine.tlaSHA-pin the setup actions. This makes the coordinator's verification-host identity enforced rather than asserted, and is the natural next step after the OQ-001 cleanup.
https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ