Justification logic originated as part of a successful project to provide a constructive semantics for intuitionistic logic. The technical machinery developed in this area: an appropriate proof theory, model theory, complexity estimates and a broad variety of applications, can serve as a basis for a new, hyperintensional logic. Hyperintensional systems go beyond logical equivalence. Fermat’s Last Theorem, FLT, is logically equivalent to $0=0$ since both are provable, and hence denote the same proposition. However, the context of proofs distinguishes them immediately: a proof of $0=0$ is not necessarily a proof of FLT, and vice versa. Justification logics offer a more precise logical tool; we discuss a number of examples from different areas in which new methods provide a superior analysis.