Adding Formal Verification Report #154
Conversation
dkcumming
commented
Jan 21, 2026
dkcumming
commented
- Adds the report Stephen wrote that contains:
- details of Solana
- details of equivalence proofs
- hand proofs for equivalence of P-Token and SPL-Token
- Updates VERIFICATION.md:
- Assumptions
- Limitations
- Shared harnesses
- Remove old smir script, artefacts, and dot files
dkcumming
requested review from
jberthold,
palinatolmach,
sskeirik and
tothtamas28
| - **Production code**: `src/entrypoint.rs` - Used for normal builds | ||
| - **Verification code**: `src/entrypoint-runtime-verification.rs` - Used when `runtime-verification` feature is enabled | ||
|
|
||
| Both P-Token and SPL token `entrypoint-runtime-verification.rs` have `include!` macros that import the respective prelude and shared |
There was a problem hiding this comment.
IIRC, the markdown convention is one sentence per line, and I'm not sure whether splitting the sentence into multiple lines would not introduce display issues on some devices. lgtm otherwise!
There was a problem hiding this comment.
This should render correctly in browsers. I have cut them shorter since the AWS application Jost and I were asked to introduce more line breaks to make them easier, so this is just the same approach from there.
sskeirik
left a comment
sskeirik
left a comment
There was a problem hiding this comment.
I perused the equivalence proofs report itself and it looks good! Thanks!
One minor comment: there is an asymmetry between the P-Token and SPL-Token verification guide files. We have:
- p-token/test-properties/VERIFICATION_GUIDE.md
- program/test-properties/README.md
It might be good to synchronize these two files at some point. Maybe they should both be README files, as this provides a better experience on GH?
One last point is that the SPL-Token test-properties README is a bit harder to follow than the corresponding text on the P-Token side. I think some introductory text at the top that describes the what and why could be helpful.
|
@sskeirik Yeah I haven't actually looked at the program/README.md. That will be fixed up at some point but not this PR |
