There is a confusion about terminology here I think. Mathematical proofs including cryptography proofs use models simplifying reality; i.e. the real practical system might still be susceptible to attacks despite a proof of security.
For crypto primitives (classic mc eliece, curve25519, ed25519, RSA, etc etc) the standard for proofs is currently showing that they are as hard as some well studied mathematical problem. This is done by showing that an attack on the primitive leads to an attack on the underlying mathematical primitive. The proof for Diffie-Hellman shows that attacking DH leads to an efficient solution for the discrete log problem. I.e. the proof is a reduction to the underlying primitive.
No primitive is perfectly secure (at least a brute force – i.e. guessing each possibility is possible); there is some probability that the adversary can guess the right key. We call this probability the adversary's advantage. One task in cryptoanalysis is to find better attacks against primitives with a higher advantage; if an attack with a polynomial time average runtime is found, the primitive is broken. Finding a higher non-polynomial attack is still an interesting result.
The standard for protocols is proving that the protocol is secure assuming the primitives are secure; since multiple primitives are used you basically get a formula deriving an advantage for breaking the entire protocol. The proof is a reduction to a set of primitives.
We did not build a proof in that gold standard, although we are working on it. We built a proof in the symbolic model – known as a symbolic analysis. This uses the perfect cryptography assumption; i.e. we assumed that the advantages for each primitive are zero. Google "Dolev-Yao-Model".
This makes the proof much easier; a proof assistant such as ProVerif can basically find a proof automatically using logic programming methods (horn clauses).
The definitions of security are fairly well understood; unfortunately there is a lot to go into so I can't expand on that here. Looking up "IND-CPA" and "IND-CCA" might be a good start; these are the security games/models of security for asymmetric encryption; you could move on to the models for key exchange algorithms there. Reading the [noise protocol spec](https://noiseprotocol.org/) is also a good start.
A professor in university had an interesting illustration of the attackers advantage.
First off, an attack is straight up impossible. If you need to invest ~ 10k operations for each atom in the observable universe to break a system with more than 50% probability, well. That won't get broken, until breakthroughs in related mathematics happen. Even if you were lucky to guess a key once, you will never be twice.
Then, you enter the area of throwing money at it. You can conquer quite a few exponents of two of search space if you throw a distributed system worth billions of dollars at it. And a couple more millions in change in post-docs shaving off fractions off of that exponent. Here you are usually safe, since it'll be hard even with all that hardware, manpower and math research.
But once it's exponential growth with lower exponents or even polynomial, it's just an implementation and optimization issue on the way to real-time decodeability.
However, even if the math is hard, the implementation might not be. And that's why a formally proven implementation of a very hard algorithm is exciting. If the implementation is provably as hard as discrete logarithms, and you get broken, a silly amount of modern crypto gets broken all at once.
Or we might learn something about formal verification and your method and tooling. Which is also good progress.
There is a confusion about terminology here I think. Mathematical proofs including cryptography proofs use models simplifying reality; i.e. the real practical system might still be susceptible to attacks despite a proof of security.
For crypto primitives (classic mc eliece, curve25519, ed25519, RSA, etc etc) the standard for proofs is currently showing that they are as hard as some well studied mathematical problem. This is done by showing that an attack on the primitive leads to an attack on the underlying mathematical primitive. The proof for Diffie-Hellman shows that attacking DH leads to an efficient solution for the discrete log problem. I.e. the proof is a reduction to the underlying primitive.
No primitive is perfectly secure (at least a brute force – i.e. guessing each possibility is possible); there is some probability that the adversary can guess the right key. We call this probability the adversary's advantage. One task in cryptoanalysis is to find better attacks against primitives with a higher advantage; if an attack with a polynomial time average runtime is found, the primitive is broken. Finding a higher non-polynomial attack is still an interesting result.
The standard for protocols is proving that the protocol is secure assuming the primitives are secure; since multiple primitives are used you basically get a formula deriving an advantage for breaking the entire protocol. The proof is a reduction to a set of primitives.
We did not build a proof in that gold standard, although we are working on it. We built a proof in the symbolic model – known as a symbolic analysis. This uses the perfect cryptography assumption; i.e. we assumed that the advantages for each primitive are zero. Google "Dolev-Yao-Model".
This makes the proof much easier; a proof assistant such as ProVerif can basically find a proof automatically using logic programming methods (horn clauses).
The definitions of security are fairly well understood; unfortunately there is a lot to go into so I can't expand on that here. Looking up "IND-CPA" and "IND-CCA" might be a good start; these are the security games/models of security for asymmetric encryption; you could move on to the models for key exchange algorithms there. Reading the [noise protocol spec](https://noiseprotocol.org/) is also a good start.