Sol.College

Full lesson

excalead

Continuous auditing for Solana smart contracts, with Formal Verification & AI

What it does

From the project README:

We combine the rigor of the **Rocq (Coq)** proof assistant with the speed of **AI automation** to bring formal methods to every Solana developer.
Original
Excalead/excalead
SuperStack fork
Blockchains/excalead @ 71dcf87
Stars
6
Last push (original)
2025-12-05
Languages
Rocq Prover, Rust, Shell, Dune
Detected stack
Anchor
Categories
AI & Agents
Licence
MIT
Homepage
https://excalead.com/

Architecture

27 source files. By extension: .rs ×27.

Top-level directorySource files
Excalead26
src1

Dapp: devnet deploy pending

⏳ Devnet deploy pending — goes live when the devnet wallet is topped up. This fork's own dapp is not deployed yet, so there is no program address or transaction to show. It is queued in dapp-queue.txt; once devnet SOL is available it is deployed, exercised with real devnet transactions, and this section switches to the live dapp at /dapps/excalead/. Until then, the lesson and step-by-step guide below are complete, and you can run it locally with the commands below.

Key code, explained

Excerpts chosen automatically where the code uses the most Solana concepts, pinned to the fork's commit.

Excalead/excalead · Excalead/src/examples/quantu_8004/validation_registry/lib.rs L109–132 @ 71dcf87 · MIT · original
        validation_request.bump = ctx.bumps.validation_request;         // Increment total requests counter        config.total_requests = config.total_requests            .checked_add(1)            .ok_or(ValidationError::Overflow)?;         // Emit event with full metadata (URI stored in event, not on-chain)        emit!(ValidationRequested {            agent_id,            validator_address,            nonce,            request_uri,            request_hash,            requester: ctx.accounts.requester.key(),            created_at: clock.unix_timestamp,        });         msg!("Validation requested for agent #{} by validator {}", agent_id, validator_address);         Ok(())    }     /// Validator responds to a validation request (ERC-8004: validationResponse)
  1. Line 109 validation_request.bump = ctx.bumps.validation_request;: Uses the bump seed, the extra byte that pushes the derived address off the ed25519 curve.
  2. Line 113 .checked_add(1): Uses checked arithmetic so overflow fails instead of wrapping.
  3. Line 117 emit!(ValidationRequested {: Emits an Anchor event that clients can parse from the logs.
  4. Line 124 created_at: clock.unix_timestamp,: Reads on-chain time from the Clock sysvar.
  5. Line 127 msg!("Validation requested for agent #{} by validator {}", agent_id, validator_address);: Logs to the program log, which is visible in explorers and the test output.
Excalead/excalead · Excalead/src/secure/basic4.rs L25–48 @ 71dcf87 · MIT · original
            ctx.accounts.authority.key(),            ctx.accounts.counter.authority,            ErrorCode::Unauthorized        );         ctx.accounts.counter.count += 1;        Ok(())    }} #[derive(Accounts)]pub struct Initialize<'info> {    #[account(        init,        payer = authority,        space = Counter::SIZE,        seeds = [b"counter"],        bump    )]    counter: Account<'info, Counter>,    #[account(mut)]    authority: Signer<'info>,    system_program: Program<'info, System>,}
  1. Line 38 init,: Creates and pays for a new account. Space and payer must be specified.
  2. Line 41 seeds = [b"counter"],: Declares the PDA seeds. Anchor re-derives the address and rejects the account if it doesn't match.
  3. Line 42 bump: Uses the bump seed, the extra byte that pushes the derived address off the ed25519 curve.
  4. Line 46 authority: Signer<'info>,: Requires this account to have signed the transaction.
Excalead/excalead · Excalead/src/examples/domin8/reference/instructions/initialize.rs L13–36 @ 71dcf87 · MIT · original
    )]    pub config: Account<'info, GameConfig>,        #[account(        init,        payer = authority,        space = GameRound::LEN,        seeds = [GAME_ROUND_SEED],        bump    )]    pub game_round: Account<'info, GameRound>,        /// CHECK: This is the vault PDA that will hold game funds    #[account(        seeds = [VAULT_SEED],        bump    )]    pub vault: UncheckedAccount<'info>,        #[account(mut)]    pub authority: Signer<'info>,        pub system_program: Program<'info, System>,}
  1. Line 17 init,: Creates and pays for a new account. Space and payer must be specified.
  2. Line 20 seeds = [GAME_ROUND_SEED],: Declares the PDA seeds. Anchor re-derives the address and rejects the account if it doesn't match.
  3. Line 21 bump: Uses the bump seed, the extra byte that pushes the derived address off the ed25519 curve.
  4. Line 33 pub authority: Signer<'info>,: Requires this account to have signed the transaction.
Excalead/excalead · Excalead/src/examples/domin8/reference/instructions/deposit_bet.rs L13–36 @ 71dcf87 · MIT · original
    )]    pub game_round: Account<'info, GameRound>,        /// CHECK: This is the vault PDA that holds game funds    #[account(        mut,        seeds = [VAULT_SEED],        bump    )]    pub vault: UncheckedAccount<'info>,        #[account(mut)]    pub player: Signer<'info>,        pub system_program: Program<'info, System>,} pub fn deposit_bet(    ctx: Context<DepositBet>,    amount: u64,) -> Result<()> {    let game_round = &mut ctx.accounts.game_round;    let player_key = ctx.accounts.player.key();    let clock = Clock::get()?;
  1. Line 19 seeds = [VAULT_SEED],: Declares the PDA seeds. Anchor re-derives the address and rejects the account if it doesn't match.
  2. Line 20 bump: Uses the bump seed, the extra byte that pushes the derived address off the ed25519 curve.
  3. Line 25 pub player: Signer<'info>,: Requires this account to have signed the transaction.
  4. Line 36 let clock = Clock::get()?;: Reads on-chain time from the Clock sysvar.

How to run

No package.json, Anchor.toml, Cargo.toml, go.mod or Makefile was found near the root. See the project README.

What you could build from it