Botan is a crypto library written in C++. It provides a variety of cryptographic algorithms, including common ones such as AES, MD5, SHA, HMAC, RSA, Diffie-Hellman, DSA, and ECDSA, as well as many others that are more obscure or specialized. It also offers SSL/TLS (client and server), X.509v3 certificates and CRLs, and PKCS #10 certificate requests. A message processing system that uses a filter/pipeline metaphor allows for many common cryptographic tasks to be completed with just a few lines of code. Assembly and SIMD optimizations for common CPUs offers speedups for critical algorithms like AES and SHA-1.
LAPACK is a linear algebra library, based on LINPACK and EISPACK, designed to provide routines for handling simultaneous equations and matrix algebra efficiently, particularly on shared memory vector processors, parallel processors, and clusters. The code is written in Fortran, and requires the BLAS (Basic Linear Algebra Subprograms) library.
Mantissa is a collection of various mathematical algorithms in Java aimed towards simulation. It features a small set of linear algebra classes, a least squares estimator, some curve fitting classes, several ordinary differential equation integrators (all supporting multiple switching functions and dense output), vectors and rotations in a three dimensional space, algebra-related classes like rational and double polynomials, various orthogonal polynomials, some optimization algorithms using direct search methods, and more.
FLENS is short for Flexible Library for Efficient Numerical Solutions. This C++ can be used as a builing block for the implementation of other (higher-level) numerical libraries or numerical applications. It is a C++ library (requires a C++11 conform compiler). Easy install, as FLENS is headers only. It gives you Matrix/vector types for dense linear algebra; a generic (i.e. templated) implementation of BLAS; and a generic reimplementation of LAPACK. If high performance BLAS libraries like ATLAS, GotoBLAS, etc. are available, you simply can link against them and boost performance.
VXL is a set of portable C++ libraries designed for computer vision research and implementation. Numerics, imaging, and geometry are provided by stand-alone core libraries, with easy to use APIs and sophisticated processing algorithms. Other libraries provide stereo, video, structure from motion, probability modeling, GUI design, classification, robust estimation, feature tracking, topology, 3d imaging, and much more. It is written and used by an international team from academia and industry.
Isabelle is a popular generic theorem prover developed at Cambridge University and TU Munich. Existing logics like Isabelle/HOL provide a theorem proving environment ready to use for sizable applications. Isabelle may also serve as framework for rapid prototyping of deductive systems. It comes with a large library including Isabelle/HOL (classical higher-order logic), Isabelle/HOLCF (Scott's Logic for Computable Functions with HOL), Isabelle/FOL (classical and intuitionistic first-order logic), and Isabelle/ZF (Zermelo-Fraenkel set theory on top of FOL).
Higher Order Logic (HOL) is a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An Oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution, and property checking.