Techniques to verify or invalidate the security of computer systems have come a long way in recent years. While sophisticated tools are available to specify and formally verify the behavior of a system, attack techniques have evolved to the point of questioning the possibility of obtaining adequate levels of security, especially in critical applications. In a recent paper, Bognar et al. have clearly highlighted this inconsistency between the two worlds: on one side, formal verification allows writing irrefutable proofs of the security of a system, on the other side, concrete attacks make these proofs waver, exhibiting a gap between models and implementations which is very complex to bridge. In this extended abstract, we outline a new general methodology based on robust non-interference preservation that reduces this gap by bringing together some peculiarities of the two approaches. Our methodology uses automata learning to extract behavioral models of real systems, and model checking to analyze them and identify attacks or anomalies.