⚠️ Without Guardrail (Buggy LLM)
Agent hallucinates test completion & attempts illegal deployment.
--- 🧠 NODE: PLAN ---
[TLA+] Verification PASS. Safe to proceed to 'plan'.
--- 💻 NODE: CODE ---
[TLA+] Verification PASS. Safe to proceed to 'code'.
🔧 Tool: run_terminal -> pip install fastapi
🔧 Tool: edit_file -> main.py
--- 🧪 NODE: TEST ---
[TLA+] Verifying state transition...
⚠️ BUGGY LLM BEHAVIOR: Hallucinating test completion.
--- 🚀 NODE: DEPLOY ---
[TLA+] Verifying state transition to pc='deploy'...
❌ ========================================= ❌
🚨 TLA+ INVARIANT VIOLATION DETECTED 🚨
❌ ========================================= ❌
FATAL ERROR: Invariant Violation: NoDeployUntested!
Cannot safely transition to 'deploy' without a 'test_report' artifact.
Execution was halted BEFORE illegal transition.
✅ With Guardrail (Formal Math)
Mathematical verification over agent state spaces.
--- 🧠 NODE: PLAN ---
[TLA+] Verification PASS.
--- 💻 NODE: CODE ---
[TLA+] Verification PASS.
🔧 Tool: edit_file -> main.py
--- 🧪 NODE: TEST ---
[TLA+] Verification PASS.
🔧 Tool: browser_test -> visiting http://localhost:8000/todos
📝 Artifact test_report created.
--- 🚀 NODE: DEPLOY ---
[TLA+] Verifying state transition to pc='deploy'...
[TLA+] Verification PASS. Safe to proceed.
✅ ========================================= ✅
RUN COMPLETE (All invariants passed)
✅ ========================================= ✅
📂 Workspace Files Created/Modified:
- main.py (137 bytes)