# Formal Safety Properties

For auditors or formal verification, key properties include:

#### **P1 — Solvency:**

At all times:\
totalAssets(zksync) ≥ totalShares × sharePrice

#### **P2 — Non-inflationary deposits:**

Mint(shares) only if assets\_received\_finalized == true

#### **P3 — Non-deflationary withdrawals:**

Burn(shares) only if assets\_sent\_validated == true

#### **P4 — Plane-independence:**

Failure of plane X cannot modify valid accounting of plane Y.

#### **P5 — Deterministic NAV:**

NAV(t) depends only on validated\_state(t), never on remote assumptions.

#### **P6 — No replay risk:**

Timestamps and proof roots bind remote data to specific reporting cycles.

#### **P7 — Price integrity:**

NAV\_price\_update = f(verified\_price\_sources)

These properties ensure mathematical correctness.


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://multistake-1.gitbook.io/multistake-docs/documentation/security-model/securing-multistake/formal-safety-properties.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.