Soroban Contract Templates and Security Code Examples

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/Centurylong/sanctifier/llms.txt

Use this file to discover all available pages before exploring further.

​

Using contracts as templates

cargo build -p amm-pool --release --target wasm32-unknown-unknown

sanctifier analyze contracts/amm-pool

​

amm-pool

• Slippage protection — The swap function accepts a min_amount_out parameter; the transaction reverts if the calculated output falls below it, preventing sandwich attacks.
• MEV resistance — A deadline (Unix timestamp) parameter causes stale transactions to revert automatically.
• K-invariant enforcement — After every swap the contract explicitly verifies new_k >= old_k, providing an on-chain assertion that the constant product property is never violated.
• Checked arithmetic throughout — All balance and reserve math uses checked_add, checked_mul, and checked_div; no raw +/* operators appear in financial code paths.

pub fn swap(
    env: Env,
    user: Address,
    token_in: Address,
    amount_in: u128,
    min_amount_out: u128,   // slippage guard
    deadline: u64,          // MEV guard
) -> u128

cd contracts/amm-pool
cargo test
PROPTEST_CASES=10000 cargo test --test proptest_amm  # high-intensity property testing
cargo kani --harness verify_constant_product_invariant

​

reentrancy-guard

• Storage-backed mutex — The lock survives cross-contract call boundaries because it lives in instance storage, not a local variable.
• Pure state-transition core — enter_pure and exit_pure are side-effect-free functions that can be exhaustively verified by Kani without any host-type stubs.
• no_std compatibility — Works in any Soroban contract without pulling in std.

use reentrancy_guard::ReentrancyGuard;

pub fn withdraw(env: Env, amount: i128) {
    let guard = ReentrancyGuard::new(&env);
    guard.enter();  // panics with "reentrancy detected" if re-entered
    // ... safely perform the withdrawal ...
    guard.exit();
}

cd contracts/reentrancy-guard
cargo kani

​

runtime-guard-wrapper

• Pre-execution guards — Verifies the wrapped contract address is configured and that instance-storage integrity keys are present before forwarding any call.
• Post-execution invariant checks — After each guarded call the wrapper asserts the invariants_checked counter strictly advanced; a stuck counter surfaces as a GuardError::InvariantCounterStuck event.
• Audit-trail events — The guard_invariant_result! macro publishes inv_fail events with a machine-readable payload; off-chain indexers can subscribe to a single topic to observe invariant failures across all instrumented contracts.
• Bounded storage — The call log is capped at 100 entries and metrics at 1,000 entries, preventing the instance-storage capacity DoS described in SOB-2024-025.

pub fn init(env: Env, wrapped_contract: Address)
pub fn execute_guarded(env: Env, function_name: Symbol, args: Vec<Val>) -> Result<Val, Error>
pub fn get_stats(env: Env) -> (u32, u32, u32)  // (invariants_checked, executions, guard_failures)
pub fn health_check(env: Env) -> bool

sanctifier deploy ./contracts/runtime-guard-wrapper --network testnet --validate

soroban contract invoke \
  --id "$CONTRACT_ID" --network testnet \
  -- init "$WRAPPED_CONTRACT"

soroban contract invoke \
  --id "$CONTRACT_ID" --network testnet \
  -- health_check

​

protected-vault

• Direct integration of reentrancy-guard as a workspace dependency.
• Positive access-control (amount > 0 assertion before state mutation).
• Demonstrates the pattern described in vulnerability entry SOB-2024-015.

pub fn withdraw(env: Env, amount: i128) {
    assert!(amount > 0, "amount must be positive");
    let guard = ReentrancyGuard::new(&env);
    guard.enter();
    let balance: i128 = env.storage().instance().get(&BALANCE_KEY).unwrap_or(0);
    assert!(balance >= amount, "insufficient balance");
    env.storage().instance().set(&BALANCE_KEY, &(balance - amount));
    guard.exit();
}

​

token-invariants

• Core logic separation — pure::{mint_pure, burn_pure, transfer_pure} contain no Env, Address, or Symbol dependencies, making them directly Kani-verifiable.
• Annotated invariants — #[sanctify::invariant(balance >= 0)] and supply-conservation assertions are declared inline and automatically checked by sanctifier verify.
• Kani harnesses — Located in src/kani_proofs.rs; verify overflow safety and conservation properties.

sanctifier verify contracts/token-invariants
sanctifier prove --path contracts/token-invariants --invariant supply_conserved
cargo kani --manifest-path contracts/token-invariants/Cargo.toml

​

sep41-token-invariants

• Allowance decrement enforced before balance mutation, preventing SOL-2024-009.
• Allowance race condition guard (set to zero before non-zero), preventing SOB-2024-017.
• All five token operations (transfer, transfer_from, approve, mint, burn) have Kani harnesses in src/kani_proofs.rs.

sanctifier verify contracts/sep41-token-invariants
cargo kani --manifest-path contracts/sep41-token-invariants/Cargo.toml

​

vulnerable-contract

• set_admin without any require_auth call (triggers finding S001 / SOL-2024-001).
• A contrasting set_admin_secure function showing the correct pattern.

sanctifier analyze contracts/vulnerable-contract --format json

​

token-with-bugs

• initialize does not persist admin, name, or symbol, leaving the initialization guard incomplete (triggers SOL-2024-001 pattern).
• Missing require_auth on privileged entry points.
• Intentional arithmetic issues for S003 detector coverage.

​

kani-poc

• initialize_pure(is_initialized: bool) -> Result<(), &'static str> — pure function verified to reject double-initialization for all possible boolean inputs.
• Shows how to structure a contract so the security-critical arithmetic is separated from the host-interaction layer, enabling Kani coverage without stubs.

cd contracts/kani-poc
cargo kani

​

zk-verifier

• Storing large cryptographic artifacts (verifying keys) in persistent storage rather than instance storage, avoiding SOB-2024-025.
• Using ark-serialize::CanonicalDeserialize to safely parse untrusted byte inputs.
• wee_alloc as a global allocator for lean WASM output.

pub fn init(env: Env, vk_bytes: Bytes)
pub fn verify(env: Env, proof_bytes: Bytes, public_inputs_bytes: Bytes) -> bool

​

Running all contract tests

cargo test --workspace --exclude sanctifier-cli --exclude sanctifier-core

sanctifier analyze contracts/

sanctifier analyze contracts/ \
  --format json \
  2>&1 | grep -v "vulnerable-contract\|token-with-bugs"

ignore_paths = ["contracts/vulnerable-contract", "contracts/token-with-bugs"]