使用说明

严格游戏

启发式框架展示：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<Setup> = Game::new();

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

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

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

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<InProgress>) -> Result<(), MoveError> {
        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<InProgress>) -> Result<(), MoveError> {
        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<Phase> {
    board: Board,
    history: Vec<Move>,
    phase_data: Phase,  // Phase-specific data
}

// Setup phase: no current player yet
impl Game<Setup> {
    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<InProgress> {
        Game {
            board: self.board,
            history: self.history,
            phase_data: InProgress { to_move: first_player },
        }
    }
}

// InProgress phase: has current player
impl Game<InProgress> {
    /// 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<MoveResult, MoveError> {
        // 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<InProgress>) -> Result<(), MoveError> {
        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<InProgress>) -> Result<(), MoveError> {
        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<InProgress>) -> Result<(), MoveError> {
        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<InProgress>) -> Result<(), MoveError> {
        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 << 'EOF'
{
  "mcpServers": {
    "strictly-games": {
      "command": "/absolute/path/to/strictly_games/target/release/strictly_games",
      "args": [],
      "env": {}
    }
  }
}
EOF

# Then run copilot normally
copilot

或者使用命令行标志进行一次性使用：

# From the project directory
cd /path/to/strictly_games

# Pass config as JSON
copilot --additional-mcp-config '{"mcpServers":{"strictly-games":{"command":"'$(pwd)'/target/release/strictly_games","args":[],"env":{}}}}'

# Or from a file
copilot --additional-mcp-config @mcp-config.json

示例配置文件 (mcp-config.json):

{
  "mcpServers": {
    "strictly-games": {
      "command": "/home/user/strictly_games/target/release/strictly_games",
      "args": [],
      "env": {}
    }
  }
}

VS代码集成

对于VS代码，添加到 .vscode/settings.json 在您的工作空间中：

{
  "github.copilot.chat.mcp.servers": {
    "strictly-games": {
      "command": "/path/to/strictly_games/target/release/strictly_games"
    }
  }
}

终端用户界面（TUI）

TUI提供了一个交互式终端界面来对抗AI代理。

独立模式（推荐）

尝试该系统的最简单方法是自动生成服务器和AI代理：

cargo run tui

控制：

方向键：移动光标
进入：放置移动
q：退出
r：重新启动游戏

TUI自动：

在端口3000上生成HTTP游戏服务器
生成连接到服务器的AI代理
作为人类玩家连接
退出时清理子流程

远程模式

连接到现有服务器：

# Terminal 1: Start server
cargo run http --port 3000

# Terminal 2: Start AI agent
cargo run agent --server-url http://localhost:3000 --test-play

# Terminal 3: Start TUI
cargo run tui --server-url http://localhost:3000

这展示了分布式架构：TUI、服务器和代理都独立运行。

玩Tic Tac脚趾

连接后，请Claude或Copilot玩：

You: Let's play tic-tac-toe!

Claude: I'll start a new game.
[calls start_game tool]

New game started!
1|2|3
-+-+-
4|5|6
-+-+-
7|8|9

I'll play X in the center.
[calls make_move with position: 4]

Move accepted. Player O to move.
1|2|3
-+-+-
4|X|6
-+-+-
7|8|9

可用工具

start_game

开始一个新的井字游戏
玩家X先走
返回空板

make_move

论据： position （0-8，其中0=左上角，8=右下角）
验证移动（方块必须为空，游戏正在进行中）
返回更新的棋盘和游戏状态
例子： {"position": 4} 玩中心广场

get_board

返回当前板状态
显示当前玩家、游戏状态、移动次数

电路板设计

职位编号为0-8：

0|1|2
-+-+-
3|4|5
-+-+-
6|7|8

用数字表示空白方块，X/O表示已占用：

X|O|3
-+-+-
X|5|O
-+-+-
7|8|9

发展

# Build the project
cargo build

# Run with debug logging
RUST_LOG=strictly_games=debug,elicitation=debug cargo run

# Run tests
cargo test

# Run with all features (requires OpenCV, Tesseract)
cargo build --all-features

# Run justfile recipes
just check          # Compile only
just test-package   # Test this package
just check-all      # Full check (clippy, fmt, test)

贡献

我们欢迎展示以下内容的贡献 验证优先开发:

设计域类型 使无效州无法代表
添加合同 以声明方式编码规则
撰写合同 构建复杂的验证
写Kani证明 验证正确性
通过MCP曝光 用于代理交互

有关模式，请参阅现有游戏。所有代码都必须遵循上述架构原则。

依赖项

引出 -类型安全诱导和MCP集成
rmcp -模型上下文协议实现
东京 -异步运行时
追踪 -结构化日志记录

路线图

第一阶段：基础 （当前）

✅ 基本MCP服务器基础设施
✅ 带移动验证的Tic tac脚趾
✅ 通过跟踪实现完全可观察性

第二阶段：合同

添加经Kani验证的搬家合法性合同
演示携带验证码的模式
复杂作业的合同构成

第三阶段：扩展游戏

二十一点（概率验证）
跳棋（游戏树搜索）
国际象棋（复杂状态空间）

第四阶段：启发式整合

互动游戏配置
锦标赛组织
战略启发

哲学

激励框架基于三个原则：

1.使非法国家失去形象

// ❌ Traditional: Positions are numbers (what if user enters 10?)
type Position = u8;  // 0-255... but only 0-8 valid!

// ✅ Elicitation: Positions are an enum
enum Position { TopLeft, ..., BottomRight }  // Only 9 exist!

2.验证是组成

// ❌ Traditional: Validation is imperative spaghetti
fn validate_move(mov: Move, game: Game) -> 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<InProgress>) -> Result<(), MoveError> {
        SquareIsEmpty::check(mov, game)?;
        PlayersTurn::check(mov, game)?;
        Ok(())
    }
}

3.类型是证据

// If you have Game<Finished>, the game IS finished
// If you have Game<InProgress>, 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<Phase> 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许可证(许可证-麻省理工学院)

由您选择。

致谢

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

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

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