Computer programs are increasingly used in legal procedures such as computing taxes, attributing social allowances, establishing contracts, e-voting etc. This, of course, raise important questions : are such programs reliable ? Are they fair ? Are they implementing the laws as stated in the books ? These concerns are not only questioning what the programs are computing but also how they are computing it.

To express such properties of programs, a general framework called Hyper Properties has been proposed. It allows to specify relational properties of computer systems by comparing several executions. Large classes of privacy and fairness properties have been identified to be expressible as hyper properties. In turn, this led to the systematic study of new logics to specify and verify hyper properties of programs. These tools have been successfully used for the verification of reactive systems, cryptographic programs, and other fields of applications. In this short talk, we argue that hyper properties could also be applied to the study of legal expert systems.