Package: easycrypt Version: 2026.09-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 227374 Depends: why3 Priority: optional Section: misc Filename: pool/main/e/easycrypt/easycrypt_2026.09-1+resolute_amd64.deb Size: 55495974 SHA256: 5486c4d890ff219888c0632a945f596492de0dce1923bf23fad26e530c4f9e3a SHA1: 80af7186d3172ed51b27afb55fafa2715f22cd3b MD5sum: 166f496da6529b22af37cb6d9e40e81e Description: Computer-Aided Cryptographic Proofs EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of code-based, game-playing cryptographic security proofs, but it's capable of more general formal verification tasks. Another important application of EasyCrypt is proving the functional correctness of low-level implementations—particularly those in Jasmin—against high-level specifications. Package: jasmin-compiler Version: 2026.09.0-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 65451 Depends: libapron Priority: optional Section: misc Filename: pool/main/j/jasmin-compiler/jasmin-compiler_2026.09.0-1+resolute_amd64.deb Size: 17135136 SHA256: 7862ef1eb50ab189cb69ff0659fa92d295d4c7ea20c976d1cde514d0763bf4fb SHA1: 857c99d22a0b88caf83941df9895da92aee1043b MD5sum: ddf13e15fbf703fc7fc9a2f7eb07d9a1 Description: The Jasmin Workbench for High-Assurance Cryptography Implementations The Jasmin programming language smoothly combines high-level and low-level constructs, so as to support “assembly in the head” programming. Programmers can control many low-level details that are performance-critical: instruction selection and scheduling, what registers to spill and when, etc. They can also rely on high-level abstractions (variables, functions, arrays, loops, etc.) to structure their code and make it more amenable to formal verification. Package: libapron Source: apron Version: 0.9.15-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 2638 Depends: libmpfr6, libppl-c4 Priority: optional Section: libs Filename: pool/main/a/apron/libapron_0.9.15-1+resolute_amd64.deb Size: 845230 SHA256: 3154856df39a4cebec79937a2424cd64c74d5f02f53230ce795a1e512ae8c675 SHA1: e71672a61058001896d4645b5aad0ad83b5139b8 MD5sum: 53012a8c8a50f854d144142dc0901a5f Description: The Apron Numerical Abstract Domain Library Apron is a library to represent properties of numeric variables, such as variable bounds or linear relations between variables, and to manipulate these properties through semantic operations, such as variable assignments, tests, conjunctions, entailment. Package: libapron-dev Source: apron Version: 0.9.15-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 7557 Depends: libapron (= 0.9.15-1+resolute) Priority: optional Section: libdevel Filename: pool/main/a/apron/libapron-dev_0.9.15-1+resolute_amd64.deb Size: 1021614 SHA256: 72c93521571156e1c15dd14b3ad7b340af5f9670e1d7f4654ae8d4b54ec6d599 SHA1: 9764c6baf271cdb88ca642bccd3976a693cbcc88 MD5sum: cffa965c551eecf5e0366c59e26ab9c7 Description: The Apron Numerical Abstract Domain Library - development This package contains the headers and static libraries not included in the main libapron package. Package: libapron-ocaml-dev Source: apron Version: 0.9.15-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 3531 Depends: libapron (= 0.9.15-1+resolute), libgmpidl-ocaml Priority: optional Section: ocaml Filename: pool/main/a/apron/libapron-ocaml-dev_0.9.15-1+resolute_amd64.deb Size: 515028 SHA256: 8b381a8b81f8c2bbd15097426b2ba88703e57b56f1e4cb843442fdcae0b66f47 SHA1: 70b6fd4bc245dbdb37d971e54f68b67f8f2970d8 MD5sum: c32de7e21c1aa40a8129c690fbfe3c50 Description: The Apron Numerical Abstract Domain Library (OCaml libraries) This package contains the OCaml libraries for Apron Package: libbitwuzla-cxx-ocaml-dev Source: bitwuzla Version: 0.9.0-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 30705 Depends: libmpfr-dev Priority: optional Section: libs Filename: pool/main/b/bitwuzla/libbitwuzla-cxx-ocaml-dev_0.9.0-1+resolute_amd64.deb Size: 6549632 SHA256: 498258674c43d9d7f8bdc965d69144eddaae735fc28004f65b825a893f92776d SHA1: 42f438ec0f71dd6a42d05f37c82cb9e705ed7320 MD5sum: 582a5226f849b86908f13be28e346c0b Description: SMT solver for AUFBVFP (C++ API) Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions and their combinations. Its name is derived from an Austrian dialect expression that can be translated as “someone who tinkers with bits”. Package: libgmpidl-ocaml Version: 1.3.0-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 1297 Depends: camlidl, libbigarray-compat-ocaml-dev, libmpfr-dev Conflicts: libgmp-ocaml Priority: optional Section: ocaml Filename: pool/main/libg/libgmpidl-ocaml/libgmpidl-ocaml_1.3.0-1+resolute_amd64.deb Size: 223130 SHA256: f7721b9ed84004b5bfcca82ce5d74228ad05e6f1cdc84d9e606aa7e8a6875098 SHA1: 9ce2c30f12b106592a215afd88a3d29bcc964e88 MD5sum: bec97c7ce0273135bf23eb8574a2514d Description: OCaml interface to the GMP library This is MLGMPIDL. Package: libjasmin-easycrypt Source: jasmin-compiler Version: 2026.09.0-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 284 Recommends: easycrypt Priority: optional Section: misc Filename: pool/main/j/jasmin-compiler/libjasmin-easycrypt_2026.09.0-1+resolute_amd64.deb Size: 49490 SHA256: 944f161702abac140fccce37fd40b65eeb8153a8ede674d09d82b3fa54429c97 SHA1: 7c4d2dfbd93569265881a23ed2227fc5fc49be43 MD5sum: 40c77fb9c1b5491d361e387c0f480aaf Description: The Jasmin Workbench for High-Assurance Cryptography Implementations (EasyCrypt libraries) This package contains the EasyCrypt libraries of Jasmin Package: libjasmin-ocaml-dev Source: jasmin-compiler Version: 2026.09.0-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 106747 Depends: libangstrom-ocaml-dev, libbatteries-ocaml-dev, libmenhir-ocaml-dev, libzarith-ocaml-dev Priority: optional Section: ocaml Filename: pool/main/j/jasmin-compiler/libjasmin-ocaml-dev_2026.09.0-1+resolute_amd64.deb Size: 26534986 SHA256: 7c51c03d8675b3572d21aa151b4fcd5e8e5c75d050edf238a6d669419c7cbed4 SHA1: 0c51cd9299cdcb54db4fa7b98ea93a2ae37f3a72 MD5sum: a4e9674095b56b4c14c2f4c1aad86e6c Description: The Jasmin Workbench for High-Assurance Cryptography Implementations (OCaml libraries) This package contains the OCaml libraries of Jasmin Package: libmarkdown-ocaml-dev Source: markdown Version: 0.2.1-1+resolute Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 549 Depends: libbatteries-ocaml-dev, libtyxml-ocaml-dev Priority: optional Section: ocaml Filename: pool/main/m/markdown/libmarkdown-ocaml-dev_0.2.1-1+resolute_amd64.deb Size: 152342 SHA256: 821dc8a077147f2edf82cfd318b1341d444deb2f05522baf3b3b8ade54788a67 SHA1: d9f49280cfea5e58df7410eb0b0fb6737378bce0 MD5sum: 5dece6d769717427500b00e854f1d990 Description: Markdown processor for Ocsigen This is a pure OCaml parser for Markdown files. It was originally written for Ocsigen but may be useful in other contexts too. Package: libz3-4 Source: z3 Version: 4.16.0-1+resolute Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 19331 Depends: libc6 (>= 2.38), libgcc-s1 (>= 4.3), libstdc++6 (>= 14) Breaks: libz3-dev (<< 4.4.1) Replaces: libz3-dev (<< 4.4.1) Multi-Arch: same Homepage: https://github.com/Z3Prover/z3 Priority: optional Section: libs Filename: pool/main/z/z3/libz3-4_4.16.0-1+resolute_amd64.deb Size: 7182548 SHA256: 9509aac355ace3c29b5c24f82b1ea76ed0e129bacfb3f89b7d4090c866d327c7 SHA1: 4a3357fa98d5756866a0f465f9ce02b861f836c8 MD5sum: f34c9a3ac04b761a5c5d6be6cb641967 Description: theorem prover from Microsoft Research - runtime libraries Z3 is a state-of-the-art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories. Z3 offers a compelling match for software analysis and verification tools, since several common software constructs map directly into supported theories. . This package contains runtime libraries. You shouldn't have to install it manually. Package: libz3-dev Source: z3 Version: 4.16.0-1+resolute Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 626 Depends: libz3-4 (= 4.16.0-1+resolute) Multi-Arch: same Homepage: https://github.com/Z3Prover/z3 Priority: optional Section: libdevel Filename: pool/main/z/z3/libz3-dev_4.16.0-1+resolute_amd64.deb Size: 111080 SHA256: 350709e688564772c00decd96c158481189aec8e1fda2daa0ae0ef5a718e75a8 SHA1: 5a9643be3f42473bb1d5c896a91c5c6ed2128d0f MD5sum: f922877e663dfe12e841e3c741eca3ef Description: theorem prover from Microsoft Research - development files Z3 is a state-of-the-art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories. Z3 offers a compelling match for software analysis and verification tools, since several common software constructs map directly into supported theories. . This package can be used to invoke Z3 via its C++ API. Package: libz3-java Source: z3 Version: 4.16.0-1+resolute Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 214 Depends: libz3-jni (>= 4.16.0-1+resolute), libz3-jni (<< 4.16.0-1+resolute.1~), libz3-dev (= 4.16.0-1+resolute) Homepage: https://github.com/Z3Prover/z3 Priority: optional Section: java Filename: pool/main/z/z3/libz3-java_4.16.0-1+resolute_amd64.deb Size: 187262 SHA256: db042d714c3f95fee56acc2ac1251e410eb4c5fc39e40a4da13fd4b6f5667359 SHA1: 7c3deac9df00124e2a9a3784f401ccafad985251 MD5sum: df45c8cd318b942e35f00b7e89550034 Description: theorem prover from Microsoft Research - java bindings Z3 is a state-of-the-art theorem prover from Microsoft Research. See the z3 package for a detailed description. . This package can be used to invoke Z3 via its Java API. Package: libz3-jni Source: z3 Version: 4.16.0-1+resolute Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 241 Depends: libz3-dev (= 4.16.0-1+resolute), libc6 (>= 2.4), libgcc-s1 (>= 3.3.1), libstdc++6 (>= 5), libz3-4 (>= 4.16.0) Multi-Arch: same Homepage: https://github.com/Z3Prover/z3 Priority: optional Section: java Filename: pool/main/z/z3/libz3-jni_4.16.0-1+resolute_amd64.deb Size: 43024 SHA256: d7fcc4b772ae7f0d6e20629cf9efa2292044659dd30a2fa0d4d8c6ba26b71483 SHA1: 54f3445b8532430f66d899d071306a6b9d883d25 MD5sum: c5d0763ed8d59729870963ce3f2f346e Description: theorem prover from Microsoft Research - JNI library Z3 is a state-of-the-art theorem prover from Microsoft Research. See the z3 package for a detailed description. . This package provides the JNI library to invoke Z3 via its Java API. Package: python3-z3 Source: z3 Version: 4.16.0-1+resolute Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 654 Depends: libz3-dev (= 4.16.0-1+resolute), python3-pkg-resources, python3:any Homepage: https://github.com/Z3Prover/z3 Priority: optional Section: python Filename: pool/main/z/z3/python3-z3_4.16.0-1+resolute_amd64.deb Size: 87674 SHA256: b90ba2173df67385d497a2829bca9d3afa5e0f1a99ff619aab04a641aac33293 SHA1: a36ccc418fbe0e7031bfc86e614e33411b095a31 MD5sum: 18968a47bac523b7ba11fdcbf7c09411 Description: theorem prover from Microsoft Research - Python 3 bindings Z3 is a state-of-the-art theorem prover from Microsoft Research. See the z3 package for a detailed description. . This package can be used to invoke Z3 via its Python 3 API. Package: z3 Version: 4.16.0-1+resolute Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 19661 Depends: libc6 (>= 2.38), libgcc-s1 (>= 4.3), libstdc++6 (>= 14) Homepage: https://github.com/Z3Prover/z3 Priority: optional Section: science Filename: pool/main/z/z3/z3_4.16.0-1+resolute_amd64.deb Size: 7275776 SHA256: ab605141c23527b42c45dd28b2f7f2331f93d726956ae85b69ee73278d8ae0ca SHA1: 1914c9a356d163cedce0701d46a4e35757a23009 MD5sum: 5d741a70d7b9262e68db4395c1958c9d Description: theorem prover from Microsoft Research Z3 is a state-of-the-art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories. Z3 offers a compelling match for software analysis and verification tools, since several common software constructs map directly into supported theories. . The Z3 input format is an extension of the one defined by the SMT-LIB 2.0 standard.