$ nightshade vulnerable.compact --config config.json --compiler /path/to/compactc

HIGH — Public-key equality gates a state-changing effect [spoofable-authorization]
vulnerable.compact:6:3
  6 |   assert(ownPublicKey() == owner, "owner");
    |   ^
change requires raw witness data from ownPublicKey to equal ledger owner on every modeled successful reach. The guard covers 1 effect site: ledger-write stored. Every successful history reaching these effects has only raw-witness/public-data checks; no additional modeled gate is present. Equality alone does not demonstrate possession of a secret; review the intended authentication and protocol role.
Source: vulnerable.compact:6:10
Constraint: vulnerable.compact:6:3
Call path: change
Remediation: If this check is intended as authentication, enforce a suitable secret-preimage or protocol-specific proof. Review key initialization, secrecy and replay assumptions. Document and triage intentional public-data validation.

Semantic profile: compact-0.34.0-zkir2.
Baseline analysis: complete; selected rules: complete.
Rule coverage: 1 selected rule(s); 0 with incomplete entries.
1 finding(s), 0 suppressed, 0 baseline; 1/1 entrypoint(s) completed; analysis complete. Compiler validation passed.