Fault analysis is an effective cryptanalysis method for both unprotected and masked cryptographic implementations. However, it usually involves complex mathematical derivations or computation intensive statistical analysis, and requires knowledge about the fault location or pattern. Motivated by the recent advances in machine learning and formal verification, this paper proposes a fault analysis method on AES and SM4 through automatic property extraction and checking. It automatically mines verifiable fault related properties from a limited number of fault traces and retrieves the key through formal checking of the extracted properties under the verification constraints of correct and faulty ciphertext pairs. Experimental results show that 35 and 25 fault traces are enough for creating precise fault properties for AES and SM4 respectively. With two correct and faulty ciphertext pairs that satisfy any of the extracted properties, a round key of AES and SM4 can be uniquely determined.