Aquí hi ha 22 versions de Verifpal, des de 29 d’agost del 2026 fins a l’actual, 1.6.6. Cadascuna enllaça amb els instal·ladors del mateix desenvolupador.
| Versió | Data | Mida | Fitxers |
|---|---|---|---|
| 1.6.6Darrera versió | 11 d’octubre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 9823fcca92a48632e0f2543946420b863f97b7d4: Engine: Additional fixes and regression tests (@nadimkobeissi)
* 7c25b853b984fdd1a8dbd082f6561281dd550567: Expand search coverage, rule out more missed attacks (@nadimkobeissi)
* c626f1bfc171f5a39a88ee366da66a5272b71aec: Fix unlinkability regression reported by Heba Ajjour (@nadimkobeissi)
* 650f258a81d0c9423ef0b5b224ca36059293d9ff: More precise AEAD and forgery semantics (@nadimkobeissi)
* f96ea963f8c5a87140097af0911ebfac2b93ecd1: More precise AEAD and forgery semantics (@nadimkobeissi) |
| 1.6.4 | 7 d’octubre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* ab0b702021d2cacf43003c195d351910c116e310: Cargo update (@nadimkobeissi)
* 9d88b16a93f883bd6cbb59fc78dd9bda47f111a1: Cargo update (@nadimkobeissi)
* e5762e436c918ad679172c39b7c84be7fdb0bda9: Code quality pass (@nadimkobeissi)
* 6acd799fa09412c8fdfeca1a5422e7b8235f9a8e: Deducer: reuse goals whose cycle cuts recur; fail clashing equations early (@nadimkobeissi)
* 67ce38029b08c5adf2aa2aa22f8c67734e2b1adc: Fix #45, #46, #47 (@nadimkobeissi)
* f9dd68c2892549c254ae3169a8891cafde51a46f: Major source refactoring/reorganization (@nadimkobeissi)
* 23a2dd37761fb34f853f32087e32095253af802e: Performance improvements (@nadimkobeissi)
* 5962ede0d8df686223c461725119cfcf7f6d0227: Scenario analysis bug found by Heba Ajjour (@nadimkobeissi)
* 7a308d4329ff6562098c821667cf46d51f580b2f: Search: a rerouted send can supply a stuck receive (@nadimkobeissi)
* 8c568a97074e4c727029fa22d0debb06d0dd6b72: Search: the rerouted pass bypasses the stuck run's own later send (@nadimkobeissi)
* 4ba3d77a8979125bc41b91cafa4ea62a5b045a66: Search: the rerouted pass uses only sends that reach past the wait (@nadimkobeissi)
* 3dc377f1e8f224b782fe3b7dbf533756e6c39bf0: Unlinkability fixes (@nadimkobeissi)
* 0de423362992f32098f9bd5bafde56745dbe1fce: ePassport models (@nadimkobeissi) |
| 1.6.3 | 28 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* e2ae94343429a63d5ebaa65624fe2248d3d37a5d: Eliminate classes of missed attacks (@nadimkobeissi) |
| 1.6.0 | 23 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 34f0c216baba37bef51ae412a97e82eaadb9c9c4: Performance pass with five engine improvements (@nadimkobeissi)
* f025edc4faa8674ca7a3cbbb1bfb6660f0c50834: Replace the gate-based engine with joint execution (@nadimkobeissi)
* 0b0165170ce2e1187fd6703f3e4c134d3820a024: Restore some narrator improvements (@nadimkobeissi)
* 0180a165c4ce16ccee569d79446b59d2b87577e0: Restore some narrator improvements (cont.) (@nadimkobeissi)
* 7e21f4a644c466ebbd8ece75f60ac63787befd3e: Restore some narrator improvements (cont.) (@nadimkobeissi)
* 547b87d0d47f4c43800e4f828edbc2ad893b1a98: Update CLAUDE.md (@nadimkobeissi) |
| 1.5.1 | 21 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 9546906223ac13a700f200cd21ae93f991f35e85: Performance optimization pass (@nadimkobeissi)
* 827c0792e49d72e86a68d92a2e71454a87865d8c: Remove junglegym_threshold_ring.vp (@nadimkobeissi)
* 7259772f508d3c9735b1e2f1ee165f998e31937e: Validate concrete replay witnesses and preserve execution constraints [ci] (@nadimkobeissi) |
| 1.5.0 | 20 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* b9b7964821f2a232b723ef90f0d54e1a3cc3f1d6: Claim a guard was bypassed upstream only where an unguarded hop exists (@nadimkobeissi)
* 50073952948e6536ecdc06548f97ecf3480c117b: Fix four more classes of missed and false attacks, one of them a crash (@nadimkobeissi)
* da733b8f99b821ce1e0bd3da5135586075ed6d00: Fix seven classes of missed and false attacks found by auditing the engine (@nadimkobeissi)
* b579fc2515f55d84738d36a4e2ebd347e424e935: Fix six more classes of missed and false attacks found by auditing the engine (@nadimkobeissi)
* e326cfbd4a3daa4280cc5c8131adf849edd35343: Give every learned value the executions that produce it (@nadimkobeissi)
* fe92adac1acc380490bf5677c707b8667849c281: Judge a query's preconditions in the execution that produced the violation (@nadimkobeissi)
* 8e6287f0c747952ee4f6d5d009d54431721dc924: cargo update (@nadimkobeissi) |
| 1.4.12 | 17 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* b2b4ef2f88481cf3e29b4c1ea490e6ffb89077c4: Fix bug causing missed attack found by Heba Ajjour (@nadimkobeissi)
* 3892b3ca7af9faec0d65fcefc80849fd25925cf5: Remove old references to Verifpal Manual (@nadimkobeissi)
* 57a3f9c05681b7e98c7f41a1d4615306548eb190: Revert "[ci] Verifpal 1.4.12" (@nadimkobeissi)
* e3573cd6bbb3784700d2ad39a029c29560b70560: cargo update (@nadimkobeissi) |
| 1.4.11 | 16 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 21b072896429f7b0e0d656d0398d611d6fcfa0e0: Delete pqxdh-weak.vp example (@nadimkobeissi)
* 1d57833b9b908e1e8fc96a945fca47e500a46fe7: Radically improve PQXDH model (@nadimkobeissi)
* 33d21c35abbfd3006e2f82319105226f1d7d9751: Remove pqxdh from tests (@nadimkobeissi)
* 5f3805f821c06b4817ffb785d77bad0b01c375d2: Update CLAUDE.md (@nadimkobeissi)
* ba04705b683c8345fdd13659742b58191c335e7e: Update Cargo.lock (@nadimkobeissi)
* f21132d06aec762ebfb172c481104d3b39c77e89: Update README.md (@nadimkobeissi)
* 31e39f7ea0b70899897dc0843baac6829abc5c58: completeness: only refuse derivation when no execution produces it (@nadimkobeissi)
* fb9db599cc7dd958eef7c475b140df93ac775d7e: scripts: remove zig dependency (@nadimkobeissi) |
| 1.4.10 | 8 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* dc9c4a9afd3a97b917a667aff757a9e4f0f4e334: Fix imprecision in forgeable threshold signatures relative to RFC 9591 (@nadimkobeissi) |
| 1.4.9 | 8 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* caf0c3f39fbd25414451dbff8da56dc2979ff51c: Finish up performance/completeness pass (@nadimkobeissi)
* 5d0ceff81907680f9ddd951a578a117d437712ea: Fix completeness issue (@nadimkobeissi)
* 5f8818b878bccab579973e90a55a659b18847856: More fixes (@nadimkobeissi)
* 12deaa820ac7ddd86940f78917995ccdd3e7dc87: Update CLAUDE.md (@nadimkobeissi)
* d66bf990c69a5f219cc073afcf5f31a1124a9712: completeness: fix nonce-reuse closure issues (@nadimkobeissi)
* 177f524bb46b1b1ccef2c7247f30c0ed170e88d5: completeness: forgeability/rejected replay fixes (@nadimkobeissi)
* 6a2950588c1b272271e056dd30efb0ee0def841a: completeness: forgeable/malleable fixes (@nadimkobeissi)
* db7f3f863c9093f0202dac22717b5d68f5311c63: completeness: nested reuse fixes (@nadimkobeissi)
* 98f28a282635e3825fcc20908486ce3af7dd0cab: misc: update Cargo.lock (@nadimkobeissi)
* 18fd5fb25c51dec24ebab675f5e9c845ca36b947: performance: reuse existing DAG walker (@nadimkobeissi)
* b6dc00fa3a3c882f59abcd9b131cd541dd749254: performance: reused variable-free subgraphs (@nadimkobeissi) |
| 1.4.8 | 7 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* f109af9dc49e036fafbf5e8e12a80f8fd67527ea: Fix regressions in performance pass, remove final scaffolding (@nadimkobeissi)
* 4a6b6c1705bf7b734a1e2283c99718cfa519a92b: Remove aws_nitro_attestation from tests (@nadimkobeissi)
* d855f7a0e965b92c642cc0bdd87d90b9e42e1a72: Remove perf debugging code (@nadimkobeissi)
* a2190dda629331e2e55d40827c56fcb1c3e77367: Remove perf debugging code (@nadimkobeissi)
* 92881aaf11cd4ae3de5148791a65556be717b0ca: Yes, Mikerah, this *is* the sort of protocol I'd expect Verifpal to be able to analyze (@nadimkobeissi) |
| 1.4.7 | 7 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 9d0468fbf49e06cb68048731c1acb59f3411cd7c: Performance improvements (@nadimkobeissi)
* f9179dce9d70533980710b0d32d11f6fbe1ba626: Performance improvements + fixes (@nadimkobeissi)
* 26c6fb6bec5f7e6a8fc7c1114c270626d278b6f1: Performance improvements + fixes (@nadimkobeissi)
* 949c8d27215fe0155c0faaee2976a26af13988de: Performance improvements + fixes (@nadimkobeissi)
* dc97f887280b6f580a032788e3c113e600b2b616: Performance improvements + fixes (@nadimkobeissi)
* 8b1cf3ce2ca9ac72038a33d38ffbc9d38a3ba285: Performance improvements + fixes (@nadimkobeissi)
* de21a3b3fff896ee7b21f1a7eaf702641bbf7e33: Performance improvements + fixes (@nadimkobeissi)
* 0c305111c114bdc43e7f482ea3b4805004a8416e: Performance improvements + fixes (@nadimkobeissi)
* 9c455db975ae3e33abdee0312ec2b4e58ca6d4cf: Performance optimizations (@nadimkobeissi)
* 875e899b7f5cedeae8c9fea73550336f0cf97220: Performance optimizations (@nadimkobeissi)
* 7a5d5ea0322b8988eb23cd80c6c33425c3a97b91: Performance optimizations (@nadimkobeissi)
* c012d74c90f820f88916c97f68f94b947b9b0bb7: Simplifications (@nadimkobeissi)
* 14ce08467163054bdd78b96eb266f13ae53a464c: Soundness/completeness fixes (@nadimkobeissi) |
| 1.4.6 | 6 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* eaf5e397a9c0744af1945e6357e0da2f79cba6fb: Add SimpleX models (@nadimkobeissi)
* 3169fb9bff9c20eb0172bcd4d7f8490d3ad99378: Fix regression (@nadimkobeissi) |
| 1.4.5 | 6 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* af43ef78bbea0ccf162323704eb0e582a6b901c7: Add regression test (@nadimkobeissi)
* 03882c420e02f2177da8c70e0e502aa3736c751a: Fix regression (@nadimkobeissi)
* 3bd65394ef09155bbd2a6f0ac432ae77cbde1e91: Soundness/completeness fixes + more regression tests (@nadimkobeissi)
* 020800d196aeda14a659ccc3471587e2f89d4223: Soundness/completeness fixes + more regression tests (@nadimkobeissi)
* 907f34bba2d496cb8f38b2f9c85c945dc628ff51: Soundness/completeness fixes + more regression tests (@nadimkobeissi) |
| 1.4.4 | 6 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 486e60c5297337415dee438d6ec1f51b51bf610c: Ensure decomposition consistency (@nadimkobeissi)
* a18b236f9ab103ad74998b982ebacedf82b8b87b: Knowledge-rule saturation (@nadimkobeissi)
* e85a4e00b2be0598412eb20cb076d83fd1de2523: New feature: threshold cryptography modeling support (@nadimkobeissi)
* 314c70323dbe1e8a273765fbbc39ee1c0f16f047: Parallelize proposal generation on a rayon pool that only evaluates (@nadimkobeissi)
* a50cc87c0b38fe46d6d1f478fafb8d9133aa8dc4: Performance optimizations (@nadimkobeissi)
* b8e63a68a941f8b5faf0cb3e3babb2def743d2a5: Soundness/completeness fixes + more regression tests (@nadimkobeissi)
* 08d81e39f96f95898aa3a5c206c405c95d625449: Update CLAUDE.md (@nadimkobeissi)
* fb61b63f8b744e82e03738c0e01eec69100c8e13: Update tls13.vp (@nadimkobeissi) |
| 1.4.3 | 5 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* f141fc17cfac4320607b7e6eda08ec553006816f: AEAD now takes a nonce, allowing modeling of nonce reuse (@nadimkobeissi)
* 657618210e3b55f48ce2fc1d53306eeaf78a9309: Fix the swept-models array length (@nadimkobeissi)
* d9d5d7542b54fed86e4ee4772a7768f4a95de0e3: Fix unlinkability missed attack discovered by Heba Ajjour (@nadimkobeissi)
* a0421578668585a515c909748ddd3c6c5e94432f: Improve TLS 1.3 model (@nadimkobeissi)
* 4af53142ff81d13ba53a472ce52f026347dd7a64: Improve TLS 1.3 model (@nadimkobeissi)
* d6592fca89ac4fad465f5c940e293b4450cfec66: Improve attack traces (@nadimkobeissi)
* 2477067bd6cce150fd8f090c1db29ffab80b6dc0: Improve attack traces (@nadimkobeissi)
* a0d79eb0482dce5df3d5b48f1ad423f7fe1d1b00: Update CLAUDE.md (@nadimkobeissi)
* 9929ed764d05b5fa20c31719bb5c22970ac50a2c: Update CLAUDE.md (@nadimkobeissi)
* f171d1aa0c7ab59a349eaae52f5b16bc2074fe70: verifpal about: move names to Wall of Honor in Verifpal Manual (@nadimkobeissi) |
| 1.4.2 | 4 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 7de9503d5662c47ffe6b175617beb20a927aabc7: Arapinis and Duflot's Pi_Toy! (@nadimkobeissi)
* 3bbbc95a36035b2a7b72badb182bfc7829ba434c: Bug fixes and optimizations (@nadimkobeissi)
* 12a75e7d5c708665b7f3ba8f30efa3f58bbb579a: End support for Intel Macs (@nadimkobeissi)
* 0b1a9d52d37f17734b699a87f386e2ce2f2b8575: Fix many regressions (@nadimkobeissi)
* c79ce5190b9175de5fdf8157fd1dfd0e2144f53e: Fix regressions (@nadimkobeissi)
* b067dc63cffd856cc56c35bd7311583018e29e2a: Further attempts to fix Goreleaser (@nadimkobeissi)
* c747b448f4c5a49497e0d599ea6d0a2a331b6b4b: Goreleaser: try cargo cross (@nadimkobeissi)
* bbc2f6cf3e853a1bf14e371ddbcd3c1701c93cb3: Goreleaser: try cargo cross (@nadimkobeissi)
* 294c68893450af259113416f6482ce61851ec9fe: Greatly improved value tracking (@nadimkobeissi)
* a5bf03be255a25c80dbe9d74815b7614ac6d0f96: Hopefully avoid cargo-zigbuild upstream bug (@nadimkobeissi)
* 5716be5b4e3f52000e1febc648c6f91f9a3b5e19: No more FreeBSD (@nadimkobeissi)
* 54e1aa9b78ad5078b15ad90052f4f2f0d330000f: Remove passwords, PW_HASH (@nadimkobeissi)
* 6162e8db98671bb3dbaa391699f1ea77a73fe621: Remove pin (@nadimkobeissi)
* 2935fd67d059321ec670ca43068f3bf7c674f726: Rework preconditions (@nadimkobeissi)
* 24638bb87b8a526317e611424b6278dd2e9e7240: Update Makefile (@nadimkobeissi)
* 1b87e4abad005835584a2e6ff33da493c5fd8887: Update Makefile (@nadimkobeissi)
* 9b54fd89ece89005fb001f3e7f5b4079b66bd619: WASM: expose subtypes (@nadimkobeissi) |
| 1.4.1 | 3 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 6baaec3b2ac257f6a32679fb2920979b0a1ab4c5: Releaser: pin cargo-zigbuild to avoid upstream bug (@nadimkobeissi)
* 0da9b6ade192422449070ddcbd97fe0cb73d2b59: Stop relying on GitHub Actions for releases (@nadimkobeissi)
* 4d92c4a0f33285a85d051b2ca50991395a3145f6: Temporary downgrade (@nadimkobeissi)
* 9dbfc8e026da31b014d6169ff146df6ddc17dbc2: Update CLAUDE.md (@nadimkobeissi) |
| 1.3.9 | 1 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 32822504cae003ec4250c9e20e37e93fa8820409: Add a few small tests (@nadimkobeissi)
* d4d0bdee99ce4dc437c427a88abc771fb1ef69e9: Add a few small tests all over the place (@nadimkobeissi)
* 3a6dc93299cb57f3023b21ed2307ae11177624ed: Add a few small tests all over the place (@nadimkobeissi)
* 8c278c2830a9d6d3a755b1a9bcef576f29ecbb04: Bug fixes and additional tests (@nadimkobeissi)
* f134e7c9eb2794f76a67c13b4382154d145c25d7: Bug fixes and additional tests (@nadimkobeissi)
* e2608a73fd3e8865d21a6a3a189368d4991b003d: KEM_ENCAP's Decompose rule should also reveal r, not just ss (@nadimkobeissi)
* 52603fc093c42d68a1851c71f1f3326ecce560b2: Remove a couple of sections (@nadimkobeissi)
* 9c8ffcabacfe5498724a81cee85e4b6479bfc72d: Update CLAUDE.md (@nadimkobeissi) |
| 1.3.8 | 1 de setembre del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 36b48f2afe67b64fe77b6fc3957dccff1eccb061: Feature: --format latex (@nadimkobeissi)
* 5fd15e2a8d3cfd1b28234bc32246d1db5484df22: Update Cargo.toml and Cargo.lock (@nadimkobeissi)
* 4fc5b91a8ec383543e3921035606463ca50e55d6: Update GitHub CI workflows (@nadimkobeissi) |
| 1.3.7 | 31 d’agost del 2026 | — | 64 bits ZIP Notes de la versió## Changelog
* 092105cab6a6a7c17c8d7e5635426843b3b0fe0c: Add package name (@nadimkobeissi)
* 75795a9a12212f9afdde7871e351d4d822b8dd51: Better attacker term reconstruction (@nadimkobeissi)
* f57dec65217476b89909d512d471c0f74c7e7fcd: Load VERIFPAL_PUBLISH_WINGET from secrets (@nadimkobeissi)
* b43b20c504e0f3861b09af276c6c4bcf32f5346a: Performance optimizations (@nadimkobeissi)
* 5cf86b76fb85be426c16f6e51fcf3dc76847c5ed: goreleaser: winget token must use the canonical .Env form (@nadimkobeissi)
* b0b67da2c305e9cba539e4cfd434d48ad0e7b153: release: build on macOS, since darwin targets need the Apple SDK (@nadimkobeissi)
* 6c9f4fd7a681f9289ba40da2348096d1d5b1a1eb: release: install zig from PyPI instead of a mirror-backed action (@nadimkobeissi) |
| 1.3.6 | 29 d’agost del 2026 | — | 64 bits ZIP Notes de la versióVerifpal 1.3.6
Changes since v1.3.5:
- Find missed unlinkability attacks
- Improved and expanded Goreleaser configuration
All major changes between Verifpal 1.0.0 and 1.3.6 are covered
in the following blog post:
https://symbolic.software/blog/2026-08-26-verifpal-1-3/ |