Package: easycrypt Version: 2026.09-1 Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 133097 Depends: why3 Priority: optional Section: misc Filename: pool/main/e/easycrypt/easycrypt_2026.09-1_amd64.deb Size: 59456832 SHA256: a5a19fccaaecd6225ee972eed23bce2b81efe6007300f3a8c644f013ad0c0982 SHA1: 9e9715b216cb75618c72463a34b94350bab073b0 MD5sum: a2ab8e0dab948af3a4aa05dc408a0573 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+trixie Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 65904 Depends: libapron Priority: optional Section: misc Filename: pool/main/j/jasmin-compiler/jasmin-compiler_2026.09.0-1+trixie_amd64.deb Size: 15386172 SHA256: b88a3de88881a7be61bf610e9dbabd75a300d880d9b530f4b9c2cea7f46a2444 SHA1: 452988f7c1000e5485d5d8dd993eaaa38da31e47 MD5sum: 4c00aba14964253b1c280d1622f019a5 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+trixie Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 2856 Depends: libmpfr6, libppl-c4 Priority: optional Section: libs Filename: pool/main/a/apron/libapron_0.9.15-1+trixie_amd64.deb Size: 833480 SHA256: 3705a1761c289e690d0d9d408d10e0302da2f0d96fdbc7690db5eb27479e59f9 SHA1: 1c98bf89e1f6da8fe15b9b0e462b6b95b8901af4 MD5sum: ce07a779e8e5b06f07d0a5552f7ffb89 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+trixie Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 7523 Depends: libapron (= 0.9.15-1+trixie) Priority: optional Section: libdevel Filename: pool/main/a/apron/libapron-dev_0.9.15-1+trixie_amd64.deb Size: 936188 SHA256: 43f92ed7be55f0800d4594d1857a494ab66906f4eed64868bcb97b35afb32503 SHA1: b3f225f04ed3069aaf0ace2c648273cd59466dfd MD5sum: b8e4478558c17da92b69441631523f89 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+trixie Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 3047 Depends: libapron (= 0.9.15-1+trixie), libgmpidl-ocaml Priority: optional Section: ocaml Filename: pool/main/a/apron/libapron-ocaml-dev_0.9.15-1+trixie_amd64.deb Size: 507156 SHA256: f3bbeb42df122a3d957dd5959bae3e607d1cec0041bc191fea69699e6f0d3e85 SHA1: 60b611cd27cba3b770e13037f8a59f73d89ec47c MD5sum: d8f34487dc2a407961f27582618d847d 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+trixie Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 29042 Depends: libmpfr-dev Priority: optional Section: libs Filename: pool/main/b/bitwuzla/libbitwuzla-cxx-ocaml-dev_0.9.0-1+trixie_amd64.deb Size: 6391560 SHA256: a52536007153755d4b280a71c07cfaa579f53075e7186c43d0b79e7882e3b685 SHA1: 738d70f654b9aae0d5c217b9364e3920e5edb175 MD5sum: 416bd40cc8c9294366a67e48f235a10f 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+trixie Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 1106 Conflicts: libgmp-ocaml Priority: optional Section: ocaml Filename: pool/main/libg/libgmpidl-ocaml/libgmpidl-ocaml_1.3.0-1+trixie_amd64.deb Size: 211232 SHA256: 147b4363e41fed99641fe1ff4a384f6aeefd47c9982a89ef2c3bc39ce4d5cfd0 SHA1: 7da54eaa9ac9ac39793e13ac636ea0c8f387e6e5 MD5sum: 116a030cde7c221bb3925d7d73d3be23 Description: OCaml interface to the GMP library This is MLGMPIDL. Package: libjasmin-easycrypt Source: jasmin-compiler Version: 2026.09.0-1+trixie 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+trixie_amd64.deb Size: 47912 SHA256: 6d9c73c633602f32509ba1a57082f5169d0984ed959299d38a017efc14867a69 SHA1: 35eb48329717e5b903b8fb568e784af7f1340b07 MD5sum: cc63b8763716dcf5fcb404d7c57f6f6e 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+trixie Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 60383 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+trixie_amd64.deb Size: 29876244 SHA256: f704baee2c23f75c53db187d8d251dd6e35ab51db7838162d2fb9f14baf25f86 SHA1: 39c3b38dd89017241d5bdd8b50eda71ad984f1b6 MD5sum: f273803fefb629f3a5989b4a6fa3350d 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+trixie Architecture: amd64 Maintainer: Vincent Laporte Installed-Size: 352 Depends: libbatteries-ocaml-dev, libtyxml-ocaml Priority: optional Section: ocaml Filename: pool/main/m/markdown/libmarkdown-ocaml-dev_0.2.1-1+trixie_amd64.deb Size: 151668 SHA256: 5b9f5e20fe75923d26ead2d28c9718fd173ced1b97aaa418a962ba06b5b3e034 SHA1: cbef3d8d49855554b2ae30a69fb134c30a62eb5b MD5sum: b2331c37bb7434a16ff87cd3c8599c32 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+trixie Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 28101 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+trixie_amd64.deb Size: 8864888 SHA256: 0362a3901528b85603e821cf6b317dd5d624dd206fddf52cecee604d0889ec37 SHA1: 5870d6b4764e2c9f3850296f3a7cc025eb9d8bbd MD5sum: f9939ce090a6bf7bd833bf005d08250a 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+trixie Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 628 Depends: libz3-4 (= 4.16.0-1+trixie) Multi-Arch: same Homepage: https://github.com/Z3Prover/z3 Priority: optional Section: libdevel Filename: pool/main/z/z3/libz3-dev_4.16.0-1+trixie_amd64.deb Size: 112044 SHA256: af427ab58d9a14ebf0d7256f9e265940158583295d3505b6b8622b4ba061ce31 SHA1: df4f0a0433a16612cbfdec25ab1e3e70e0e497b9 MD5sum: 643342eccc8e0440ae51f6556866a374 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+trixie Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 214 Depends: libz3-jni (>= 4.16.0-1+trixie), libz3-jni (<< 4.16.0-1+trixie.1~), libz3-dev (= 4.16.0-1+trixie) Homepage: https://github.com/Z3Prover/z3 Priority: optional Section: java Filename: pool/main/z/z3/libz3-java_4.16.0-1+trixie_amd64.deb Size: 188144 SHA256: 939c94d0ee30c05f4901561b6957e9e54a52ed5fe1ff670b107e10f080cfd4f3 SHA1: 14abe8fbe17254995a0544a8cc99237763ac4069 MD5sum: 97f606dc3b7bc66263e928d16a634bf2 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+trixie Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 232 Depends: libz3-dev (= 4.16.0-1+trixie), libc6 (>= 2.4), libgcc-s1 (>= 3.0), 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+trixie_amd64.deb Size: 38396 SHA256: 33651cf63a6e98060e6e64152188c5d654e721d758ddbd28d32050318da12eaf SHA1: 6229b9c62e5588cd8e71baa219079728b597be19 MD5sum: 21d301af83fdb04167596984c850b813 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+trixie Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 654 Depends: libz3-dev (= 4.16.0-1+trixie), 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+trixie_amd64.deb Size: 86296 SHA256: 4ead161be95c015497d9e5468080c13807c9b124a6d5adc81cc1db7ed46edede SHA1: 61bb82095cd6fad199ddf2162ba577c02c93b9b6 MD5sum: 7c0ef4e22b4ab150426303c2cbe0bdee 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+trixie Architecture: amd64 Maintainer: LLVM Packaging Team Installed-Size: 28083 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+trixie_amd64.deb Size: 8869400 SHA256: b97d2d73bad0af83dfe6fc427839da5083b9341373197dda88f64635b2b4c188 SHA1: af80673efd8799c8fefd38985245f8da50c3cce3 MD5sum: 66bed4ccdcc2618c985072caba9b9b11 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.