{"_id":"@nahisaho/musubix-formal-verify","_rev":"28-343bed9241046b465f90fed9f2138e2b","name":"@nahisaho/musubix-formal-verify","dist-tags":{"latest":"3.8.2"},"versions":{"1.7.5":{"name":"@nahisaho/musubix-formal-verify","version":"1.7.5","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@1.7.5","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"77f35535179c424df889321b3c9ee85e0c0c8e77","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-1.7.5.tgz","fileCount":78,"integrity":"sha512-EJCk94Ge+BcxUfQdLg4PM8aD4Yx7XO+WHDJn0YbBg2AFmwadQf104IAECgiS7TiHfqdsEyLm4AqZk0fvaGS+Hw==","signatures":[{"sig":"MEQCIDD7PntBZtzkjCUYWti9pTNUjMrj11QrDuvFf7s+Rsi6AiA/EyPc9GeoE1h4eeJ+MTBznMm8i5xz+QGo3rSaGowzjQ==","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223054},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"8b7ee467be0b91be20c3fb8752aa37a8695bb615","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^2.0.0","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^1.7.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_1.7.5_1767665433908_0.840466224755698","host":"s3://npm-registry-packages-npm-production"}},"1.8.0":{"name":"@nahisaho/musubix-formal-verify","version":"1.8.0","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@1.8.0","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"aaca42b28ea00c0c013393eee84c46a4582a40ce","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-1.8.0.tgz","fileCount":78,"integrity":"sha512-x45BQ4CnidCtGXwf0AnEg5EnILwi8ErYKMMkM51QSLKniq2mCmzu117cHMaQKUnL6WWg5XzJMf3SR5ZVenDKNg==","signatures":[{"sig":"MEYCIQCRUn2E8IRuHFAGAQ/dAr7u38A0MZ8+k09vY40y5jIBegIhAOYDiMGk42SuqVv25A+aPRv7JJbnZqjqdv7GaR4WSfBv","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"353fab63ee795db9e5e76bad2ddac9db8af83ad2","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^1.7.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_1.8.0_1767792193476_0.7417574261355124","host":"s3://npm-registry-packages-npm-production"}},"1.8.5":{"name":"@nahisaho/musubix-formal-verify","version":"1.8.5","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@1.8.5","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"bdeb30445a4f7ee1e7b67dbae1b1a072416db505","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-1.8.5.tgz","fileCount":78,"integrity":"sha512-FdrB0eFUOdDK/txt52Qw/gd5wyPaWS/XZ+DmYlSQLNk7ws/xcCDcEEJ2G1I6fFX4SKjFAUyIA6tgjQBggEtWGA==","signatures":[{"sig":"MEUCIQC0REOdIumMx6RnpM5Glq2cj1gpo0vFx7LXGzzZxolFCwIgO5+Y+9IHWwzS5gVBUyQQvXt6tVv8/K5o6jsCBXh5zk4=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"47623f015f937611b979d1fb80f792a3b3dd4a2b","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^1.7.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_1.8.5_1767823111049_0.3458588832511633","host":"s3://npm-registry-packages-npm-production"}},"2.0.0":{"name":"@nahisaho/musubix-formal-verify","version":"2.0.0","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@2.0.0","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"c8b715d03e54354813022beb27b5cc1a1d208db2","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-2.0.0.tgz","fileCount":78,"integrity":"sha512-3D9fiO/MRqbsraxZkSVnqm3SUCF9BNxrBwCvQm8MCPN3BsV46qjrPvJXs/8oHgdsLLY2r2EJFjWRHEi6VkrSzQ==","signatures":[{"sig":"MEYCIQDef7Fm0UTyApgrXPuDGTGaeFKMpnxGwpNGBLGvmmN5ogIhAK8JUhqw1Se/C7FbTB2WXrr+LLKFQALkank+y8rX0qwG","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"e32552d2d16f36f3467d030fb3339d7c1f4a981c","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^1.7.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_2.0.0_1767832485733_0.10863993017318396","host":"s3://npm-registry-packages-npm-production"}},"2.0.1":{"name":"@nahisaho/musubix-formal-verify","version":"2.0.1","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@2.0.1","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"5a7dfd01e8ed0e80e2dd1762197d254d4cec8efd","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-2.0.1.tgz","fileCount":78,"integrity":"sha512-Mk3gZCwX3eYTZHlJ+hzrWUl/yZsIdqBF6qaYrjXnX76/QTMj8gfKkX2js3lgdUa/eN4IhFjGp3dE4PB63KBsfA==","signatures":[{"sig":"MEUCIQCVSLgjlUJIgSbF/rVJnVDBJ4cSndlqdT8WkmSymQ8c5QIgc8eZNEloIcoWmw4qWXLOcfsAKwhIdXm1fA6kJPmbb9U=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"e55a118f5669706318a1852a6b03d932d7c8d8f0","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^2.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_2.0.1_1767852701840_0.420864856262934","host":"s3://npm-registry-packages-npm-production"}},"2.1.0":{"name":"@nahisaho/musubix-formal-verify","version":"2.1.0","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@2.1.0","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"2539fddc0aa3cc4cb165aab9119002b3fee11388","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-2.1.0.tgz","fileCount":78,"integrity":"sha512-E4zxdx60IMC1A6muZDTWecgD1ZiIWaQTOV1AvXNJ28oG/YLqBqiR9yZsdHs/4Lv7PooIOcbcO7GoZVC8rJUXcQ==","signatures":[{"sig":"MEQCIDnHYW5DABGZcrjceJgxvgJv0Kh7AN7UmWcON/W0YcyMAiA0vb+8J9S4iTkxpvS2PsNEpL60Waa5zp1xJXsH1aiyvQ==","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"a1219494d973fa7a8a7fa58dfc1d54b225c03e80","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^2.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_2.1.0_1767866125377_0.03873969171345082","host":"s3://npm-registry-packages-npm-production"}},"2.1.1":{"name":"@nahisaho/musubix-formal-verify","version":"2.1.1","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@2.1.1","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"acb26e1ecaa0c4542b0fa4ca78158928bf79421d","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-2.1.1.tgz","fileCount":78,"integrity":"sha512-08UmyUBMDjdjvhDsX3Oo6pvbZnhTngJxjn4tYX3I4PC1WwcJTGd85LKju8140aVDBe+OrQfFQl8zc+pshwbeuQ==","signatures":[{"sig":"MEUCIB2qUnjrBuZm58pCldgYJnXxRnL1MndkfCCuL2Kp8WFqAiEA17KTh8QhfHWDW07kIxOUy1aWf7O6+ZFo/Dv97BiyWzI=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"759687c4ce70ba22451c22b2fcb486431d1c63e1","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^2.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_2.1.1_1767866636831_0.4766774153508717","host":"s3://npm-registry-packages-npm-production"}},"2.2.0":{"name":"@nahisaho/musubix-formal-verify","version":"2.2.0","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@2.2.0","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"f0816f8bb942cbf9cecef62de55ca5c40b051c6f","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-2.2.0.tgz","fileCount":78,"integrity":"sha512-rjxfDY2O8yjepOaXpMN+vdqHWpPuOYDmrfzWyZ6pw/W9au6GPZJ1wWadCFgPzvmGRWK2Ru8eTkQRATyYCI0e6g==","signatures":[{"sig":"MEYCIQD2ZtSTynUmzzWC/kgId+zCjAI8EelIaKA4DHy+39pcBQIhAInMZKKi7OhrMvIITdVeXpPFm0gd/CKYBlIjj8cMCGB5","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"2fc684786635c247f5541e29e735102075a02440","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^2.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_2.2.0_1767879507825_0.3720528642675387","host":"s3://npm-registry-packages-npm-production"}},"2.3.6":{"name":"@nahisaho/musubix-formal-verify","version":"2.3.6","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@2.3.6","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"6963e915172024273dfe28a78cd6a7e940fd26f4","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-2.3.6.tgz","fileCount":78,"integrity":"sha512-rjnGoZge0XPehcT6ghmdylb7lk1yoqSC4QIzTLxvTsHee1Dm1J1hcJYjvyxb2NdCqc4yyjFXU8SOo/iy8oFyZA==","signatures":[{"sig":"MEUCIQDBOqtWjDzCWRqBkpB4xWXTMzfm1ICUGe1uGH1bz6KXfwIgNIsmgbEOPFuQL0NGdew9gh8nXy58dWj+XzAES5IdexI=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"f6a7bca04f100cd3489580b9df8562b84ab98889","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^2.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_2.3.6_1768010964492_0.35765098729232103","host":"s3://npm-registry-packages-npm-production"}},"2.4.1":{"name":"@nahisaho/musubix-formal-verify","version":"2.4.1","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@2.4.1","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"3d6ee874209ba38ec657423465c8aa6e23681b18","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-2.4.1.tgz","fileCount":78,"integrity":"sha512-gUslvBL72gUfbzxs08B8tviDHCXke/D+SpigtsO1U4XC68QxF9xKc+QBJoniIxwcnaTzzFEeVX0aaXXMAUAMkQ==","signatures":[{"sig":"MEQCIAX3pZtLfeOQ2q2RswT3VBaCVSjADHlYAzxs3RjIzBqeAiAp25yQTI+Y1opqpU9PS4T1gFRpVRsLfXnzocW0IumoFA==","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"8fde732131b688f1eb7dd10ab2a2d8932ed20510","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^2.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_2.4.1_1768093459912_0.7280172334062884","host":"s3://npm-registry-packages-npm-production"}},"2.4.2":{"name":"@nahisaho/musubix-formal-verify","version":"2.4.2","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@2.4.2","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"dd45772546169a90a46551ae42cb23c947ca45ce","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-2.4.2.tgz","fileCount":78,"integrity":"sha512-UffuCzBeQ+ALhwHdqX0DJLSgHIHLSDD0wNMcGdmIDuAg+84G7exTdcHanC2z1s61l1wJoYT0VRyi7bPoWXuf/A==","signatures":[{"sig":"MEUCIQDXTgnaziLvzjE9DqxT2Ot6v2dC21Wn7nOT7fndC+E5pgIgRGwh3wE6ZEzUHj5hZj1gTXB65LrjRN7R5oo2Z8Qc1yE=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"8fde732131b688f1eb7dd10ab2a2d8932ed20510","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"deprecated":"This version has security vulnerabilities. Please upgrade to 3.x","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^2.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_2.4.2_1768093532341_0.7741185718621482","host":"s3://npm-registry-packages-npm-production"}},"3.0.7":{"name":"@nahisaho/musubix-formal-verify","version":"3.0.7","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.0.7","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"7a5d0979f81001a8d07f50b57f7883ada863250a","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.0.7.tgz","fileCount":78,"integrity":"sha512-eE1WgvxEB2F4ezhNtj1aVo3cIEMlMGVRf+VXvExBNgCeIZ2/4fsHt/DTCiD9RsMcjNR27qiQcBwodIJaQFbjXA==","signatures":[{"sig":"MEUCIQCEi52PmCfpj8nikEIjbQ8rx4KjLsWqdB9Rn4N8/pXIpQIgLg3su6NSyRKZkZsj+JAelFUSolNtHNjoQV5/WJJawoo=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"b7fa2f0f8838a1d91a87adb9351ccb31bd182d4b","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.0.7_1768167834042_0.05318510122375519","host":"s3://npm-registry-packages-npm-production"}},"3.0.13":{"name":"@nahisaho/musubix-formal-verify","version":"3.0.13","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.0.13","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"ccb6ab426edfc23f11326fcd149e40908a9d8186","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.0.13.tgz","fileCount":78,"integrity":"sha512-Ac4WrEpgYhdq8tEHB5rF+Z0UW2gYdzIY37aM7cS2pMrsPzz3k7uknWTQxwVyDdWSDHwo6pdqsYzTbU3k6dkr9w==","signatures":[{"sig":"MEUCIDEZOMvCWy7t3TZ3LBu9zBH6BnxpKxQvq/8hP36fVTZnAiEA9ceVYh1Jwbfbu06zkY0NJ1IBvgu4NsgPa+ebZqihY/U=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223056},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"e4ab8d4841e3adf37d61c9183fe181e13503d617","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.0.13_1768257380233_0.9165297757505473","host":"s3://npm-registry-packages-npm-production"}},"3.0.14":{"name":"@nahisaho/musubix-formal-verify","version":"3.0.14","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.0.14","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"068cba4e06cc685f60a1cf27808a9732572b4c60","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.0.14.tgz","fileCount":78,"integrity":"sha512-BxfYEWRVycXTt12BW3SS8iLrANhVXcWBuhtuKWYO0OB0QqtDQfSE7M849ZCw0YJ/iHTuOex67WLMrrkhUdEbsQ==","signatures":[{"sig":"MEUCIDj2C70x4SOkSDSwYZR1MBJzoLkzWYRoD3A7GBHJ6kGBAiEAuW1pRLsdpczn/s+7sK/uAf0WlkGqpM0Iu3/SmJdC0QM=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223056},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"e4ab8d4841e3adf37d61c9183fe181e13503d617","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.0.14_1768257419732_0.9820937233632123","host":"s3://npm-registry-packages-npm-production"}},"3.0.15":{"name":"@nahisaho/musubix-formal-verify","version":"3.0.15","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.0.15","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"5fd87c86921b2378661306c4f4d546d60cef72af","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.0.15.tgz","fileCount":78,"integrity":"sha512-np/wsUybIuImTR5dHnTJXs1cH3tCu8CW0yv7WPlWJFvoQXQSP+zH+cMkD/azBbC0EO3TvB6tfZShISXSyoxyXg==","signatures":[{"sig":"MEUCIHX5VmMLjod53MPSEcJEZfVTUu826SD2W0WhZYYg0ewMAiEA5t8xXd5e1OFV9ZIbP2v124bFFw4D79Ya/TEZv0w1G0k=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223056},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"e4ab8d4841e3adf37d61c9183fe181e13503d617","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.0.15_1768257494564_0.7945261568670636","host":"s3://npm-registry-packages-npm-production"}},"3.0.16":{"name":"@nahisaho/musubix-formal-verify","version":"3.0.16","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.0.16","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"85315b6fb67bed6e20bc7db2c279292fd5a93a6f","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.0.16.tgz","fileCount":78,"integrity":"sha512-oxx4NrZJfKC+g8+aaTuDDh96Qb/um48SlCZrMZH2/MOqIBY6imtAYz/zzfsseYyQ7zxZAZNbJrMwIEKcBrUW+Q==","signatures":[{"sig":"MEYCIQCv1S0cT+beGxzPwVSWpMybQGUFEi1yKjUvN/5VXR7EKgIhAPQIWnOxm98exjZht1b69SYtSVkouk6R29PSOzgSuRD1","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223056},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"c3da5058f6a6c4f6069889ed884207054a0d0386","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.0.16_1768265103246_0.42519429036671785","host":"s3://npm-registry-packages-npm-production"}},"3.0.17":{"name":"@nahisaho/musubix-formal-verify","version":"3.0.17","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.0.17","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"a25ab9ad4b91ff1718c86f7a9e72ee76b3863b7b","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.0.17.tgz","fileCount":78,"integrity":"sha512-s6VVlObGcRBeU5HkAqAXplaQeuDCQoxWvuCrLo4aiUupR77MKBa5ReHJjGYMl52CO4Gd5RzPPInXJC61gaNaRg==","signatures":[{"sig":"MEYCIQDDHJoLcFU3a0aqwYwMDmIBmVTWo7l9+QCWfVgfGeLGgAIhAJcVwwyiFWTTSxkAaYCKoQGbn6yk5sFfukZnDz/L/pAK","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223056},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"d6effc200a8ca65bc390a2940bbbee3beae9d756","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.0.17_1768267750227_0.6791485229380525","host":"s3://npm-registry-packages-npm-production"}},"3.1.0":{"name":"@nahisaho/musubix-formal-verify","version":"3.1.0","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.1.0","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"b081cee57a325d8feac15a2f0ab6d7143ff6b627","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.1.0.tgz","fileCount":78,"integrity":"sha512-GCxxmC5yOcZU6LBmA3Esw9V74/1OkPwLwKb5+qS0JFzdJPOACl6rnglYjznxBUOpWzjYe2Jpi6xKHsecP1q7OQ==","signatures":[{"sig":"MEUCIFsQghOKR831/4u3VOpBr2vS3aizpqtyXPajlzBveFIhAiEAtKKQrbbcpgBkKgw6JSJhNMiLfVQgIn4X5r013lDgq3U=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"bf978d9ed7ce4a79265567771b6e0639c31778cc","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.1.0_1768300133188_0.2832587808389202","host":"s3://npm-registry-packages-npm-production"}},"3.3.1":{"name":"@nahisaho/musubix-formal-verify","version":"3.3.1","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.3.1","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"0f83c0d8903d538611d9e92d05d24805ec515b97","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.3.1.tgz","fileCount":78,"integrity":"sha512-jQmCbDY8nQYnooRWDLQpTtOxeqdOeSHUhr/xxFexFbPT5s94tMGUkBM3JyYLJQaO+CKjeiElq7lJoIk2yEqmGA==","signatures":[{"sig":"MEYCIQCq9PZEGFEng6IW6hXRDJsypyh4NyoWKoAAm2Ld26PFQQIhAL6S+gEKWG2ybqbeESrgiApLxdyoy/N9uFZfbKnP4ALv","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"154d2aaea132b07ca9fedfc015caac8088e5ccf7","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.3.1_1768336093287_0.2192204190927094","host":"s3://npm-registry-packages-npm-production"}},"3.4.2":{"name":"@nahisaho/musubix-formal-verify","version":"3.4.2","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.4.2","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"a57a97885dbb193ac3d91b0fd8f7105c571ef5fd","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.4.2.tgz","fileCount":78,"integrity":"sha512-c9imSdXKTOvVFBwV6L0Om39n+5y38A/0MWH+xowQEXtiM4cnTcNJymhzXZRum19eVKVfJEiUyX3Eb478w3XmWA==","signatures":[{"sig":"MEYCIQDpT4smL8002SXAJzMVfbWUElovkxSbQwjIfFZYkJrgEQIhAJzonOIfXLzoDIRjcrSeBDF3R25M+l2pTEWd95u2pn81","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"90be7dd55d6f4bd22c426a9bcf358c93586d92c2","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.4.2_1768536443987_0.3178305972539708","host":"s3://npm-registry-packages-npm-production"}},"3.4.3":{"name":"@nahisaho/musubix-formal-verify","version":"3.4.3","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.4.3","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"f6f99ce07aa0ce01e0ed085945acf3cd5ea9cdac","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.4.3.tgz","fileCount":78,"integrity":"sha512-ezjyV9eiEmskFTXT4sT0PthxjTBfYsmu7O6zgn/HtIrjkYP61pB98plJOo9A3oECg822LWRFeQlb823zM+obdg==","signatures":[{"sig":"MEQCIFykbPaPPF3PzSgNR8Yjhi34f8NIyOFoWEyL9MsmWKg1AiAGn2/yRnEdwwZmdFU7waGVhLBMytvM55vsbhB7zlTTbA==","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"90be7dd55d6f4bd22c426a9bcf358c93586d92c2","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.4.3_1768546477091_0.034334185639633086","host":"s3://npm-registry-packages-npm-production"}},"3.4.5":{"name":"@nahisaho/musubix-formal-verify","version":"3.4.5","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.4.5","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"347eb021d7938dc4c84393d79d9f2cba9c634d40","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.4.5.tgz","fileCount":78,"integrity":"sha512-Toy+WQcGJln1MgrIiQUmHBiZlDugXdB/Dgh9W9chBLdXOOaAriGkSZXqjO/XfJ/3uESl3LHzxfxZr8VEUs8QEA==","signatures":[{"sig":"MEUCIDv/a0go9TynjyN4FgdTYHfZoJlNjI/fc6mbR6G+aJqIAiEA/tQKuuK3HJjk8awBqAFYdoyAZwTPf+uwzb406Qklm10=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"90be7dd55d6f4bd22c426a9bcf358c93586d92c2","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.4.5_1768646796888_0.004479377014299457","host":"s3://npm-registry-packages-npm-production"}},"3.6.0":{"name":"@nahisaho/musubix-formal-verify","version":"3.6.0","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.6.0","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"e56bb66efe4a5e0472542c99b83aa540a3ad00ef","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.6.0.tgz","fileCount":78,"integrity":"sha512-zzTh/CKzNMUoK51Trde84wGPjjPunuj4+tsplt6f5Ft04LD/dMV3WWVxXSMU+ZweTmwayDzkzCN2apKArPwN0Q==","signatures":[{"sig":"MEUCIFciT6TAGVIf0BGNrJhZTgLIZbmeWjUVoHFAfMZV6KgMAiEAyeYm/7IsvqWYCUPnupdYdL3izvkQXg4RKE4PbvCQ7T0=","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"624b9e522be6e322cdb43993874e345507df085d","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.6.0_1769143831128_0.653764628262715","host":"s3://npm-registry-packages-npm-production"}},"3.7.3":{"name":"@nahisaho/musubix-formal-verify","version":"3.7.3","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.7.3","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"92d32d7bbeb4261955d127236700c4c381b76884","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.7.3.tgz","fileCount":79,"integrity":"sha512-OpjL0qQDnyMxRCp9gkijG+W05B693cukVAOSpxLgnLVuXYQLbFYtgBDLPDtBNc4IuNim+hoteZGHtNAfBtDL8Q==","signatures":[{"sig":"MEQCIAFx2R8aQ0v0r+YINMbPecdvY5mCTtT79+1Y58tfjl/TAiB19s36qv5MUXwjFGtwJXRcnxdqtBUcUybw5H4td+3+Ag==","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":224080},"main":"dist/index.js","type":"module","_from":"file:nahisaho-musubix-formal-verify-3.7.3.tgz","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"_resolved":"/tmp/d591a365c987150afc0af1fc8248def9/nahisaho-musubix-formal-verify-3.7.3.tgz","_integrity":"sha512-OpjL0qQDnyMxRCp9gkijG+W05B693cukVAOSpxLgnLVuXYQLbFYtgBDLPDtBNc4IuNim+hoteZGHtNAfBtDL8Q==","repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.7.3_1769329080965_0.5350741133317543","host":"s3://npm-registry-packages-npm-production"}},"3.8.0":{"name":"@nahisaho/musubix-formal-verify","version":"3.8.0","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.8.0","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"32e9942be718000882a41a2888e9695be8cd1663","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.8.0.tgz","fileCount":78,"integrity":"sha512-nFUw8Gbn/FEx1Rsc+RTR8qnTj7hvB6ipjCndcKSHEBzDkLlBUXW2ubFe+4AI25+H+drzrYVL3gwIzhNI02+4yQ==","signatures":[{"sig":"MEYCIQC2e+i1UAqnZEJvPfsqx0Ur1Z/XSy8TfA1PKzA4MYjCdwIhALsKJPoKInTtZl05hXEc+Hhjd7FJtjgG7kc4SQWfHdv+","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"72b28164390da9a47dcb99036bdb30414c40938c","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.8.0_1770557590741_0.9840613973552697","host":"s3://npm-registry-packages-npm-production"}},"3.8.1":{"name":"@nahisaho/musubix-formal-verify","version":"3.8.1","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","_id":"@nahisaho/musubix-formal-verify@3.8.1","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"dist":{"shasum":"a81a865f6ac295a747e15cffcb1d0c40aa99c6c3","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.8.1.tgz","fileCount":78,"integrity":"sha512-elLGAN0IxbEPkA37h/niWjEzzO9wBJnYjwU4c9kpdM624TnMm8VIQGk6gN30oDPN2VclWikPGaeY21F/flWv7g==","signatures":[{"sig":"MEYCIQCnn3y1A0EojOZGm2YKKiKGvb400gN3mIeckN+ykNYzxAIhAKY291Lw7TPc3INcPopw3syzIS1yid5Vph1ND5nLz7BB","keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U"}],"unpackedSize":223055},"main":"dist/index.js","type":"module","types":"dist/index.d.ts","engines":{"node":">=20.0.0"},"exports":{".":{"types":"./dist/index.d.ts","import":"./dist/index.js"},"./z3":{"types":"./dist/z3/index.d.ts","import":"./dist/z3/index.js"},"./verifiers":{"types":"./dist/verifiers/index.d.ts","import":"./dist/verifiers/index.js"},"./converters":{"types":"./dist/converters/index.d.ts","import":"./dist/converters/index.js"},"./traceability":{"types":"./dist/traceability/index.d.ts","import":"./dist/traceability/index.js"}},"gitHead":"997436a73249efcef43011816e3fe89024d02bf3","scripts":{"test":"vitest run","build":"tsc","clean":"rm -rf dist","typecheck":"tsc --noEmit","test:watch":"vitest","test:coverage":"vitest run --coverage","prepublishOnly":"npm run build"},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"repository":{"url":"git+https://github.com/nahisaho/MUSUBIX.git","type":"git","directory":"packages/formal-verify"},"_npmVersion":"11.6.4","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","directories":{},"_nodeVersion":"22.21.1","dependencies":{"better-sqlite3":"^11.0.0"},"_hasShrinkwrap":false,"devDependencies":{"vitest":"^4.0.16","typescript":"^5.3.0","@types/node":"^20.10.0","@types/better-sqlite3":"^7.6.11"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"_npmOperationalInternal":{"tmp":"tmp/musubix-formal-verify_3.8.1_1770559388076_0.11676852885442845","host":"s3://npm-registry-packages-npm-production"}},"3.8.2":{"name":"@nahisaho/musubix-formal-verify","version":"3.8.2","description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","type":"module","main":"dist/index.js","types":"dist/index.d.ts","exports":{".":{"import":"./dist/index.js","types":"./dist/index.d.ts"},"./z3":{"import":"./dist/z3/index.js","types":"./dist/z3/index.d.ts"},"./verifiers":{"import":"./dist/verifiers/index.js","types":"./dist/verifiers/index.d.ts"},"./converters":{"import":"./dist/converters/index.js","types":"./dist/converters/index.d.ts"},"./traceability":{"import":"./dist/traceability/index.js","types":"./dist/traceability/index.d.ts"}},"scripts":{"build":"tsc","test":"vitest run","test:watch":"vitest","test:coverage":"vitest run --coverage","typecheck":"tsc --noEmit","clean":"rm -rf dist","prepublishOnly":"npm run build"},"keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"author":{"name":"nahisaho"},"license":"MIT","repository":{"type":"git","url":"git+https://github.com/nahisaho/MUSUBIX.git","directory":"packages/formal-verify"},"bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","engines":{"node":">=20.0.0"},"dependencies":{"better-sqlite3":"^11.0.0"},"devDependencies":{"@types/better-sqlite3":"^7.6.11","@types/node":"^20.10.0","typescript":"^5.3.0","vitest":"^4.0.16"},"peerDependencies":{"@nahisaho/musubix-core":"^3.0.0"},"gitHead":"bd446d09f48578878962c09b99260494db3499b1","_id":"@nahisaho/musubix-formal-verify@3.8.2","_nodeVersion":"22.21.1","_npmVersion":"11.6.4","dist":{"integrity":"sha512-BCi1i8UTn5zbc1Hgna3AVs5DZiw0Lvyj1VMkck7JA/GL90TkR4X2d5iGgUuZGnPnpUS8GF1tUFehfjZWmLWrDQ==","shasum":"597e3f9f3bc20a967ad4a82cf6ca9ae7b94dd8b7","tarball":"https://registry.npmjs.org/@nahisaho/musubix-formal-verify/-/musubix-formal-verify-3.8.2.tgz","fileCount":78,"unpackedSize":223055,"signatures":[{"keyid":"SHA256:DhQ8wR5APBvFHLF/+Tc+AYvPOdTpcIDqOhxsBHRwC7U","sig":"MEUCICZxbtB4bz8qLygh8+Ad+xsYf9fWnvbRhWUNcpKMFikrAiEA6ISnM3R0zdVq/nMGHXoYcZtEWziV40HhOyfeXwqKWzI="}]},"_npmUser":{"name":"nahisaho","email":"nahisaho@microsoft.com"},"directories":{},"maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"_npmOperationalInternal":{"host":"s3://npm-registry-packages-npm-production","tmp":"tmp/musubix-formal-verify_3.8.2_1770559922872_0.6143415842619369"},"_hasShrinkwrap":false}},"time":{"created":"2026-01-06T02:10:33.787Z","modified":"2026-02-08T14:12:03.155Z","1.7.5":"2026-01-06T02:10:34.093Z","1.8.0":"2026-01-07T13:23:13.631Z","1.8.5":"2026-01-07T21:58:31.242Z","2.0.0":"2026-01-08T00:34:45.885Z","2.0.1":"2026-01-08T06:11:41.974Z","2.1.0":"2026-01-08T09:55:25.531Z","2.1.1":"2026-01-08T10:03:56.981Z","2.2.0":"2026-01-08T13:38:27.982Z","2.3.6":"2026-01-10T02:09:24.653Z","2.4.1":"2026-01-11T01:04:20.074Z","2.4.2":"2026-01-11T01:05:32.503Z","3.0.7":"2026-01-11T21:43:54.193Z","3.0.13":"2026-01-12T22:36:20.383Z","3.0.14":"2026-01-12T22:36:59.884Z","3.0.15":"2026-01-12T22:38:14.722Z","3.0.16":"2026-01-13T00:45:03.394Z","3.0.17":"2026-01-13T01:29:10.377Z","3.1.0":"2026-01-13T10:28:53.342Z","3.3.1":"2026-01-13T20:28:13.424Z","3.4.2":"2026-01-16T04:07:24.143Z","3.4.3":"2026-01-16T06:54:37.238Z","3.4.5":"2026-01-17T10:46:37.026Z","3.6.0":"2026-01-23T04:50:31.288Z","3.7.3":"2026-01-25T08:18:01.117Z","3.8.0":"2026-02-08T13:33:10.909Z","3.8.1":"2026-02-08T14:03:08.243Z","3.8.2":"2026-02-08T14:12:03.049Z"},"bugs":{"url":"https://github.com/nahisaho/MUSUBIX/issues"},"author":{"name":"nahisaho"},"license":"MIT","homepage":"https://github.com/nahisaho/MUSUBIX/tree/main/packages/formal-verify#readme","keywords":["musubix","formal-verification","z3","smt","ears","precondition","postcondition","traceability"],"repository":{"type":"git","url":"git+https://github.com/nahisaho/MUSUBIX.git","directory":"packages/formal-verify"},"description":"Formal verification tools for MUSUBIX - Z3 integration, precondition/postcondition verification, and EARS-to-SMT conversion","maintainers":[{"name":"nahisaho","email":"nahisaho@microsoft.com"}],"readme":"# @nahisaho/musubix-formal-verify\n\nMUSUBIX v1.7.5 Formal Verification Edition - 形式検証ツールパッケージ\n\n## 概要\n\nZ3ソルバー統合、事前条件/事後条件検証、EARS→SMT変換、トレーサビリティDBを提供します。\n\n## インストール\n\n```bash\nnpm install @nahisaho/musubix-formal-verify\n```\n\n## 機能\n\n### Z3統合\n\n```typescript\nimport { Z3Adapter } from '@nahisaho/musubix-formal-verify/z3';\n\nconst z3 = await Z3Adapter.create();\nconst result = await z3.checkSat('(declare-const x Int) (assert (> x 0))');\nconsole.log(result); // 'sat' | 'unsat' | 'unknown'\n```\n\n### 事前条件/事後条件検証\n\n```typescript\nimport { PreconditionVerifier, PostconditionVerifier } from '@nahisaho/musubix-formal-verify/verifiers';\n\nconst preVerifier = new PreconditionVerifier(z3);\nconst result = await preVerifier.verify({\n  condition: 'amount > 0 && amount <= balance',\n  variables: { amount: 'Int', balance: 'Int' }\n});\n```\n\n### EARS→SMT変換\n\n```typescript\nimport { EarsToSmtConverter } from '@nahisaho/musubix-formal-verify/converters';\n\nconst converter = new EarsToSmtConverter();\nconst smt = converter.convert('WHEN user clicks submit, THE system SHALL save the data');\n```\n\n### トレーサビリティDB\n\n```typescript\nimport { TraceabilityDB, ImpactAnalyzer } from '@nahisaho/musubix-formal-verify/traceability';\n\nconst db = new TraceabilityDB('./trace.db');\nawait db.addLink({ source: 'REQ-001', target: 'DES-001', type: 'implements' });\n\nconst analyzer = new ImpactAnalyzer(db);\nconst impact = await analyzer.analyze('REQ-001');\n```\n\n## ライセンス\n\nMIT\n","readmeFilename":"README.md"}