As asked in the question, this post asks the topicallity of "formal verification" tools. I realize I have little experience with "formal verification" and I don't fully grasp its concepts. I saw this phrase from the round-3 official comment of NTRU Prime reacheable from here. This question asks Q...

The R1CS constraints are expressed over finite fields. Many proofing systems such as zkSnark use prover keys such as $g^{\alpha^0}, g^{\alpha^1}, ..., g^{\alpha^n}$ where $\alpha$ is a field element. I'm wondering are these field elements actually integers?