To explain what is going on mathematically:
M = (Q, q0, →, I)
where Q is the state space, q₀ is the initial state, → is the transition relation, and I is the set of invariants and admissibility rules.
This is the model of a state machine. A state machine transitions through states according to the rules and invariants. Invariants which are ∀, for all, every, always, determine the possible paths the software can take, if the invariants hold. Model checking, or state machines, are about the relationships between the states. What we can do, is decide which states are safe to reach, and which states are disaster states which must be unreachable.
The disaster set D ⊆ Q contains every state the protocol must never reach.
The way to mathematically guarantee the software only behaves as intended, is to make the disaster states unreachable:
Reach(M) ∩ D = ∅
And in the case of the Drift Protocol we can make that specific disaster state unreachable by abstracting it symbolically and mathematically guaranteeing all exploits of that disaster type are unreachable.
We can use the neuro symbolic loop to look for disaster states pre-emptively:
q_NS(y | x) ∝ q_N(y | x) · χ_S(y, x)
We can then find the disaster shape corresponding with the Drift protocol exploit:
Drift(σ) := ∃ i < j < k < ℓ such that
AdminEscalated(σ_i) ∧
BadCollateralAccepted(σ_j) ∧
OracleOrRiskCompromised(σk) ∧
qℓ ∈ D
Then we can produce the invariants that block that off, making it mathematically unreachable:
Drift(σ) ≔ ∃i∃j∃k∃ℓ(i < j ∧ j < k ∧ k < ℓ ∧ AdminEscalated(σ_i) ∧ BadCollateralAccepted(σ_j) ∧ OracleOrRiskCompromised(σk) ∧ qℓ ∈ D)
∀σ(σ ∈ Tr(M) ⇒ ¬Drift(σ))
Safe(M) := P₁ ∧ P₂ ∧ P₃
¬Safe(M) = ¬P₁ ∨ ¬P₂ ∨ ¬P₃
This abstraction is a superpower. It allows us to exhaustively enumerate and search the state space. We can then mathematically check that the Drift disaster state can never be reached. Not only that, but we can block off all disaster states of the same shape as the Drift state. This ability works best when you can predict or ask "what if?", and the "what if?" is asked by the LLM in the neural symbolic loop. As an AI it's very good at search, it can predict the next "what if?", and if it can do that, it can search what I call the witness space. Witness space is the space of ∃, or "there exists", and by asking "what if?" you can search that space to find out if an exploit exists within it.
∃p ∀σ ∈ Tr(M_p), ¬Exploit(σ) ∧ (Legit(σ) → Acc(σ))
Which is there is no exploit found within the witness space. What we need to recognize is that this is not boundless. The space we can check is bounded, which means we have to keep the search spaces reasonable enough that they can be searched within a reasonable amount of time. This is why if there are infinite possible states, you can't search through brute force enumeration, so it becomes hard to say certain things about those spaces.
You can still produce proofs allowing you to say some things, but you can't search in the same way that you can in bounded finite spaces where you can say to everyone "I've checked every possible state the software can be in, and I can mathematically guarantee the software can never be in this list of disaster states."