docs(kms/auth-eth): add formal specification (Phase 1)

A normative spec for DstackKms + DstackApp independent of code — the
deliverable an external FV firm engagement (Runtime Verification,
ChainSecurity, Certora) would build against.

Contents:
- Trust model: principals, what each is trusted for and not for, EVM
  / proxy / off-chain pipeline assumptions
- Storage layout per contract with frame-condition rules
- Per-function pre/post/frame/events/reverts specs for the entire
  public surface
- Decision-table semantics for isAppAllowed (both KMS- and App-level)
- State invariants (INV-1 through INV-7) with their current
  verification status
- Cross-contract assumptions: KMS↔App delegation, KMS↔Proxy factory,
  App↔Proxy upgrade authorization
- Adversarial scenarios: malicious registerApp + downstream gates,
  reentrancy structural-impossibility argument, gas-griefing,
  front-running, initializer selector collision
- Known verification gaps (cross-transaction invariants, delegated-
  call universal quantification, KEVM bytecode-level proof) — these
  are the items a future audit-firm engagement would close
- Open spec-level questions for the dstack team (renounceOwnership
  semantics, appImplementation drift, OS-image revocation reach,
  gatewayAppId format)

Each property in the spec that has a Halmos symbolic proof cites
the test name; properties without a citation are explicit gaps.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: h4x3rotab

kms/auth-eth/docs/formal-verification.md

@@ -8,6 +8,10 @@ SPDX-License-Identifier: Apache-2.0
 A layered approach: cheap static analysis → SMTChecker invariants → Halmos
 symbolic tests → (optional) Certora. Each layer is independently mergeable.
 
+The **formal specification** these layers verify against lives in
+[`specification.md`](./specification.md). The spec is normative — code
+and tests track the spec, not the other way around.
+
 Reference: <https://github.com/leonardoalt/ethereum_formal_verification_overview>
 
 ## Targets