The package is used for reasoning with big enough objects (mostly natural numbers). This package is essentially for backward compatibility purposes as bigenough will be subsumed by the near tactics. The formalization is based on the Mathematical Components library.

Mathematical Components for Coq has its origins in the formal proof of the Four Colour Theorem. Since then it has grown to cover many areas of mathematics and has been used for large scale projects like the formal proof of the Odd Order Theorem.

The library is written using the Ssreflect proof language that is an integral part of the distribution.

This package provides a survey of programming language semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, for a miniature example of an imperative programming language. Their encoding, the proofs of equivalence of different styles, abstract interpretation, and the proof of soundess obtained from axiomatic semantics or abstract interpretation is done in Coq. The tools can be run inside Coq, thus making them available for proof by reflection. Code can also be extracted and connected to a yacc-based parser, thanks to the use of a functor parameterized by a module type of strings. A hand-written parser is also provided in Coq, without associated proofs.

This library is an extension of coq-mathcomp which supports finite sets and finite maps on choicetypes (rather than finite types). This includes support for functions with finite support and multisets. The library also contains a generic order and set library, which will eventually be used to subsume notations for finite sets.

Coquelicot is an easier way of writing formulas and theorem statements, achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals, two-dimensional differentiability, asymptotic behaviors. It also offers some automations for performing differentiability proofs. Moreover, Coquelicot is a conservative extension of Coq's standard library and provides correspondence theorems between the two libraries.

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

Interval provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

Gappa is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act as a backend prover for the Why3 software verification plateform or as an automatic tactic for the Coq proof assistant.

Bignums is a coq library of arbitrary large numbers. It provides BigN, BigZ, BigQ that used to be part of Coq standard library.

Equations provides a notation for writing programs by dependent pattern-matching and (well-founded) recursion in Coq. It compiles everything down to eliminators for inductive types, equality and accessibility, providing a definitional extension to the Coq kernel.

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

Proof General is a major mode to turn Emacs into an interactive proof assistant to write formal mathematical proofs using a variety of theorem provers.

Formalizing syntactic theories with variable binders is not easy. Autosubst is a library for the Coq proof assistant to automate this process. Given an inductive definition of syntactic objects in de Bruijn representation augmented with binding annotations, Autosubst synthesizes the parallel substitution operation and automatically proves the basic lemmas about substitutions. This library contains an automation tactic that solves equations involving terms and substitutions. This makes the usage of substitution lemmas unnecessary. The tactic is based on our current work on a decision procedure for the equational theory of an extension of the sigma-calculus by Abadi et al. The library is completely written in Coq and uses Ltac to synthesize the substitution operation.

Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.

This package provides ifdtool, a program to dump Intel Firmware Descriptor data of an image file.

This package provides ectool, a program to dump and modify the contents of EC RAM on mobile computers.

nvramtool can see and/or modify Coreboot settings like the serial port speed, log level, etc. It requires Coreboot to be compiled with CONFIG_USE_OPTION_TABLE and some options require the iomem=relaxed kernel command line to work. Features:

• If Coreboot was compiled without CONFIG_STATIC_OPTION_TABLE, it can change its settings, which are applied after a reboot.

• It can modify Coreboot images default settings with nvramtool -C coreboot.rom [...].

• It has various options related to the file format used to store these settings.

• It can also read/write the CMOS memory where the Coreboot settings can be located.

This package provides tools for working with Intel Management Engine (ME). You need to sudo rmmod mei_me and sudo rmmod mei before using this tool. Also pass iomem=relaxed to the Linux kernel command line.

The bucts command can flip a bit in the BUC.TS register of the Intel I945 chipsets and show the register status. When the bit is set, it swaps the bootblock location. Because the bootblock region is often set read-only by the default BIOS, this enables to bypass that restriction and is used as part of a procedure to replace the nonfree BIOS with free software on various computers (Lenovo X60, X60s, X60T, T60, probably more).

The bincfg program comes with specifications files for the following binary formats:

• Various DDR3 and DDR4 SPD

• Configuration data for the Intel 82579LM Gigabit Ethernet PHY

• Configuration data for the Intel Gigabit Ethernet controller present in the Intel ICH9-M chipset.

• Intel Firmware Descriptor data for the Lenovo ThinkPad X200

• Configuration data for the ITE IT8718F SuperIO

It also comes with example files generated by bincfg.

GNU cpio copies files into or out of cpio or tar archives. Indeed, many formats are supported, including legacy formats. The format is determined automatically by the program and is handled appropriately. Furthermore, the location of the archive is not important. It can be another file on the drive, a tape, or data on a pipe.

This package provides a base64 stream encoder/decoder written in C99.

This package provides a header-only single-file std::filesystem compatible helper library, based on the C++17 and C++20 specs, but implemented for C++11, C++14, C++17 or C++20.