A major peculiarity of quantum programming is the impossibility to use standard debugging techniques there. Indeed, runtime state (partial) inspection is made impossible to use because of destructive and non-deterministic measurement. Still, quantum programming manipulates complex data structures with unintuitive behaviors, so that any realistic usage scenario would necessarily provide original verification and debugging solutions. The natural direction is to lie on formal analysis of programs, with static semantical analysis. In recent years, several such propositions were developed (Coqq, Qafny, QHL,…), enabling a user to build formal, mathematical proofs that a program she is writing satisfies its specifications. These have been successively applied to the most standard programs and programming features from the litterature. The drawback is the cost of building formal proofs. In the general case, the formal proof of a program specifications is indeed much longer than the program itself and requires a strong expertise in formal verification and computer aided proof from the developper. Therefore, the next challenge for quantum verification is to lower the size of programs specifications proofs and the level of expertise they require. In this talk we discuss the potentiality offered by the “path-sum” representation to tackle this problem.