快速接入

先看主来源和安装命令，再打开仓库或文档；下面只保留这个条目的关键接入事实。

详细介绍

严格游戏

启发式框架展示：LLM代理的类型安全游戏

艺术正在将混乱转化为形式，这就是游戏。游戏有规则。——斯蒂芬·桑德海姆

Strictly Games展示了激励框架在行动中——展示如何构建 类型安全操作语义 使代理行为无效 不可靠的 在类型层面。

为什么这很重要

传统方法：

Prompt: "Only make legal moves in tic-tac-toe"
Reality: Agent tries position 10 (doesn't exist) or places X on occupied square
Fix: Better prompts, few-shot examples, RLHF

激发方法：

// Positions are an enum - position 10 doesn't exist
pub enum Position { TopLeft, TopCenter, ... }

// Moves validated by contracts before application
SquareIsEmpty::check(&action, &game)?;
PlayersTurn::check(&action, &game)?;

// Invalid moves don't compile, can't be represented

我们没有建立更好的提示。我们正在构建使正确性不可避免的类型系统。

启发式架构

这个代码库展示了Elicitation框架的四个关键模式：

1. 类型状态机

游戏阶段以类型参数编码，使得非法状态转换成为不可能：

// Phase encoded as type parameter
let game: Game = Game::new();

// start() consumes Setup, returns InProgress
let game: Game = game.start(Player::X);

// make_move() consumes InProgress, returns InProgress or Finished
let result: MoveResult = game.make_move(action)?;

无效转换不存在：您无法调用 make_move() 上 Game 或 restart() 上 Game.

2. 一级诉讼

域事件（移动）在应用程序之前独立验证：

// Actions are domain types with validation
let action = Move::new(Player::X, Position::Center);

// Contract-based validation (declarative, composable)
LegalMove::check(&action, &game)?;

// Apply validated action
let result = game.make_move(action)?;

动作有自己的语义——它们不仅仅是数据 携带证明的代码.

3. 合同驱动的验证

规则是声明性契约，而不是强制性检查：

/// Precondition: Square must be empty
pub struct SquareIsEmpty;

impl SquareIsEmpty {
    pub fn check(mov: &Move, game: &Game) -> Result {
        if !game.board().is_empty(mov.position) {
            Err(MoveError::SquareOccupied(mov.position))
        } else {
            Ok(())
        }
    }
}

// Compose contracts
pub struct LegalMove;

impl LegalMove {
    pub fn check(mov: &Move, game: &Game) -> Result {
        SquareIsEmpty::check(mov, game)?;
        PlayersTurn::check(mov, game)?;
        Ok(())
    }
}

合同包括：

声明式 -说明什么必须是真实的，而不是如何检查
可组合 -由简单规则构建的复杂规则
可验证的 -可以用Kani/Creusot正式证明
可重复使用的 -相同的合同适用于各种游戏变体

4. 干净的边界

域逻辑是纯粹的——没有表示，没有I/O，没有框架耦合：

// Domain types know nothing about:
// - How they're rendered (terminal? GUI? web?)
// - How moves arrive (MCP? HTTP? keyboard?)
// - Where state is stored (memory? database?)

// This makes them:
// - Testable in isolation
// - Reusable across contexts
// - Formally verifiable
// - Framework-agnostic

游戏逻辑是 纯变换--从一个有效的状态到另一个有效状态，合同强制执行合法性。

教程：实现类型安全游戏

让我们通过tic-tac-toe实现来了解这些模式的实际应用。

步骤1：定义域类型

从不可约域概念开始：

// Players are an enum - only two exist
#[derive(Debug, Clone, Copy, PartialEq, Eq, Elicit)]
pub enum Player { X, O }

// Positions are bounded - only 9 valid squares
#[derive(Debug, Clone, Copy, PartialEq, Eq, Elicit)]
pub enum Position {
    TopLeft, TopCenter, TopRight,
    MiddleLeft, Center, MiddleRight,
    BottomLeft, BottomCenter, BottomRight,
}

// Square state encodes occupancy
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Square {
    Empty,
    Occupied(Player),
}

关键见解： 无效位置（如10或-1） 不存在--它们在类型中无法表示。

步骤2：构建复合类型

将图元组合成更高级别的结构：

// Board is array of squares
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Board {
    squares: [Square; 9],
}

impl Board {
    /// Check if position is empty
    pub fn is_empty(&self, pos: Position) -> bool {
        matches!(self.squares[pos as usize], Square::Empty)
    }
    
    /// Place a mark
    pub fn place(&mut self, pos: Position, player: Player) {
        self.squares[pos as usize] = Square::Occupied(player);
    }
}

步骤3：定义阶段标记

创建零大小的类型来编码游戏阶段：

/// Phase marker: Game is being set up
pub struct Setup;

/// Phase marker: Game is in progress
pub struct InProgress;

/// Phase marker: Game has finished
pub struct Finished;

/// Outcome of finished game
pub enum Outcome {
    Winner(Player),
    Draw,
}

步骤4：实现类型状态游戏

游戏结构在阶段上是通用的：

/// Type-safe game with phase encoded as type parameter
pub struct Game
 {
    board: Board,
    history: Vec,
    phase_data: Phase,  // Phase-specific data
}

// Setup phase: no current player yet
impl Game {
    pub fn new() -> Self {
        Self {
            board: Board::empty(),
            history: Vec::new(),
            phase_data: Setup,
        }
    }
    
    /// Transition: Setup → InProgress
    pub fn start(self, first_player: Player) -> Game {
        Game {
            board: self.board,
            history: self.history,
            phase_data: InProgress { to_move: first_player },
        }
    }
}

// InProgress phase: has current player
impl Game {
    /// Who moves next?
    pub fn to_move(&self) -> Player {
        self.phase_data.to_move
    }
    
    /// Attempt move - may transition to Finished
    pub fn make_move(mut self, action: Move) -> Result {
        // Validate via contracts (see Step 5)
        LegalMove::check(&action, &self)?;
        
        // Apply move
        self.board.place(action.position, action.player);
        self.history.push(action);
        
        // Check for game end
        if let Some(outcome) = self.check_outcome() {
            Ok(MoveResult::Finished(Game {
                board: self.board,
                history: self.history,
                phase_data: Finished { outcome },
            }))
        } else {
            // Toggle player
            self.phase_data.to_move = self.phase_data.to_move.opponent();
            Ok(MoveResult::Continue(self))
        }
    }
}

关键见解： make_move() 消耗 self--你不能意外地重用过时的游戏状态。

步骤5：定义合同

零大小结构类型的声明性规则：

/// Contract: Square must be empty
pub struct SquareIsEmpty;

impl SquareIsEmpty {
    pub fn check(mov: &Move, game: &Game) -> Result {
        if !game.board().is_empty(mov.position) {
            Err(MoveError::SquareOccupied(mov.position))
        } else {
            Ok(())
        }
    }
}

/// Contract: Must be player's turn
pub struct PlayersTurn;

impl PlayersTurn {
    pub fn check(mov: &Move, game: &Game) -> Result {
        if mov.player != game.to_move() {
            Err(MoveError::WrongPlayer { expected: game.to_move(), got: mov.player })
        } else {
            Ok(())
        }
    }
}

/// Composite contract: Move is legal
pub struct LegalMove;

impl LegalMove {
    pub fn check(mov: &Move, game: &Game) -> Result {
        SquareIsEmpty::check(mov, game)?;
        PlayersTurn::check(mov, game)?;
        Ok(())
    }
}

第6步：定义行动

移动是域事件，而不仅仅是数据：

/// A move action
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct Move {
    pub player: Player,
    pub position: Position,
}

impl Move {
    pub fn new(player: Player, position: Position) -> Self {
        Self { player, position }
    }
}

/// Move validation error
#[derive(Debug, Clone, Display, Error)]
pub enum MoveError {
    #[display("Square {} is occupied", _0)]
    SquareOccupied(Position),
    
    #[display("Wrong player: expected {:?}, got {:?}", expected, got)]
    WrongPlayer { expected: Player, got: Player },
}

步骤7：正式验证（已经完成！）

你不写Kani证明。你已经通过作文进行了正式的验证。

通过使用 #[derive(Elicit)] 在您的域类型上，您继承了Elicitation Framework的 321份经过验证的合同:

#[derive(Debug, Clone, Copy, PartialEq, Eq, Elicit)]
pub enum Position {
    TopLeft, TopCenter, TopRight,
    MiddleLeft, Center, MiddleRight,
    BottomLeft, BottomCenter, BottomRight,
}

这给了你什么（由Kani在启发式框架中证明）：

✅ 选择返回值验证变量 -代理人只能退回9个职位中的一个\ ✅ 选择排气空间 -所有9个位置都是可枚举的\ ✅ 选择性喷油器 -职位→ 索引映射为1:1\ ✅ FiniteDomain -位置空间是有界的（正好有9个元素）\ ✅ 无无效状态 -位置10不存在，无法构建

组合验证：

// Position is verified (via Elicitation)
// Player is verified (via Elicitation)
// Therefore Move is verified (composition preserves properties)
pub struct Move {
    pub player: Player,    // ✅ Verified
    pub position: Position, // ✅ Verified
}

// Contracts on verified types = verified system
impl LegalMove {
    pub fn check(mov: &Move, game: &Game) -> Result {
        SquareIsEmpty::check(mov, game)?;    // Contract on verified type
        PlayersTurn::check(mov, game)?;      // Contract on verified type
        Ok(())
    }
}

形式验证的温暖毯通过组合推理延伸到你的整个游戏中。

不需要Kani设置。没有可供书写的校对工具。无验证时间。通过使用框架的已验证原语，您可以免费获得它。

看 FORMAL_VERIFICATION.md 完整解释继承的验证保证。

安装

# Clone the repository
git clone https://github.com/crumplecup/strictly_games.git
cd strictly_games

# Build the server
cargo build --release

运行服务器

服务器使用MCP协议通过stdin/stdout进行通信：

# Run directly
cargo run

# Or use the built binary
./target/release/strictly_games

服务器将启动并等待stdin上的MCP消息。您将看到：

Starting Strictly Games MCP server
Server ready - connect via MCP protocol

连接到克劳德桌面

添加到您的Claude Desktop MCP配置(claude_desktop_config.json):

{
  "mcpServers": {
    "strictly-games": {
      "command": "/path/to/strictly_games/target/release/strictly_games"
    }
  }
}

在macOS上：

# Edit config
code ~/Library/Application\ Support/Claude/claude_desktop_config.json

# Restart Claude Desktop

在Linux上：

# Edit config
code ~/.config/Claude/claude_desktop_config.json

# Restart Claude Desktop

连接到GitHub Copilot CLI

GitHub Copilot CLI在以下位置使用配置文件 ~/.copilot/mcp-config.json:

# Create/edit the config file
cat > ~/.copilot/mcp-config.json  bool {
    if game.board[mov.pos] != Empty { return false; }
    if mov.player != game.current_player { return false; }
    if game.is_finished { return false; }
    true
}

// ✅ Elicitation: Validation is declarative contracts
impl LegalMove {
    fn check(mov: &Move, game: &Game) -> Result {
        SquareIsEmpty::check(mov, game)?;
        PlayersTurn::check(mov, game)?;
        Ok(())
    }
}

3.类型是证据

// If you have Game, the game IS finished
// If you have Game, moves ARE legal
// If you have Move that passed LegalMove::check, it IS valid

// The type system is your proof system

益处

对于代理商

更少的幻觉 -无效的动作不存在产生幻觉
更好的理解 -以类型编码的域结构
更清晰的错误 -带有上下文的类型安全错误

对于开发者

施工正确性 -无效状态无法表示
重塑信心 -编译器检查规则更改
形式验证 -Kani证明保证属性
可再用元件 -合同由游戏组成

用于系统设计

可测试性 -纯函数，确定性
可维护性 -类型签名是文档
可进化性 -在不破坏不变量的情况下添加特征

路线图

第一阶段：基础 （当前）

✅ 类型状态机（tic-tac-toe）
✅ 基于合同的验证
✅ 一级诉讼
✅ MCP集成

第二阶段：验证

为合同添加Kani证明
演示证明成分
文档验证模式

第三阶段：扩展游戏

二十一点（概率状态）
Checkers（更大的状态空间）
国际象棋（复杂规则）

第四阶段：启发式深潜

通过启发进行互动游戏配置
锦标赛组织
战略启发与比较

代码结构

该实现展示了干净的分离：

src/games/tictactoe/
├── position.rs       # Domain primitive: Position enum
├── types.rs          # Core types: Player, Square, Board
├── phases.rs         # Phase markers: Setup, InProgress, Finished
├── action.rs         # Domain events: Move, MoveError
├── contracts.rs      # Validation: SquareIsEmpty, PlayersTurn, LegalMove
├── typestate.rs      # State machine: Game
 with transitions
├── wrapper.rs        # Type-erased wrapper for runtime polymorphism
└── mod.rs           # Public API and documentation

导航指南

从types.rs开始 -查看域图元（Player、Square、Board）
读取phases.rs -了解状态机阶段
研究合同 -请参阅声明性验证
探索typestate.rs -查看类型如何强制转换
检查包装器.rs -使用AnyGame学习运行时多态性

每个文件都包含大量文档。

许可证

根据以下任一方式获得许可：

Apache许可证，版本2.0(特许通行证)
MIT许可证(许可证-麻省理工学院)

由您选择。

致谢

与引出框架，证明类型安全代理交互在当今是实用且可实现的。

______________________________________________________________________

“我们正在为代理构建类型安全的操作语义，而不是更好的提示。”

关键见解： 防止代理人犯错的最好方法就是犯错 无法代表 在类型系统中。这就是启发式框架。

目录标签

类型安全RustClaude本地部署游戏框架代理交互规则验证形式化验证

支持客户端

Claude DesktopClaude

接入字段

传输方式（transport，传输协议）

未说明

鉴权方式（authType，认证方式）

none

工具数量（toolCount，工具数）

3

资源数量（resourceCount，资源数）

0

提示词数量（promptCount，提示词数）

0

权限和风险

未说明none部署方式未说明

接入前请确认传输方式、认证方式和部署位置，并根据实际工具能力限制访问范围。

安装前确认

不要直接授予不必要的文件、网络或账号权限；先核对安装命令和配置内容。

仍需确认：installCommand

来源信息

MCP World

mcpworld.com

/detail/64ff41e46113c8d60a3b5632df001192

一个基于类型系统的游戏框架，通过类型安全的设计使无效的代理行为在类型层面上不可表示，适用于构建规则明确的游戏和代理交互。

继续浏览同类 MCP

更多安全风控 MCP（3,600）返回 MCP 目录

上一个 MCP

Strava MCP Fbc42bdd

一个用于与Strava API集成的模型上下文协议（MCP）服务器，提供对活动、运动员数据、路线、路段、俱乐部和装备等主要Strava API端点的全面访问。

下一个 MCP

Stripe Ad5e97ee

The Stripe Model Context Protocol server allows you to integrate with Stripe APIs through function calling. This protocol supports various tools to interact with different Stripe services.

strictly games