Talk by Giu­seppe Pri­mie­ro (Università degli Studi di Milano Statale): On verify­ing com­pu­ta­ti­o­nal sys­tems. From func­ti­o­nal to non-func­ti­o­nal pro­per­ties

The history of formal verification can be understood as an evolving response to the problem of computational correctness. Early approaches treated computer programs as abstract, closed, and fully specified artefacts. In this phase, correctness was primarily conceived as input–output conformity, grounded in mathematical semantics and deductive reasoning. With the rise of concurrency, distribution, and large-scale systems, verification expanded to address non-deterministic behaviour. Correctness was no longer purely functional but increasingly temporal and probabilistic. In the contemporary era of machine learning and AI systems, verification faces a deeper transformation. Systems are no longer fully transparent, deterministic, or confined to purely functional specifications. Instead, they operate in open sociotechnical environments and must satisfy non-functional properties such as trustworthiness, fairness, transparency, and responsibility. This evolution marks a conceptual shift: from verifying that a system computes the correct function to verifying that it behaves in normatively acceptable ways under uncertainty and social impact. Formal verification thus extends beyond mathematical conformity to specification and becomes a tool for assessing epistemic reliability, distributive justice, and accountable design. In the context of AI, the central question of formal verification is no longer only “Does the system compute correctly?” but also “Can we formally guarantee that its probabilistic, opaque, and non-deterministic behaviour is trustworthy, fair, and responsibly governed?”