We present an overview of Clousot, our current tool to statically check CodeContracts. CodeContracts enable a compiler and languageindependent speciﬁcation of Contracts (precondition, postconditions and object invariants). Clousot checks every method in isolation using an assume/guarantee reasoning: For each method under analysis Clousot assumes its precondition and asserts the postcondition. For each invoked method, Clousot asserts its precondition and assumes the postcondition. Clousot also checks the absence of common runtime errors, such as null-pointer errors, buﬀer or array overruns, divisions by zero, as well as less common ones such as checked integer overﬂows or ﬂoating point precision mismatches in comparisons. At the core of Clousot there is an abstract interpretation engine which infers program facts. Facts are used to discharge the assertions. The use of abstract interpretation (vs usual weakest precondition-based checkers) has two main advantages: (i) the checker automatically infers loop invariants letting the user focus only on boundary speciﬁcations; (ii) the checker is deterministic in its behavior (which abstractly mimics the ﬂow of the program) and it can be tuned for precision and cost. Clousot embodies other techniques, such as iterative domain reﬁnement, goal-directed backward propagation, precondition and postcondition inference, and message prioritization.