Matita (that means pencil in italian) is an experimental, interactive theorem prover under development at the Computer Science Department of the University of Bologna.

An interactive prover is a software tool aiding the development of formal proofs by man-machine collaboration. It provides a formal language where mathematical definitions, executable algorithms and theorems cohexist, and an interactive environment keeping the current status of the proof, and updating it according to commands (usually called tactics) issued by the user.

Matita is based on a Dependent Type System known as the Calculus of Inductive Constructions.

It embeds key computational constructs of functional programming languages: functions can be defined by (well-founded) recursion, and are live entities that can be tested and executed.

At the same time, proofs are an integrated part of the formalism, allowing, via the Curry Howard isomorphism, a smooth interplay between specification, implementation and verification: proofs are objects of the language, and can be treated as normal data, naturally leading to a programming style akin to proof-carrying-code, where chunks of software come equipped with proofs of (some of) their properties.

Matita is currently adopted in the European Union "Certified Complexity" Project CerCo for the formal verification of a complexity-preserving compiler from a large subset of C to a microcontroller assembly of the kind traditionally used in embedded systems.