feat(verify): Phase 16 LemmaScript -> Dafny+Z3 proofs of unify measure + bindings lookup (machine-checked, 0 errors)

Author: MesTTo

.gitignore

@@ -3,3 +3,8 @@ dist/
 *.tsbuildinfo
 .DS_Store
 zod
+
+# LemmaScript generated artifacts (regenerable via `pnpm verify`)
+verification/*.dfy
+verification/*.dfy.gen
+verification/*.lean

package.json

@@ -14,14 +14,16 @@
     "format": "prettier --write \"packages/*/src/**/*.ts\" \"*.{json,md}\"",
     "format:check": "prettier --check \"packages/*/src/**/*.ts\" \"*.{json,md}\"",
     "oracle": "vitest run packages/core/src/oracle.test.ts",
-    "bench": "pnpm --filter @metta-ts/core build && node packages/node/bench/suite.mjs"
+    "bench": "pnpm --filter @metta-ts/core build && node packages/node/bench/suite.mjs",
+    "verify": "lsc check --backend=dafny verification/clamp.ts verification/terms.ts verification/bindings.ts"
   },
   "devDependencies": {
     "@types/node": "^22.20.0",
     "@vitest/coverage-v8": "^2.1.8",
     "eslint": "^10.5.0",
     "eslint-config-prettier": "^10.1.8",
     "fast-check": "^3.23.1",
+    "lemmascript": "^0.5.7",
     "mitata": "^1.0.34",
     "prettier": "^3.8.4",
     "tsup": "^8.3.5",