Merge branch 'dev' into unify-logs

benchmarks/run-formal-eval.ts

@@ -0,0 +1,153 @@
+import "dotenv/config";
+import { readFileSync, writeFileSync, existsSync } from "node:fs";
+import { resolve } from "node:path";
+import { coderAgent } from "../src/agents/coder/agent.ts";
+
+// ─── Config ────────────────────────────────────────────────────────────────────
+const FORMAL_EVAL_PATH =
+  process.env.FORMAL_EVAL_PATH ??
+  resolve("..", "formal-eval", "data", "FormalEval.jsonl");
+
+const OUTPUT_PATH = process.env.BENCHMARK_OUTPUT ?? resolve("benchmarks", "samples.jsonl");
+const SAMPLES_PER_TASK = Number(process.env.SAMPLES_PER_TASK ?? "1");
+const SKIP_REVIEW = process.env.SKIP_REVIEW !== "false"; // skip review by default for speed
+
+// ─── Types ─────────────────────────────────────────────────────────────────────
+interface FormalEvalProblem {
+  task_id: string;
+  complexity: string;
+  description: string;
+  prompt: string;
+  canonical_solution: string;
+  test: string;
+  entry_point: string;
+}
+
+interface SampleOutput {
+  task_id: string;
+  completion: string;
+}
+
+// ─── Helpers ───────────────────────────────────────────────────────────────────
+
+function readProblems(path: string): FormalEvalProblem[] {
+  const content = readFileSync(path, "utf-8");
+  return content
+    .split("\n")
+    .filter((line) => line.trim())
+    .map((line) => JSON.parse(line));
+}
+
+/**
+ * Extrai a "completion" (body do contrato) a partir do contrato completo gerado.
+ * O FormalEval espera: prompt + completion = contrato completo.
+ * Então precisamos remover tudo que já está no prompt.
+ */
+function extractCompletion(generatedContract: string, prompt: string): string {
+  // Estratégia 1: Se o contrato gerado contém o prompt exato, pegar o que vem depois
+  const promptTrimmed = prompt.trimEnd();
+  const idx = generatedContract.indexOf(promptTrimmed);
+  if (idx !== -1) {
+    return generatedContract.slice(idx + promptTrimmed.length);
+  }
+
+  // Estratégia 2: Encontrar a declaração "contract <Name> {" e pegar o body
+  // O prompt sempre termina com "contract <Name> {\n"
+  const contractDeclMatch = prompt.match(/contract\s+(\w+)\s*\{?\s*$/m);
+  if (contractDeclMatch) {
+    const contractName = contractDeclMatch[1];
+    const pattern = new RegExp(`contract\\s+${contractName}\\s*\\{`);
+    const match = generatedContract.match(pattern);
+    if (match?.index !== undefined) {
+      const afterDecl = generatedContract.slice(match.index + match[0].length);
+      return afterDecl;
+    }
+  }
+
+  // Estratégia 3: Fallback — Tenta remover pragma + imports + declaração até "{"
+  const lines = generatedContract.split("\n");
+  let bodyStart = 0;
+  for (let i = 0; i < lines.length; i++) {
+    if (lines[i].match(/contract\s+\w+.*\{/)) {
+      bodyStart = i + 1;
+      break;
+    }
+  }
+  return lines.slice(bodyStart).join("\n");
+}
+
+/**
+ * Adapta o prompt do FormalEval para ser interpretado pelo Coder Agent.
+ * Inclui instrução explícita para gerar apenas o body.
+ */
+function buildRequirements(problem: FormalEvalProblem): string {
+  return `Complete the following Solidity contract. Generate ONLY the contract body (state variables, functions, and closing brace "}").
+Do NOT include the SPDX license, pragma, or contract declaration — they are already provided.
+The code must compile with solc ^0.8.19.
+
+Here is the contract declaration with its specification:
+
+${problem.prompt}
+
+IMPORTANT: Return ONLY the code that goes INSIDE the contract (after the opening brace). Include the closing "}" at the end.`;
+}
+
+// ─── Main ──────────────────────────────────────────────────────────────────────
+
+async function main() {
+  if (!existsSync(FORMAL_EVAL_PATH)) {
+    console.error(`FormalEval dataset not found at: ${FORMAL_EVAL_PATH}`);
+    console.error("Set FORMAL_EVAL_PATH env variable to the correct path.");
+    process.exit(1);
+  }
+
+  const problems = readProblems(FORMAL_EVAL_PATH);
+  console.log(`Loaded ${problems.length} problems from FormalEval`);
+  console.log(`Generating ${SAMPLES_PER_TASK} sample(s) per task...`);
+  console.log(`Output: ${OUTPUT_PATH}\n`);
+
+  const samples: SampleOutput[] = [];
+  let completed = 0;
+
+  for (const problem of problems) {
+    for (let s = 0; s < SAMPLES_PER_TASK; s++) {
+      const label = `[${problem.task_id}] (${problem.complexity}) sample ${s + 1}/${SAMPLES_PER_TASK}`;
+      console.log(`→ ${label}: ${problem.description}`);
+
+      try {
+        const requirements = buildRequirements(problem);
+        const result = await coderAgent.invoke({ requirements: [requirements] });
+
+        const generated = result.contract;
+        const completion = extractCompletion(generated, problem.prompt);
+
+        samples.push({ task_id: problem.task_id, completion });
+
+        const hasErrors = result.compilationErrors.length > 0;
+        console.log(`  ✓ Done${hasErrors ? ` (with ${result.compilationErrors.length} compile errors)` : ""}`);
+      } catch (error) {
+        const msg = error instanceof Error ? error.message : String(error);
+        console.error(`  ✗ Failed: ${msg}`);
+        // Still emit an empty completion so FormalEval doesn't complain about missing tasks
+        samples.push({ task_id: problem.task_id, completion: "// generation failed\n}\n" });
+      }
+
+      completed++;
+    }
+  }
+
+  // Write JSONL output
+  const jsonl = samples.map((s) => JSON.stringify(s)).join("\n") + "\n";
+  writeFileSync(OUTPUT_PATH, jsonl, "utf-8");
+
+  console.log(`\n${"═".repeat(60)}`);
+  console.log(`Benchmark complete: ${completed} completions generated`);
+  console.log(`Output saved to: ${OUTPUT_PATH}`);
+  console.log(`\nTo evaluate, run:`);
+  console.log(`  cd ../formal-eval && evaluate_formal_correctness ${resolve(OUTPUT_PATH)}`);
+}
+
+main().catch((err) => {
+  console.error("Fatal error:", err);
+  process.exit(1);
+});

benchmarks/samples.jsonl

@@ -0,0 +1,45 @@
+{"task_id":"FormalEval/0","completion":"    uint256 private storedValue;\n    address public owner;\n    bool private locked;\n\n    event ValueStored(uint256 indexed newValue, address indexed sender);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the contract owner\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n        storedValue = 0;\n    }\n\n    /// @notice Stores a new value in the contract\n    /// @param _value The value to be stored\n    function store(uint256 _value) public onlyOwner nonReentrant {\n        storedValue = _value;\n        emit ValueStored(_value, msg.sender);\n    }\n\n    /// @notice Retrieves the currently stored value\n    /// @return The stored uint256 value\n    function retrieve() public view returns (uint256) {\n        return storedValue;\n    }\n}"}
+{"task_id":"FormalEval/0","completion":"    uint256 private storedValue;\n    address public owner;\n    bool private locked;\n\n    event ValueStored(uint256 indexed newValue, address indexed sender);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the contract owner\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n        storedValue = 0;\n    }\n\n    /// @notice Stores a new value in the contract\n    /// @param _value The value to be stored\n    function store(uint256 _value) public onlyOwner nonReentrant {\n        storedValue = _value;\n        emit ValueStored(_value, msg.sender);\n    }\n\n    /// @notice Retrieves the currently stored value\n    /// @return The stored uint256 value\n    function retrieve() public view returns (uint256) {\n        return storedValue;\n    }\n}"}
+{"task_id":"FormalEval/0","completion":"    uint256 private storedValue;\n    address private immutable owner;\n\n    event ValueStored(uint256 indexed newValue, address indexed sender);\n\n    error Unauthorized();\n\n    modifier onlyOwner() {\n        if (msg.sender != owner) revert Unauthorized();\n        _;\n    }\n\n    constructor() {\n        owner = msg.sender;\n        storedValue = 0;\n    }\n\n    /// @notice Stores a new value in the contract\n    /// @param _value The uint256 value to be stored\n    function store(uint256 _value) external {\n        storedValue = _value;\n        emit ValueStored(_value, msg.sender);\n    }\n\n    /// @notice Retrieves the currently stored value\n    /// @return The current uint256 value\n    function retrieve() external view returns (uint256) {\n        return storedValue;\n    }\n}"}
+{"task_id":"FormalEval/1","completion":"\n    uint256 private count;\n    bool private locked;\n\n    event CounterIncremented(uint256 newValue);\n    event CounterDecremented(uint256 newValue);\n\n    modifier noReentrancy() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        count = 0;\n        locked = false;\n    }\n\n    /// @notice Increases the counter by 1\n    function increment() external noReentrancy {\n        count += 1;\n        emit CounterIncremented(count);\n    }\n\n    /// @notice Decreases the counter by 1\n    /// @dev Reverts if the counter is 0 to prevent underflow\n    function decrement() external noReentrancy {\n        require(count > 0, \"Counter: cannot decrement below zero\");\n        count -= 1;\n        emit CounterDecremented(count);\n    }\n\n    /// @notice Returns the current counter value\n    /// @return The current count\n    function getCount() external view returns (uint256) {\n        return count;\n    }\n}"}
+{"task_id":"FormalEval/1","completion":"\n    uint256 private count;\n    bool private locked;\n\n    event Incremented(uint256 newValue);\n    event Decremented(uint256 newValue);\n\n    modifier noReentrancy() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        count = 0;\n        locked = false;\n    }\n\n    /// @notice Increases the counter by 1\n    function increment() external noReentrancy {\n        count += 1;\n        emit Incremented(count);\n    }\n\n    /// @notice Decreases the counter by 1\n    /// @dev Reverts if the counter is already 0\n    function decrement() external noReentrancy {\n        require(count > 0, \"Counter: cannot decrement below zero\");\n        count -= 1;\n        emit Decremented(count);\n    }\n\n    /// @notice Returns the current counter value\n    /// @return The current count\n    function getCount() external view returns (uint256) {\n        return count;\n    }\n}"}
+{"task_id":"FormalEval/1","completion":"\n    uint256 private count;\n    bool private locked;\n\n    event Incremented(uint256 newValue);\n    event Decremented(uint256 newValue);\n\n    modifier noReentrancy() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        count = 0;\n        locked = false;\n    }\n\n    /// @notice Increases the counter by 1\n    function increment() external noReentrancy {\n        count += 1;\n        emit Incremented(count);\n    }\n\n    /// @notice Decreases the counter by 1\n    /// @dev Reverts if the counter is 0 to prevent underflow\n    function decrement() external noReentrancy {\n        require(count > 0, \"Counter: cannot decrement below 0\");\n        count -= 1;\n        emit Decremented(count);\n    }\n\n    /// @notice Returns the current counter value\n    /// @return The current count\n    function getCount() external view returns (uint256) {\n        return count;\n    }\n}"}
+{"task_id":"FormalEval/2","completion":"\n    /// @notice Event emitted when an addition is performed\n    event Addition(uint256 a, uint256 b, uint256 result);\n    /// @notice Event emitted when a subtraction is performed\n    event Subtraction(uint256 a, uint256 b, uint256 result);\n    /// @notice Event emitted when a multiplication is performed\n    event Multiplication(uint256 a, uint256 b, uint256 result);\n    /// @notice Event emitted when a division is performed\n    event Division(uint256 a, uint256 b, uint256 result);\n\n    /// @notice Adds two numbers\n    /// @param a First number\n    /// @param b Second number\n    /// @return result The sum of a and b\n    function add(uint256 a, uint256 b) external returns (uint256 result) {\n        result = a + b;\n        emit Addition(a, b, result);\n    }\n\n    /// @notice Subtracts b from a\n    /// @param a Minuend\n    /// @param b Subtrahend\n    /// @return result The difference of a and b\n    function subtract(uint256 a, uint256 b) external returns (uint256 result) {\n        require(a >= b, \"Calculator: subtraction result would be negative\");\n        result = a - b;\n        emit Subtraction(a, b, result);\n    }\n\n    /// @notice Multiplies two numbers\n    /// @param a First number\n    /// @param b Second number\n    /// @return result The product of a and b\n    function multiply(uint256 a, uint256 b) external returns (uint256 result) {\n        result = a * b;\n        emit Multiplication(a, b, result);\n    }\n\n    /// @notice Divides a by b\n    /// @param a Dividend\n    /// @param b Divisor\n    /// @return result The quotient of a and b\n    function divide(uint256 a, uint256 b) external returns (uint256 result) {\n        require(b != 0, \"Calculator: division by zero\");\n        result = a / b;\n        emit Division(a, b, result);\n    }\n}"}
+{"task_id":"FormalEval/2","completion":"\n    /// @notice Event emitted when an addition is performed\n    event Addition(uint256 a, uint256 b, uint256 result);\n    /// @notice Event emitted when a subtraction is performed\n    event Subtraction(uint256 a, uint256 b, uint256 result);\n    /// @notice Event emitted when a multiplication is performed\n    event Multiplication(uint256 a, uint256 b, uint256 result);\n    /// @notice Event emitted when a division is performed\n    event Division(uint256 a, uint256 b, uint256 result);\n\n    /// @notice Adds two numbers\n    /// @param a First operand\n    /// @param b Second operand\n    /// @return result The sum of a and b\n    function add(uint256 a, uint256 b) external returns (uint256 result) {\n        result = a + b;\n        emit Addition(a, b, result);\n    }\n\n    /// @notice Subtracts b from a\n    /// @param a First operand\n    /// @param b Second operand\n    /// @return result The difference of a and b\n    function subtract(uint256 a, uint256 b) external returns (uint256 result) {\n        require(a >= b, \"Calculator: subtraction underflow\");\n        result = a - b;\n        emit Subtraction(a, b, result);\n    }\n\n    /// @notice Multiplies two numbers\n    /// @param a First operand\n    /// @param b Second operand\n    /// @return result The product of a and b\n    function multiply(uint256 a, uint256 b) external returns (uint256 result) {\n        result = a * b;\n        emit Multiplication(a, b, result);\n    }\n\n    /// @notice Divides a by b\n    /// @param a First operand\n    /// @param b Second operand\n    /// @return result The quotient of a divided by b\n    function divide(uint256 a, uint256 b) external returns (uint256 result) {\n        require(b != 0, \"Calculator: division by zero\");\n        result = a / b;\n        emit Division(a, b, result);\n    }\n}"}
+{"task_id":"FormalEval/2","completion":"\n    /// @notice Event emitted when an addition is performed\n    event Addition(uint256 a, uint256 b, uint256 result);\n\n    /// @notice Event emitted when a subtraction is performed\n    event Subtraction(uint256 a, uint256 b, uint256 result);\n\n    /// @notice Event emitted when a multiplication is performed\n    event Multiplication(uint256 a, uint256 b, uint256 result);\n\n    /// @notice Event emitted when a division is performed\n    event Division(uint256 a, uint256 b, uint256 result);\n\n    /// @notice Adds two numbers\n    /// @param a First operand\n    /// @param b Second operand\n    /// @return The sum of a and b\n    function add(uint256 a, uint256 b) external returns (uint256) {\n        uint256 result = a + b;\n        emit Addition(a, b, result);\n        return result;\n    }\n\n    /// @notice Subtracts b from a\n    /// @param a First operand\n    /// @param b Second operand\n    /// @return The difference of a and b\n    /// @dev Reverts if b > a to prevent underflow\n    function subtract(uint256 a, uint256 b) external returns (uint256) {\n        require(a >= b, \"Calculator: subtraction result would be negative\");\n        uint256 result = a - b;\n        emit Subtraction(a, b, result);\n        return result;\n    }\n\n    /// @notice Multiplies two numbers\n    /// @param a First operand\n    /// @param b Second operand\n    /// @return The product of a and b\n    function multiply(uint256 a, uint256 b) external returns (uint256) {\n        uint256 result = a * b;\n        emit Multiplication(a, b, result);\n        return result;\n    }\n\n    /// @notice Divides a by b\n    /// @param a First operand\n    /// @param b Second operand\n    /// @return The quotient of a and b\n    /// @dev Reverts if b is 0\n    function divide(uint256 a, uint256 b) external returns (uint256) {\n        require(b != 0, \"Calculator: division by zero\");\n        uint256 result = a / b;\n        emit Division(a, b, result);\n        return result;\n    }\n}"}
+{"task_id":"FormalEval/3","completion":"    uint256[] private values;\n\n    /// @notice Event emitted when a new value is added to the array\n    event ValueAdded(uint256 value);\n\n    /// @notice Appends a value to the array\n    /// @param _value The value to be added\n    function push(uint256 _value) external {\n        values.push(_value);\n        emit ValueAdded(_value);\n    }\n\n    /// @notice Returns the minimum value in the array\n    /// @dev Reverts if the array is empty\n    /// @return min The smallest value found\n    function getMin() external view returns (uint256 min) {\n        require(values.length > 0, \"Array is empty\");\n        min = values[0];\n        for (uint256 i = 1; i < values.length; i++) {\n            if (values[i] < min) {\n                min = values[i];\n            }\n        }\n    }\n\n    /// @notice Returns the maximum value in the array\n    /// @dev Reverts if the array is empty\n    /// @return max The largest value found\n    function getMax() external view returns (uint256 max) {\n        require(values.length > 0, \"Array is empty\");\n        max = values[0];\n        for (uint256 i = 1; i < values.length; i++) {\n            if (values[i] > max) {\n                max = values[i];\n            }\n        }\n    }\n\n    /// @notice Returns the number of elements in the array\n    /// @return The length of the array\n    function getLength() external view returns (uint256) {\n        return values.length;\n    }\n}"}
+{"task_id":"FormalEval/3","completion":"    uint256[] private values;\n\n    /// @notice Event emitted when a new value is added\n    event ValueAdded(uint256 value);\n\n    /// @notice Appends a value to the array\n    /// @param _value The value to be added\n    function push(uint256 _value) external {\n        values.push(_value);\n        emit ValueAdded(_value);\n    }\n\n    /// @notice Returns the minimum value in the array\n    /// @return min The smallest value found\n    function getMin() external view returns (uint256 min) {\n        require(values.length > 0, \"Array is empty\");\n        min = values[0];\n        for (uint256 i = 1; i < values.length; i++) {\n            if (values[i] < min) {\n                min = values[i];\n            }\n        }\n    }\n\n    /// @notice Returns the maximum value in the array\n    /// @return max The largest value found\n    function getMax() external view returns (uint256 max) {\n        require(values.length > 0, \"Array is empty\");\n        max = values[0];\n        for (uint256 i = 1; i < values.length; i++) {\n            if (values[i] > max) {\n                max = values[i];\n            }\n        }\n    }\n\n    /// @notice Returns the number of elements in the array\n    /// @return length The total count of elements\n    function getLength() external view returns (uint256 length) {\n        return values.length;\n    }\n}"}
+{"task_id":"FormalEval/3","completion":"    uint256[] private values;\n\n    /// @notice Event emitted when a new value is added to the array\n    event ValueAdded(uint256 indexed value);\n\n    /// @notice Appends a value to the array\n    /// @param _value The value to be added\n    function push(uint256 _value) external {\n        values.push(_value);\n        emit ValueAdded(_value);\n    }\n\n    /// @notice Returns the minimum value in the array\n    /// @return min The smallest value found\n    function getMin() external view returns (uint256 min) {\n        require(values.length > 0, \"Array is empty\");\n        min = values[0];\n        for (uint256 i = 1; i < values.length; i++) {\n            if (values[i] < min) {\n                min = values[i];\n            }\n        }\n    }\n\n    /// @notice Returns the maximum value in the array\n    /// @return max The largest value found\n    function getMax() external view returns (uint256 max) {\n        require(values.length > 0, \"Array is empty\");\n        max = values[0];\n        for (uint256 i = 1; i < values.length; i++) {\n            if (values[i] > max) {\n                max = values[i];\n            }\n        }\n    }\n\n    /// @notice Returns the number of elements in the array\n    /// @return length The total count of elements\n    function getLength() external view returns (uint256 length) {\n        return values.length;\n    }\n}"}
+{"task_id":"FormalEval/4","completion":"    mapping(address => string) private _names;\n    mapping(address => bool) private _registered;\n\n    /// @notice Emitted when a new name is registered\n    event Registered(address indexed user, string name);\n\n    /// @notice Emitted when a registration is removed\n    event Unregistered(address indexed user);\n\n    /// @notice Registers the caller with a specific name\n    /// @param _name The name to associate with the sender's address\n    function register(string calldata _name) external {\n        require(bytes(_name).length > 0, \"Name cannot be empty\");\n        _names[msg.sender] = _name;\n        _registered[msg.sender] = true;\n        emit Registered(msg.sender, _name);\n    }\n\n    /// @notice Returns the name associated with an address\n    /// @param _addr The address to query\n    /// @return The registered name\n    function getName(address _addr) external view returns (string memory) {\n        return _names[_addr];\n    }\n\n    /// @notice Checks if an address is registered\n    /// @param _addr The address to check\n    /// @return True if registered, false otherwise\n    function isRegistered(address _addr) external view returns (bool) {\n        return _registered[_addr];\n    }\n\n    /// @notice Removes the registration for the caller\n    function unregister() external {\n        require(_registered[msg.sender], \"Address not registered\");\n        delete _names[msg.sender];\n        delete _registered[msg.sender];\n        emit Unregistered(msg.sender);\n    }\n}"}
+{"task_id":"FormalEval/4","completion":"    mapping(address => string) private _names;\n    mapping(address => bool) private _registered;\n\n    /// @notice Emitted when a new name is registered\n    event Registered(address indexed user, string name);\n\n    /// @notice Emitted when a registration is removed\n    event Unregistered(address indexed user);\n\n    /// @notice Registers the caller with a specific name\n    /// @param _name The name to associate with the sender's address\n    function register(string calldata _name) external {\n        require(bytes(_name).length > 0, \"Name cannot be empty\");\n        _names[msg.sender] = _name;\n        _registered[msg.sender] = true;\n        emit Registered(msg.sender, _name);\n    }\n\n    /// @notice Retrieves the name associated with an address\n    /// @param _addr The address to query\n    /// @return The registered name or an empty string\n    function getName(address _addr) external view returns (string memory) {\n        return _names[_addr];\n    }\n\n    /// @notice Checks if an address is registered\n    /// @param _addr The address to check\n    /// @return True if registered, false otherwise\n    function isRegistered(address _addr) external view returns (bool) {\n        return _registered[_addr];\n    }\n\n    /// @notice Removes the registration for the caller\n    function unregister() external {\n        require(_registered[msg.sender], \"Address not registered\");\n        delete _names[msg.sender];\n        delete _registered[msg.sender];\n        emit Unregistered(msg.sender);\n    }\n}"}
+{"task_id":"FormalEval/4","completion":"    mapping(address => string) private _names;\n    mapping(address => bool) private _registered;\n\n    event Registered(address indexed user, string name);\n    event Unregistered(address indexed user);\n\n    /// @notice Registers the caller with a specific name.\n    /// @param _name The name to associate with the caller's address.\n    function register(string calldata _name) external {\n        require(bytes(_name).length > 0, \"Name cannot be empty\");\n        _names[msg.sender] = _name;\n        _registered[msg.sender] = true;\n        emit Registered(msg.sender, _name);\n    }\n\n    /// @notice Retrieves the name associated with an address.\n    /// @param _addr The address to query.\n    /// @return The registered name or an empty string.\n    function getName(address _addr) external view returns (string memory) {\n        return _names[_addr];\n    }\n\n    /// @notice Checks if an address is registered.\n    /// @param _addr The address to check.\n    /// @return True if registered, false otherwise.\n    function isRegistered(address _addr) external view returns (bool) {\n        return _registered[_addr];\n    }\n\n    /// @notice Removes the registration for the caller.\n    function unregister() external {\n        require(_registered[msg.sender], \"Address not registered\");\n        delete _names[msg.sender];\n        delete _registered[msg.sender];\n        emit Unregistered(msg.sender);\n    }\n}"}
+{"task_id":"FormalEval/5","completion":"\n    string private _name;\n    string private _symbol;\n    uint8 private _decimals;\n    uint256 private _totalSupply;\n    address private _owner;\n    mapping(address => uint256) private _balances;\n\n    event Transfer(address indexed from, address indexed to, uint256 value);\n\n    modifier onlyOwner() {\n        require(msg.sender == _owner, \"BasicToken: caller is not the owner\");\n        _;\n    }\n\n    constructor(string memory name_, string memory symbol_, uint8 decimals_) {\n        _name = name_;\n        _symbol = symbol_;\n        _decimals = decimals_;\n        _owner = msg.sender;\n    }\n\n    function name() public view returns (string memory) {\n        return _name;\n    }\n\n    function symbol() public view returns (string memory) {\n        return _symbol;\n    }\n\n    function decimals() public view returns (uint8) {\n        return _decimals;\n    }\n\n    function totalSupply() public view returns (uint256) {\n        return _totalSupply;\n    }\n\n    function balanceOf(address account) public view returns (uint256) {\n        return _balances[account];\n    }\n\n    function mint(address to, uint256 amount) public onlyOwner {\n        require(to != address(0), \"BasicToken: mint to the zero address\");\n\n        _totalSupply += amount;\n        _balances[to] += amount;\n        emit Transfer(address(0), to, amount);\n    }\n\n    function transfer(address to, uint256 amount) public returns (bool) {\n        require(to != address(0), \"BasicToken: transfer to the zero address\");\n        require(_balances[msg.sender] >= amount, \"BasicToken: insufficient balance\");\n\n        _balances[msg.sender] -= amount;\n        _balances[to] += amount;\n        \n        emit Transfer(msg.sender, to, amount);\n        return true;\n    }\n}"}
+{"task_id":"FormalEval/5","completion":"\n    string private _name;\n    string private _symbol;\n    uint8 private _decimals;\n    uint256 private _totalSupply;\n    address private _owner;\n\n    mapping(address => uint256) private _balances;\n\n    event Transfer(address indexed from, address indexed to, uint256 value);\n\n    modifier onlyOwner() {\n        require(msg.sender == _owner, \"BasicToken: caller is not the owner\");\n        _;\n    }\n\n    constructor(string memory name_, string memory symbol_, uint8 decimals_) {\n        _name = name_;\n        _symbol = symbol_;\n        _decimals = decimals_;\n        _owner = msg.sender;\n    }\n\n    function name() external view returns (string memory) {\n        return _name;\n    }\n\n    function symbol() external view returns (string memory) {\n        return _symbol;\n    }\n\n    function decimals() external view returns (uint8) {\n        return _decimals;\n    }\n\n    function totalSupply() external view returns (uint256) {\n        return _totalSupply;\n    }\n\n    function balanceOf(address account) external view returns (uint256) {\n        return _balances[account];\n    }\n\n    function mint(address to, uint256 amount) external onlyOwner {\n        require(to != address(0), \"BasicToken: mint to the zero address\");\n\n        _totalSupply += amount;\n        _balances[to] += amount;\n        emit Transfer(address(0), to, amount);\n    }\n\n    function transfer(address to, uint256 amount) external returns (bool) {\n        require(to != address(0), \"BasicToken: transfer to the zero address\");\n        require(_balances[msg.sender] >= amount, \"BasicToken: insufficient balance\");\n\n        _balances[msg.sender] -= amount;\n        _balances[to] += amount;\n        \n        emit Transfer(msg.sender, to, amount);\n        return true;\n    }\n}"}
+{"task_id":"FormalEval/5","completion":"\n    string private _name;\n    string private _symbol;\n    uint8 private _decimals;\n    uint256 private _totalSupply;\n    address private _owner;\n    mapping(address => uint256) private _balances;\n\n    event Transfer(address indexed from, address indexed to, uint256 value);\n\n    modifier onlyOwner() {\n        require(msg.sender == _owner, \"BasicToken: caller is not the owner\");\n        _;\n    }\n\n    constructor(string memory name_, string memory symbol_, uint8 decimals_) {\n        _name = name_;\n        _symbol = symbol_;\n        _decimals = decimals_;\n        _owner = msg.sender;\n    }\n\n    function name() external view returns (string memory) {\n        return _name;\n    }\n\n    function symbol() external view returns (string memory) {\n        return _symbol;\n    }\n\n    function decimals() external view returns (uint8) {\n        return _decimals;\n    }\n\n    function totalSupply() external view returns (uint256) {\n        return _totalSupply;\n    }\n\n    function balanceOf(address account) external view returns (uint256) {\n        return _balances[account];\n    }\n\n    function mint(address to, uint256 amount) external onlyOwner {\n        require(to != address(0), \"BasicToken: mint to the zero address\");\n        \n        _totalSupply += amount;\n        _balances[to] += amount;\n        \n        emit Transfer(address(0), to, amount);\n    }\n\n    function transfer(address to, uint256 amount) external returns (bool) {\n        require(to != address(0), \"BasicToken: transfer to the zero address\");\n        require(_balances[msg.sender] >= amount, \"BasicToken: insufficient balance\");\n\n        _balances[msg.sender] -= amount;\n        _balances[to] += amount;\n\n        emit Transfer(msg.sender, to, amount);\n        return true;\n    }\n}"}
+{"task_id":"FormalEval/6","completion":"\n    address private _owner;\n\n    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);\n\n    error Unauthorized();\n    error InvalidOwner();\n\n    constructor() {\n        _owner = msg.sender;\n        emit OwnershipTransferred(address(0), msg.sender);\n    }\n\n    modifier onlyOwner() {\n        if (msg.sender != _owner) revert Unauthorized();\n        _;\n    }\n\n    /// @notice Returns the address of the current owner.\n    function owner() public view returns (address) {\n        return _owner;\n    }\n\n    /// @notice Transfers ownership of the contract to a new account (`newOwner`).\n    /// @param newOwner The address to transfer ownership to.\n    function transferOwnership(address newOwner) public onlyOwner {\n        if (newOwner == address(0)) revert InvalidOwner();\n        address oldOwner = _owner;\n        _owner = newOwner;\n        emit OwnershipTransferred(oldOwner, newOwner);\n    }\n\n    /// @notice Leaves the contract without owner. It will not be possible to call\n    /// `onlyOwner` functions anymore.\n    function renounceOwnership() public onlyOwner {\n        address oldOwner = _owner;\n        _owner = address(0);\n        emit OwnershipTransferred(oldOwner, address(0));\n    }\n}"}
+{"task_id":"FormalEval/6","completion":"\n    address private _owner;\n\n    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);\n\n    /// @notice Sets the initial owner of the contract as the deployer.\n    constructor() {\n        _owner = msg.sender;\n        emit OwnershipTransferred(address(0), msg.sender);\n    }\n\n    /// @notice Returns the address of the current owner.\n    function owner() public view returns (address) {\n        return _owner;\n    }\n\n    /// @notice Throws if called by any account other than the owner.\n    modifier onlyOwner() {\n        require(msg.sender == _owner, \"Ownable: caller is not the owner\");\n        _;\n    }\n\n    /// @notice Transfers ownership of the contract to a new account (`newOwner`).\n    /// @param newOwner The address to transfer ownership to.\n    function transferOwnership(address newOwner) public onlyOwner {\n        require(newOwner != address(0), \"Ownable: new owner is the zero address\");\n        address oldOwner = _owner;\n        _owner = newOwner;\n        emit OwnershipTransferred(oldOwner, newOwner);\n    }\n\n    /// @notice Leaves the contract without owner. It will not be possible to call\n    /// `onlyOwner` functions anymore.\n    function renounceOwnership() public onlyOwner {\n        address oldOwner = _owner;\n        _owner = address(0);\n        emit OwnershipTransferred(oldOwner, address(0));\n    }\n}"}
+{"task_id":"FormalEval/6","completion":"\n    address private _owner;\n\n    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);\n\n    /// @notice Sets the initial owner of the contract as the deployer.\n    constructor() {\n        _owner = msg.sender;\n        emit OwnershipTransferred(address(0), msg.sender);\n    }\n\n    /// @notice Returns the address of the current owner.\n    function owner() public view returns (address) {\n        return _owner;\n    }\n\n    /// @notice Throws if called by any account other than the owner.\n    modifier onlyOwner() {\n        require(msg.sender == _owner, \"Ownable: caller is not the owner\");\n        _;\n    }\n\n    /// @notice Transfers ownership of the contract to a new account (`newOwner`).\n    /// @param newOwner The address to transfer ownership to.\n    function transferOwnership(address newOwner) public onlyOwner {\n        require(newOwner != address(0), \"Ownable: new owner is the zero address\");\n        address oldOwner = _owner;\n        _owner = newOwner;\n        emit OwnershipTransferred(oldOwner, newOwner);\n    }\n\n    /// @notice Leaves the contract without owner. It will not be possible to call\n    /// `onlyOwner` functions anymore.\n    function renounceOwnership() public onlyOwner {\n        address oldOwner = _owner;\n        _owner = address(0);\n        emit OwnershipTransferred(oldOwner, address(0));\n    }\n}"}
+{"task_id":"FormalEval/7","completion":"\n    address public owner;\n    uint256 public maxWhitelistedAddresses;\n    uint256 public numWhitelistedCount;\n\n    mapping(address => bool) public whitelistedAddresses;\n\n    event AddedToWhitelist(address indexed account);\n    event RemovedFromWhitelist(address indexed account);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the contract owner\");\n        _;\n    }\n\n    constructor(uint256 _maxWhitelistedAddresses) {\n        require(_maxWhitelistedAddresses > 0, \"Max capacity must be greater than 0\");\n        owner = msg.sender;\n        maxWhitelistedAddresses = _maxWhitelistedAddresses;\n    }\n\n    /// @notice Adds the caller to the whitelist\n    function addToWhitelist() external {\n        require(!whitelistedAddresses[msg.sender], \"Address is already whitelisted\");\n        require(numWhitelistedCount < maxWhitelistedAddresses, \"Whitelist is full\");\n\n        whitelistedAddresses[msg.sender] = true;\n        numWhitelistedCount += 1;\n\n        emit AddedToWhitelist(msg.sender);\n    }\n\n    /// @notice Removes an address from the whitelist\n    /// @param _addr The address to remove\n    function removeFromWhitelist(address _addr) external onlyOwner {\n        require(whitelistedAddresses[_addr], \"Address is not in the whitelist\");\n\n        whitelistedAddresses[_addr] = false;\n        numWhitelistedCount -= 1;\n\n        emit RemovedFromWhitelist(_addr);\n    }\n\n    /// @notice Checks if an address is whitelisted\n    /// @param _addr The address to check\n    function isWhitelisted(address _addr) external view returns (bool) {\n        return whitelistedAddresses[_addr];\n    }\n\n    /// @notice Returns the current number of whitelisted addresses\n    function getNumWhitelisted() external view returns (uint256) {\n        return numWhitelistedCount;\n    }\n\n    /// @notice Returns the maximum capacity\n    function maxWhitelisted() external view returns (uint256) {\n        return maxWhitelistedAddresses;\n    }\n}"}
+{"task_id":"FormalEval/7","completion":"\n    address public owner;\n    uint256 public maxWhitelistedAddresses;\n    uint256 public numWhitelistedCount;\n\n    mapping(address => bool) public whitelistedAddresses;\n\n    event AddedToWhitelist(address indexed account);\n    event RemovedFromWhitelist(address indexed account);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the contract owner\");\n        _;\n    }\n\n    constructor(uint256 _maxWhitelistedAddresses) {\n        require(_maxWhitelistedAddresses > 0, \"Max capacity must be greater than 0\");\n        owner = msg.sender;\n        maxWhitelistedAddresses = _maxWhitelistedAddresses;\n    }\n\n    /// @notice Adds the caller to the whitelist\n    function addToWhitelist() external {\n        require(!whitelistedAddresses[msg.sender], \"Address is already whitelisted\");\n        require(numWhitelistedCount < maxWhitelistedAddresses, \"Whitelist capacity reached\");\n\n        whitelistedAddresses[msg.sender] = true;\n        numWhitelistedCount += 1;\n\n        emit AddedToWhitelist(msg.sender);\n    }\n\n    /// @notice Removes an address from the whitelist\n    /// @param _addr The address to remove\n    function removeFromWhitelist(address _addr) external onlyOwner {\n        require(whitelistedAddresses[_addr], \"Address is not in the whitelist\");\n\n        whitelistedAddresses[_addr] = false;\n        numWhitelistedCount -= 1;\n\n        emit RemovedFromWhitelist(_addr);\n    }\n\n    /// @notice Checks if an address is whitelisted\n    function isWhitelisted(address _addr) external view returns (bool) {\n        return whitelistedAddresses[_addr];\n    }\n\n    /// @notice Returns the current number of whitelisted addresses\n    function getNumWhitelisted() external view returns (uint256) {\n        return numWhitelistedCount;\n    }\n\n    /// @notice Returns the maximum capacity\n    function maxWhitelisted() external view returns (uint256) {\n        return maxWhitelistedAddresses;\n    }\n}"}
+{"task_id":"FormalEval/7","completion":"\n    address public owner;\n    uint256 public maxWhitelistedAddresses;\n    uint256 public numWhitelistedCount;\n\n    mapping(address => bool) public whitelistedAddresses;\n\n    event AddedToWhitelist(address indexed account);\n    event RemovedFromWhitelist(address indexed account);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the contract owner\");\n        _;\n    }\n\n    constructor(uint256 _maxWhitelistedAddresses) {\n        require(_maxWhitelistedAddresses > 0, \"Max capacity must be greater than 0\");\n        owner = msg.sender;\n        maxWhitelistedAddresses = _maxWhitelistedAddresses;\n    }\n\n    /// @notice Adds the caller to the whitelist\n    function addToWhitelist() external {\n        require(!whitelistedAddresses[msg.sender], \"Address is already whitelisted\");\n        require(numWhitelistedCount < maxWhitelistedAddresses, \"Whitelist is full\");\n\n        whitelistedAddresses[msg.sender] = true;\n        numWhitelistedCount += 1;\n\n        emit AddedToWhitelist(msg.sender);\n    }\n\n    /// @notice Removes an address from the whitelist\n    /// @param _addr The address to be removed\n    function removeFromWhitelist(address _addr) external onlyOwner {\n        require(whitelistedAddresses[_addr], \"Address is not in the whitelist\");\n\n        whitelistedAddresses[_addr] = false;\n        numWhitelistedCount -= 1;\n\n        emit RemovedFromWhitelist(_addr);\n    }\n\n    /// @notice Checks if an address is whitelisted\n    /// @param _addr The address to check\n    function isWhitelisted(address _addr) external view returns (bool) {\n        return whitelistedAddresses[_addr];\n    }\n\n    /// @notice Returns the current number of whitelisted addresses\n    function getNumWhitelisted() external view returns (uint256) {\n        return numWhitelistedCount;\n    }\n\n    /// @notice Returns the maximum capacity of the whitelist\n    function maxWhitelisted() external view returns (uint256) {\n        return maxWhitelistedAddresses;\n    }\n}"}
+{"task_id":"FormalEval/8","completion":"    address private owner;\n    bool private locked;\n\n    struct LockInfo {\n        uint256 amount;\n        uint256 unlockTime;\n    }\n\n    mapping(address => LockInfo) private locks;\n\n    event Deposit(address indexed sender, uint256 amount, uint256 unlockTime);\n    event Withdrawal(address indexed sender, uint256 amount);\n\n    modifier nonReentrant() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n    }\n\n    /// @notice Locks ETH until the specified unlockTime\n    /// @param unlockTime The timestamp when the funds can be withdrawn\n    function deposit(uint256 unlockTime) external payable {\n        require(msg.value > 0, \"Amount must be greater than 0\");\n        require(unlockTime > block.timestamp, \"Unlock time must be in the future\");\n        require(locks[msg.sender].amount == 0, \"Existing lock found, withdraw first\");\n\n        locks[msg.sender] = LockInfo({\n            amount: msg.value,\n            unlockTime: unlockTime\n        });\n\n        emit Deposit(msg.sender, msg.value, unlockTime);\n    }\n\n    /// @notice Withdraws all locked ETH if the unlock time has passed\n    function withdraw() external nonReentrant {\n        LockInfo storage userLock = locks[msg.sender];\n        \n        require(userLock.amount > 0, \"No locked funds\");\n        require(block.timestamp >= userLock.unlockTime, \"Funds are still locked\");\n\n        uint256 amountToWithdraw = userLock.amount;\n        \n        userLock.amount = 0;\n        userLock.unlockTime = 0;\n\n        (bool success, ) = payable(msg.sender).call{value: amountToWithdraw}(\"\");\n        require(success, \"Transfer failed\");\n\n        emit Withdrawal(msg.sender, amountToWithdraw);\n    }\n\n    /// @notice Returns the locked balance for a specific address\n    /// @param _addr The address to query\n    function getBalance(address _addr) external view returns (uint256) {\n        return locks[_addr].amount;\n    }\n\n    /// @notice Returns the unlock time for a specific address\n    /// @param _addr The address to query\n    function getUnlockTime(address _addr) external view returns (uint256) {\n        return locks[_addr].unlockTime;\n    }\n}"}
+{"task_id":"FormalEval/8","completion":"    address private owner;\n    bool private locked;\n\n    mapping(address => uint256) private balances;\n    mapping(address => uint256) private unlockTimes;\n\n    event Deposit(address indexed sender, uint256 amount, uint256 unlockTime);\n    event Withdrawal(address indexed sender, uint256 amount);\n\n    modifier nonReentrant() {\n        require(!locked, \"ReentrancyGuard: reentrant call\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n    }\n\n    /// @notice Locks ETH until the specified unlock time.\n    /// @param unlockTime The timestamp when the funds can be withdrawn.\n    function deposit(uint256 unlockTime) external payable {\n        require(msg.value > 0, \"Amount must be greater than 0\");\n        require(unlockTime > block.timestamp, \"Unlock time must be in the future\");\n        \n        balances[msg.sender] += msg.value;\n        unlockTimes[msg.sender] = unlockTime;\n\n        emit Deposit(msg.sender, msg.value, unlockTime);\n    }\n\n    /// @notice Withdraws all locked ETH for the sender if the unlock time has passed.\n    function withdraw() external nonReentrant {\n        uint256 amount = balances[msg.sender];\n        uint256 unlockTime = unlockTimes[msg.sender];\n\n        require(amount > 0, \"No funds to withdraw\");\n        require(block.timestamp >= unlockTime, \"Funds are still locked\");\n\n        balances[msg.sender] = 0;\n        unlockTimes[msg.sender] = 0;\n\n        (bool success, ) = payable(msg.sender).call{value: amount}(\"\");\n        require(success, \"Transfer failed\");\n\n        emit Withdrawal(msg.sender, amount);\n    }\n\n    /// @notice Returns the locked balance for a specific address.\n    /// @param _addr The address to query.\n    function getBalance(address _addr) external view returns (uint256) {\n        return balances[_addr];\n    }\n\n    /// @notice Returns the unlock time for a specific address.\n    /// @param _addr The address to query.\n    function getUnlockTime(address _addr) external view returns (uint256) {\n        return unlockTimes[_addr];\n    }\n}"}
+{"task_id":"FormalEval/8","completion":"\n    address private owner;\n    bool private locked;\n\n    mapping(address => uint256) private balances;\n    mapping(address => uint256) private unlockTimes;\n\n    event Deposit(address indexed sender, uint256 amount, uint256 unlockTime);\n    event Withdrawal(address indexed sender, uint256 amount);\n\n    modifier nonReentrant() {\n        require(!locked, \"ReentrancyGuard: reentrant call\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n    }\n\n    /// @notice Locks ETH until the specified unlockTime\n    /// @param unlockTime The timestamp when the funds can be withdrawn\n    function deposit(uint256 unlockTime) external payable {\n        require(msg.value > 0, \"Amount must be greater than 0\");\n        require(unlockTime > block.timestamp, \"Unlock time must be in the future\");\n        \n        balances[msg.sender] += msg.value;\n        unlockTimes[msg.sender] = unlockTime;\n\n        emit Deposit(msg.sender, msg.value, unlockTime);\n    }\n\n    /// @notice Withdraws all locked ETH for the sender\n    function withdraw() external nonReentrant {\n        uint256 amount = balances[msg.sender];\n        uint256 unlockTime = unlockTimes[msg.sender];\n\n        require(amount > 0, \"No funds to withdraw\");\n        require(block.timestamp >= unlockTime, \"Funds are still locked\");\n\n        balances[msg.sender] = 0;\n        unlockTimes[msg.sender] = 0;\n\n        (bool success, ) = payable(msg.sender).call{value: amount}(\"\");\n        require(success, \"Transfer failed\");\n\n        emit Withdrawal(msg.sender, amount);\n    }\n\n    /// @notice Returns the locked balance for a specific address\n    /// @param _addr The address to query\n    function getBalance(address _addr) external view returns (uint256) {\n        return balances[_addr];\n    }\n\n    /// @notice Returns the unlock time for a specific address\n    /// @param _addr The address to query\n    function getUnlockTime(address _addr) external view returns (uint256) {\n        return unlockTimes[_addr];\n    }\n}"}
+{"task_id":"FormalEval/9","completion":"    address public owner;\n\n    struct Proposal {\n        string description;\n        uint256 voteCount;\n    }\n\n    Proposal[] private proposals;\n    mapping(uint256 => mapping(address => bool)) private votes;\n    bool private locked;\n\n    event ProposalCreated(uint256 indexed proposalId, string description);\n    event Voted(uint256 indexed proposalId, address indexed voter);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the contract owner\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n    }\n\n    /// @notice Creates a new proposal\n    /// @param description The text description of the proposal\n    /// @return proposalId The index of the created proposal\n    function createProposal(string calldata description) external onlyOwner returns (uint256) {\n        uint256 proposalId = proposals.length;\n        proposals.push(Proposal({\n            description: description,\n            voteCount: 0\n        }));\n        emit ProposalCreated(proposalId, description);\n        return proposalId;\n    }\n\n    /// @notice Casts a vote for a specific proposal\n    /// @param proposalId The ID of the proposal to vote for\n    function vote(uint256 proposalId) external nonReentrant {\n        require(proposalId < proposals.length, \"Invalid proposal ID\");\n        require(!votes[proposalId][msg.sender], \"Already voted on this proposal\");\n\n        votes[proposalId][msg.sender] = true;\n        proposals[proposalId].voteCount += 1;\n\n        emit Voted(proposalId, msg.sender);\n    }\n\n    /// @notice Retrieves proposal details\n    /// @param proposalId The ID of the proposal\n    /// @return description The proposal description\n    /// @return voteCount The current number of votes\n    function getProposal(uint256 proposalId) external view returns (string memory, uint256) {\n        require(proposalId < proposals.length, \"Invalid proposal ID\");\n        Proposal storage p = proposals[proposalId];\n        return (p.description, p.voteCount);\n    }\n\n    /// @notice Returns the total number of proposals created\n    function getProposalCount() external view returns (uint256) {\n        return proposals.length;\n    }\n\n    /// @notice Checks if an address has already voted on a proposal\n    /// @param proposalId The ID of the proposal\n    /// @param voter The address to check\n    function hasVoted(uint256 proposalId, address voter) external view returns (bool) {\n        require(proposalId < proposals.length, \"Invalid proposal ID\");\n        return votes[proposalId][voter];\n    }\n}"}
+{"task_id":"FormalEval/9","completion":"    address public owner;\n\n    struct Proposal {\n        string description;\n        uint256 voteCount;\n    }\n\n    Proposal[] private proposals;\n    mapping(uint256 => mapping(address => bool)) private votes;\n    bool private locked;\n\n    event ProposalCreated(uint256 indexed proposalId, string description);\n    event Voted(uint256 indexed proposalId, address indexed voter);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the contract owner\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n    }\n\n    /// @notice Creates a new proposal\n    /// @param description The text description of the proposal\n    /// @return proposalId The ID of the newly created proposal\n    function createProposal(string calldata description) external onlyOwner returns (uint256) {\n        uint256 proposalId = proposals.length;\n        proposals.push(Proposal({\n            description: description,\n            voteCount: 0\n        }));\n        emit ProposalCreated(proposalId, description);\n        return proposalId;\n    }\n\n    /// @notice Casts a vote for a specific proposal\n    /// @param proposalId The ID of the proposal to vote for\n    function vote(uint256 proposalId) external nonReentrant {\n        require(proposalId < proposals.length, \"Invalid proposal ID\");\n        require(!votes[proposalId][msg.sender], \"Already voted on this proposal\");\n\n        votes[proposalId][msg.sender] = true;\n        proposals[proposalId].voteCount += 1;\n\n        emit Voted(proposalId, msg.sender);\n    }\n\n    /// @notice Retrieves proposal details\n    /// @param proposalId The ID of the proposal\n    /// @return description The proposal description\n    /// @return voteCount The current number of votes\n    function getProposal(uint256 proposalId) external view returns (string memory, uint256) {\n        require(proposalId < proposals.length, \"Invalid proposal ID\");\n        Proposal storage p = proposals[proposalId];\n        return (p.description, p.voteCount);\n    }\n\n    /// @notice Returns the total number of proposals\n    function getProposalCount() external view returns (uint256) {\n        return proposals.length;\n    }\n\n    /// @notice Checks if an address has already voted on a proposal\n    /// @param proposalId The ID of the proposal\n    /// @param voter The address to check\n    function hasVoted(uint256 proposalId, address voter) external view returns (bool) {\n        require(proposalId < proposals.length, \"Invalid proposal ID\");\n        return votes[proposalId][voter];\n    }\n}"}
+{"task_id":"FormalEval/9","completion":"    address public owner;\n\n    struct Proposal {\n        string description;\n        uint256 voteCount;\n    }\n\n    Proposal[] private proposals;\n    mapping(uint256 => mapping(address => bool)) private votes;\n    bool private locked;\n\n    event ProposalCreated(uint256 indexed proposalId, string description);\n    event Voted(uint256 indexed proposalId, address indexed voter);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the contract owner\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n    }\n\n    /// @notice Creates a new proposal\n    /// @param description The text description of the proposal\n    /// @return proposalId The ID of the newly created proposal\n    function createProposal(string calldata description) external onlyOwner returns (uint256) {\n        uint256 proposalId = proposals.length;\n        proposals.push(Proposal({\n            description: description,\n            voteCount: 0\n        }));\n        emit ProposalCreated(proposalId, description);\n        return proposalId;\n    }\n\n    /// @notice Casts a vote for a specific proposal\n    /// @param proposalId The ID of the proposal to vote for\n    function vote(uint256 proposalId) external nonReentrant {\n        require(proposalId < proposals.length, \"Invalid proposal ID\");\n        require(!votes[proposalId][msg.sender], \"Already voted on this proposal\");\n\n        votes[proposalId][msg.sender] = true;\n        proposals[proposalId].voteCount += 1;\n\n        emit Voted(proposalId, msg.sender);\n    }\n\n    /// @notice Retrieves details of a proposal\n    /// @param proposalId The ID of the proposal\n    /// @return description The proposal description\n    /// @return voteCount The current number of votes\n    function getProposal(uint256 proposalId) external view returns (string memory, uint256) {\n        require(proposalId < proposals.length, \"Invalid proposal ID\");\n        Proposal storage p = proposals[proposalId];\n        return (p.description, p.voteCount);\n    }\n\n    /// @notice Returns the total number of proposals\n    function getProposalCount() external view returns (uint256) {\n        return proposals.length;\n    }\n\n    /// @notice Checks if an address has voted on a specific proposal\n    /// @param proposalId The ID of the proposal\n    /// @param voter The address to check\n    function hasVoted(uint256 proposalId, address voter) external view returns (bool) {\n        require(proposalId < proposals.length, \"Invalid proposal ID\");\n        return votes[proposalId][voter];\n    }\n}"}
+{"task_id":"FormalEval/10","completion":"\n    address[] public owners;\n    mapping(address => bool) public isOwner;\n    uint256 public numConfirmationsRequired;\n\n    struct Transaction {\n        address to;\n        uint256 value;\n        bytes data;\n        bool executed;\n        uint256 numConfirmations;\n    }\n\n    Transaction[] public transactions;\n    mapping(uint256 => mapping(address => bool)) public isConfirmed;\n\n    event SubmitTransaction(address indexed owner, uint256 indexed txIndex, address indexed to, uint256 value, bytes data);\n    event ConfirmTransaction(address indexed owner, uint256 indexed txIndex);\n    event RevokeConfirmation(address indexed owner, uint256 indexed txIndex);\n    event ExecuteTransaction(address indexed owner, uint256 indexed txIndex);\n\n    modifier onlyOwner() {\n        require(isOwner[msg.sender], \"Not an owner\");\n        _;\n    }\n\n    modifier txExists(uint256 _txIndex) {\n        require(_txIndex < transactions.length, \"Transaction does not exist\");\n        _;\n    }\n\n    modifier notExecuted(uint256 _txIndex) {\n        require(!transactions[_txIndex].executed, \"Transaction already executed\");\n        _;\n    }\n\n    modifier notConfirmed(uint256 _txIndex) {\n        require(!isConfirmed[_txIndex][msg.sender], \"Transaction already confirmed\");\n        _;\n    }\n\n    constructor(address[] memory _owners, uint256 _numConfirmationsRequired) {\n        require(_owners.length > 0, \"Owners required\");\n        require(_numConfirmationsRequired > 0 && _numConfirmationsRequired <= _owners.length, \"Invalid number of required confirmations\");\n\n        for (uint256 i = 0; i < _owners.length; i++) {\n            address owner = _owners[i];\n            require(owner != address(0), \"Invalid owner\");\n            require(!isOwner[owner], \"Owner not unique\");\n\n            isOwner[owner] = true;\n            owners.push(owner);\n        }\n\n        numConfirmationsRequired = _numConfirmationsRequired;\n    }\n\n    receive() external payable {}\n\n    function submitTransaction(address _to, uint256 _value, bytes calldata _data) external onlyOwner {\n        uint256 txIndex = transactions.length;\n        transactions.push(Transaction({\n            to: _to,\n            value: _value,\n            data: _data,\n            executed: false,\n            numConfirmations: 0\n        }));\n        emit SubmitTransaction(msg.sender, txIndex, _to, _value, _data);\n    }\n\n    function confirmTransaction(uint256 _txIndex) external onlyOwner txExists(_txIndex) notExecuted(_txIndex) notConfirmed(_txIndex) {\n        Transaction storage transaction = transactions[_txIndex];\n        transaction.numConfirmations += 1;\n        isConfirmed[_txIndex][msg.sender] = true;\n        emit ConfirmTransaction(msg.sender, _txIndex);\n    }\n\n    function executeTransaction(uint256 _txIndex) external onlyOwner txExists(_txIndex) notExecuted(_txIndex) {\n        Transaction storage transaction = transactions[_txIndex];\n        require(transaction.numConfirmations >= numConfirmationsRequired, \"Cannot execute: insufficient confirmations\");\n\n        transaction.executed = true;\n        (bool success, ) = transaction.to.call{value: transaction.value}(transaction.data);\n        require(success, \"Transaction failed\");\n\n        emit ExecuteTransaction(msg.sender, _txIndex);\n    }\n\n    function revokeConfirmation(uint256 _txIndex) external onlyOwner txExists(_txIndex) notExecuted(_txIndex) {\n        require(isConfirmed[_txIndex][msg.sender], \"Transaction not confirmed\");\n        Transaction storage transaction = transactions[_txIndex];\n        transaction.numConfirmations -= 1;\n        isConfirmed[_txIndex][msg.sender] = false;\n        emit RevokeConfirmation(msg.sender, _txIndex);\n    }\n\n    function getTransactionCount() external view returns (uint256) {\n        return transactions.length;\n    }\n\n    function getTransaction(uint256 _txIndex) external view returns (address to, uint256 value, bytes memory data, bool executed, uint256 numConfirmations) {\n        Transaction storage transaction = transactions[_txIndex];\n        return (transaction.to, transaction.value, transaction.data, transaction.executed, transaction.numConfirmations);\n    }\n\n    function getOwners() external view returns (address[] memory) {\n        return owners;\n    }\n}"}
+{"task_id":"FormalEval/10","completion":"\n    address[] public owners;\n    mapping(address => bool) public isOwner;\n    uint256 public numConfirmationsRequired;\n\n    struct Transaction {\n        address to;\n        uint256 value;\n        bytes data;\n        bool executed;\n        uint256 numConfirmations;\n    }\n\n    Transaction[] public transactions;\n    mapping(uint256 => mapping(address => bool)) public isConfirmed;\n\n    event SubmitTransaction(address indexed owner, uint256 indexed txIndex, address indexed to, uint256 value, bytes data);\n    event ConfirmTransaction(address indexed owner, uint256 indexed txIndex);\n    event RevokeConfirmation(address indexed owner, uint256 indexed txIndex);\n    event ExecuteTransaction(address indexed owner, uint256 indexed txIndex);\n\n    modifier onlyOwner() {\n        require(isOwner[msg.sender], \"Not an owner\");\n        _;\n    }\n\n    modifier txExists(uint256 _txIndex) {\n        require(_txIndex < transactions.length, \"Transaction does not exist\");\n        _;\n    }\n\n    modifier notExecuted(uint256 _txIndex) {\n        require(!transactions[_txIndex].executed, \"Transaction already executed\");\n        _;\n    }\n\n    modifier notConfirmed(uint256 _txIndex) {\n        require(!isConfirmed[_txIndex][msg.sender], \"Transaction already confirmed\");\n        _;\n    }\n\n    constructor(address[] memory _owners, uint256 _numConfirmationsRequired) {\n        require(_owners.length > 0, \"Owners required\");\n        require(_numConfirmationsRequired > 0 && _numConfirmationsRequired <= _owners.length, \"Invalid number of required confirmations\");\n\n        for (uint256 i = 0; i < _owners.length; i++) {\n            address owner = _owners[i];\n            require(owner != address(0), \"Invalid owner\");\n            require(!isOwner[owner], \"Owner not unique\");\n\n            isOwner[owner] = true;\n            owners.push(owner);\n        }\n\n        numConfirmationsRequired = _numConfirmationsRequired;\n    }\n\n    receive() external payable {}\n\n    function submitTransaction(address _to, uint256 _value, bytes calldata _data) external onlyOwner {\n        uint256 txIndex = transactions.length;\n        transactions.push(Transaction({\n            to: _to,\n            value: _value,\n            data: _data,\n            executed: false,\n            numConfirmations: 0\n        }));\n        emit SubmitTransaction(msg.sender, txIndex, _to, _value, _data);\n    }\n\n    function confirmTransaction(uint256 _txIndex) external onlyOwner txExists(_txIndex) notExecuted(_txIndex) notConfirmed(_txIndex) {\n        Transaction storage transaction = transactions[_txIndex];\n        transaction.numConfirmations += 1;\n        isConfirmed[_txIndex][msg.sender] = true;\n        emit ConfirmTransaction(msg.sender, _txIndex);\n    }\n\n    function executeTransaction(uint256 _txIndex) external onlyOwner txExists(_txIndex) notExecuted(_txIndex) {\n        Transaction storage transaction = transactions[_txIndex];\n        require(transaction.numConfirmations >= numConfirmationsRequired, \"Cannot execute: insufficient confirmations\");\n\n        transaction.executed = true;\n        (bool success, ) = transaction.to.call{value: transaction.value}(transaction.data);\n        require(success, \"Transaction failed\");\n\n        emit ExecuteTransaction(msg.sender, _txIndex);\n    }\n\n    function revokeConfirmation(uint256 _txIndex) external onlyOwner txExists(_txIndex) notExecuted(_txIndex) {\n        require(isConfirmed[_txIndex][msg.sender], \"Transaction not confirmed\");\n        Transaction storage transaction = transactions[_txIndex];\n        transaction.numConfirmations -= 1;\n        isConfirmed[_txIndex][msg.sender] = false;\n        emit RevokeConfirmation(msg.sender, _txIndex);\n    }\n\n    function getTransactionCount() external view returns (uint256) {\n        return transactions.length;\n    }\n\n    function getTransaction(uint256 _txIndex) external view returns (address to, uint256 value, bytes memory data, bool executed, uint256 numConfirmations) {\n        Transaction storage transaction = transactions[_txIndex];\n        return (transaction.to, transaction.value, transaction.data, transaction.executed, transaction.numConfirmations);\n    }\n\n    function getOwners() external view returns (address[] memory) {\n        return owners;\n    }\n}"}
+{"task_id":"FormalEval/10","completion":"\n    address[] public owners;\n    mapping(address => bool) public isOwner;\n    uint256 public numConfirmationsRequired;\n\n    struct Transaction {\n        address to;\n        uint256 value;\n        bytes data;\n        bool executed;\n        uint256 numConfirmations;\n    }\n\n    Transaction[] public transactions;\n    mapping(uint256 => mapping(address => bool)) public isConfirmed;\n\n    event SubmitTransaction(address indexed owner, uint256 indexed txIndex, address indexed to, uint256 value, bytes data);\n    event ConfirmTransaction(address indexed owner, uint256 indexed txIndex);\n    event RevokeConfirmation(address indexed owner, uint256 indexed txIndex);\n    event ExecuteTransaction(address indexed owner, uint256 indexed txIndex);\n\n    modifier onlyOwner() {\n        require(isOwner[msg.sender], \"Not an owner\");\n        _;\n    }\n\n    modifier txExists(uint256 _txIndex) {\n        require(_txIndex < transactions.length, \"Transaction does not exist\");\n        _;\n    }\n\n    modifier notExecuted(uint256 _txIndex) {\n        require(!transactions[_txIndex].executed, \"Transaction already executed\");\n        _;\n    }\n\n    modifier notConfirmed(uint256 _txIndex) {\n        require(!isConfirmed[_txIndex][msg.sender], \"Transaction already confirmed\");\n        _;\n    }\n\n    constructor(address[] memory _owners, uint256 _numConfirmationsRequired) {\n        require(_owners.length > 0, \"Owners required\");\n        require(_numConfirmationsRequired > 0 && _numConfirmationsRequired <= _owners.length, \"Invalid number of required confirmations\");\n\n        for (uint256 i = 0; i < _owners.length; i++) {\n            address owner = _owners[i];\n            require(owner != address(0), \"Invalid owner\");\n            require(!isOwner[owner], \"Owner not unique\");\n\n            isOwner[owner] = true;\n            owners.push(owner);\n        }\n\n        numConfirmationsRequired = _numConfirmationsRequired;\n    }\n\n    receive() external payable {}\n\n    function submitTransaction(address _to, uint256 _value, bytes calldata _data) external onlyOwner {\n        uint256 txIndex = transactions.length;\n        transactions.push(Transaction({\n            to: _to,\n            value: _value,\n            data: _data,\n            executed: false,\n            numConfirmations: 0\n        }));\n        emit SubmitTransaction(msg.sender, txIndex, _to, _value, _data);\n    }\n\n    function confirmTransaction(uint256 _txIndex) external onlyOwner txExists(_txIndex) notExecuted(_txIndex) notConfirmed(_txIndex) {\n        Transaction storage transaction = transactions[_txIndex];\n        transaction.numConfirmations += 1;\n        isConfirmed[_txIndex][msg.sender] = true;\n        emit ConfirmTransaction(msg.sender, _txIndex);\n    }\n\n    function executeTransaction(uint256 _txIndex) external onlyOwner txExists(_txIndex) notExecuted(_txIndex) {\n        Transaction storage transaction = transactions[_txIndex];\n        require(transaction.numConfirmations >= numConfirmationsRequired, \"Cannot execute: insufficient confirmations\");\n\n        transaction.executed = true;\n        (bool success, ) = transaction.to.call{value: transaction.value}(transaction.data);\n        require(success, \"Transaction failed\");\n\n        emit ExecuteTransaction(msg.sender, _txIndex);\n    }\n\n    function revokeConfirmation(uint256 _txIndex) external onlyOwner txExists(_txIndex) notExecuted(_txIndex) {\n        require(isConfirmed[_txIndex][msg.sender], \"Transaction not confirmed\");\n        Transaction storage transaction = transactions[_txIndex];\n        transaction.numConfirmations -= 1;\n        isConfirmed[_txIndex][msg.sender] = false;\n        emit RevokeConfirmation(msg.sender, _txIndex);\n    }\n\n    function getTransactionCount() external view returns (uint256) {\n        return transactions.length;\n    }\n\n    function getTransaction(uint256 _txIndex) external view returns (address to, uint256 value, bytes memory data, bool executed, uint256 numConfirmations) {\n        Transaction storage transaction = transactions[_txIndex];\n        return (transaction.to, transaction.value, transaction.data, transaction.executed, transaction.numConfirmations);\n    }\n\n    function getOwners() external view returns (address[] memory) {\n        return owners;\n    }\n}"}
+{"task_id":"FormalEval/11","completion":"\n    address private immutable _beneficiary;\n    uint256 private immutable _start;\n    uint256 private immutable _duration;\n    uint256 private _released;\n    bool private _locked;\n\n    event TokensReleased(uint256 amount);\n\n    modifier onlyBeneficiary() {\n        require(msg.sender == _beneficiary, \"Not the beneficiary\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!_locked, \"Reentrancy guard\");\n        _locked = true;\n        _;\n        _locked = false;\n    }\n\n    constructor(address beneficiary_, uint256 startTime_, uint256 duration_) {\n        require(beneficiary_ != address(0), \"Beneficiary is zero address\");\n        require(duration_ > 0, \"Duration must be greater than 0\");\n        _beneficiary = beneficiary_;\n        _start = startTime_;\n        _duration = duration_;\n    }\n\n    receive() external payable {}\n\n    function beneficiary() external view returns (address) {\n        return _beneficiary;\n    }\n\n    function start() external view returns (uint256) {\n        return _start;\n    }\n\n    function duration() external view returns (uint256) {\n        return _duration;\n    }\n\n    function released() external view returns (uint256) {\n        return _released;\n    }\n\n    function vestedAmount(uint256 timestamp) public view returns (uint256) {\n        uint256 totalBalance = address(this).balance + _released;\n\n        if (timestamp < _start) {\n            return 0;\n        } else if (timestamp >= _start + _duration) {\n            return totalBalance;\n        } else {\n            return (totalBalance * (timestamp - _start)) / _duration;\n        }\n    }\n\n    function releasable() public view returns (uint256) {\n        return vestedAmount(block.timestamp) - _released;\n    }\n\n    function release() external onlyBeneficiary nonReentrant {\n        uint256 amount = releasable();\n        require(amount > 0, \"No tokens to release\");\n\n        _released += amount;\n        emit TokensReleased(amount);\n\n        (bool success, ) = payable(_beneficiary).call{value: amount}(\"\");\n        require(success, \"Transfer failed\");\n    }\n}"}
+{"task_id":"FormalEval/11","completion":"\n    address private immutable _beneficiary;\n    uint256 private immutable _start;\n    uint256 private immutable _duration;\n    uint256 private _released;\n    bool private _locked;\n\n    event TokensReleased(uint256 amount);\n\n    modifier onlyBeneficiary() {\n        require(msg.sender == _beneficiary, \"Not authorized\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!_locked, \"Reentrancy detected\");\n        _locked = true;\n        _;\n        _locked = false;\n    }\n\n    constructor(address beneficiary_, uint256 startTime_, uint256 duration_) {\n        require(beneficiary_ != address(0), \"Invalid beneficiary\");\n        require(duration_ > 0, \"Duration must be > 0\");\n        _beneficiary = beneficiary_;\n        _start = startTime_;\n        _duration = duration_;\n    }\n\n    receive() external payable {}\n\n    function beneficiary() external view returns (address) {\n        return _beneficiary;\n    }\n\n    function start() external view returns (uint256) {\n        return _start;\n    }\n\n    function duration() external view returns (uint256) {\n        return _duration;\n    }\n\n    function released() external view returns (uint256) {\n        return _released;\n    }\n\n    function releasable() public view returns (uint256) {\n        return vestedAmount(block.timestamp) - _released;\n    }\n\n    function release() external onlyBeneficiary nonReentrant {\n        uint256 amount = releasable();\n        require(amount > 0, \"Nothing to release\");\n\n        _released += amount;\n        (bool success, ) = payable(_beneficiary).call{value: amount}(\"\");\n        require(success, \"Transfer failed\");\n\n        emit TokensReleased(amount);\n    }\n\n    function vestedAmount(uint256 timestamp) public view returns (uint256) {\n        uint256 totalBalance = address(this).balance + _released;\n\n        if (timestamp < _start) {\n            return 0;\n        } else if (timestamp >= _start + _duration) {\n            return totalBalance;\n        } else {\n            return (totalBalance * (timestamp - _start)) / _duration;\n        }\n    }\n}"}
+{"task_id":"FormalEval/11","completion":"\n    address private immutable _beneficiary;\n    uint256 private immutable _start;\n    uint256 private immutable _duration;\n    uint256 private _released;\n\n    event TokensReleased(uint256 amount);\n\n    modifier onlyBeneficiary() {\n        require(msg.sender == _beneficiary, \"Not the beneficiary\");\n        _;\n    }\n\n    constructor(address beneficiary_, uint256 startTime_, uint256 duration_) {\n        require(beneficiary_ != address(0), \"Beneficiary is zero address\");\n        require(duration_ > 0, \"Duration must be greater than 0\");\n        _beneficiary = beneficiary_;\n        _start = startTime_;\n        _duration = duration_;\n    }\n\n    receive() external payable {}\n\n    function beneficiary() external view returns (address) {\n        return _beneficiary;\n    }\n\n    function start() external view returns (uint256) {\n        return _start;\n    }\n\n    function duration() external view returns (uint256) {\n        return _duration;\n    }\n\n    function released() external view returns (uint256) {\n        return _released;\n    }\n\n    function vestedAmount(uint256 timestamp) public view returns (uint256) {\n        if (timestamp < _start) {\n            return 0;\n        } else if (timestamp >= _start + _duration) {\n            return address(this).balance + _released;\n        } else {\n            return ((address(this).balance + _released) * (timestamp - _start)) / _duration;\n        }\n    }\n\n    function releasable() public view returns (uint256) {\n        return vestedAmount(block.timestamp) - _released;\n    }\n\n    function release() external onlyBeneficiary {\n        uint256 amount = releasable();\n        require(amount > 0, \"No tokens to release\");\n\n        _released += amount;\n        emit TokensReleased(amount);\n\n        (bool success, ) = payable(_beneficiary).call{value: amount}(\"\");\n        require(success, \"Transfer failed\");\n    }\n}"}
+{"task_id":"FormalEval/12","completion":"    address public seller;\n    uint256 public endAt;\n    bool public ended;\n\n    address public highestBidder;\n    uint256 public highestBid;\n\n    mapping(address => uint256) public pendingReturns;\n\n    event BidPlaced(address indexed bidder, uint256 amount);\n    event AuctionEnded(address indexed winner, uint256 amount);\n\n    modifier onlyOwner() {\n        require(msg.sender == seller, \"Not the seller\");\n        _;\n    }\n\n    constructor(uint256 startingBid, uint256 auctionDuration) {\n        seller = msg.sender;\n        highestBid = startingBid;\n        endAt = block.timestamp + auctionDuration;\n    }\n\n    /// @notice Place a bid in the auction\n    function bid() external payable {\n        require(block.timestamp < endAt, \"Auction expired\");\n        require(msg.value > highestBid, \"Bid too low\");\n\n        if (highestBidder != address(0)) {\n            pendingReturns[highestBidder] += highestBid;\n        }\n\n        highestBidder = msg.sender;\n        highestBid = msg.value;\n\n        emit BidPlaced(msg.sender, msg.value);\n    }\n\n    /// @notice Withdraw overbid funds\n    function withdraw() external returns (bool) {\n        uint256 amount = pendingReturns[msg.sender];\n        if (amount > 0) {\n            pendingReturns[msg.sender] = 0;\n            (bool success, ) = payable(msg.sender).call{value: amount}(\"\");\n            require(success, \"Transfer failed\");\n            return true;\n        }\n        return false;\n    }\n\n    /// @notice End the auction and transfer funds to seller\n    function end() external onlyOwner {\n        require(block.timestamp >= endAt, \"Auction not yet ended\");\n        require(!ended, \"Auction already ended\");\n\n        ended = true;\n        \n        (bool success, ) = payable(seller).call{value: highestBid}(\"\");\n        require(success, \"Transfer to seller failed\");\n\n        emit AuctionEnded(highestBidder, highestBid);\n    }\n\n    function getSeller() external view returns (address) { return seller; }\n    function getHighestBidder() external view returns (address) { return highestBidder; }\n    function getHighestBid() external view returns (uint256) { return highestBid; }\n    function getEnded() external view returns (bool) { return ended; }\n    function getEndAt() external view returns (uint256) { return endAt; }\n}"}
+{"task_id":"FormalEval/12","completion":"    address public seller;\n    uint256 public endAt;\n    bool public ended;\n\n    address public highestBidder;\n    uint256 public highestBid;\n\n    mapping(address => uint256) public pendingReturns;\n\n    event BidPlaced(address indexed bidder, uint256 amount);\n    event AuctionEnded(address indexed winner, uint256 amount);\n\n    modifier onlyOwner() {\n        require(msg.sender == seller, \"Not the seller\");\n        _;\n    }\n\n    constructor(uint256 _startingBid, uint256 _auctionDuration) {\n        seller = msg.sender;\n        highestBid = _startingBid;\n        endAt = block.timestamp + _auctionDuration;\n    }\n\n    function bid() external payable {\n        require(block.timestamp < endAt, \"Auction expired\");\n        require(msg.value > highestBid, \"Bid too low\");\n\n        if (highestBidder != address(0)) {\n            pendingReturns[highestBidder] += highestBid;\n        }\n\n        highestBidder = msg.sender;\n        highestBid = msg.value;\n\n        emit BidPlaced(msg.sender, msg.value);\n    }\n\n    function withdraw() external returns (bool) {\n        uint256 amount = pendingReturns[msg.sender];\n        if (amount > 0) {\n            pendingReturns[msg.sender] = 0;\n            (bool success, ) = payable(msg.sender).call{value: amount}(\"\");\n            require(success, \"Transfer failed\");\n        }\n        return true;\n    }\n\n    function end() external onlyOwner {\n        require(block.timestamp >= endAt, \"Auction not yet ended\");\n        require(!ended, \"Auction already ended\");\n\n        ended = true;\n        emit AuctionEnded(highestBidder, highestBid);\n\n        (bool success, ) = payable(seller).call{value: highestBid}(\"\");\n        require(success, \"Transfer to seller failed\");\n    }\n\n    function getSeller() external view returns (address) { return seller; }\n    function getHighestBidder() external view returns (address) { return highestBidder; }\n    function getHighestBid() external view returns (uint256) { return highestBid; }\n    function getEnded() external view returns (bool) { return ended; }\n    function getEndAt() external view returns (uint256) { return endAt; }\n}"}
+{"task_id":"FormalEval/12","completion":"    address public seller;\n    uint256 public endAt;\n    bool public ended;\n\n    address public highestBidder;\n    uint256 public highestBid;\n\n    mapping(address => uint256) public pendingReturns;\n\n    event BidPlaced(address indexed bidder, uint256 amount);\n    event AuctionEnded(address indexed winner, uint256 amount);\n\n    modifier onlySeller() {\n        require(msg.sender == seller, \"Not the seller\");\n        _;\n    }\n\n    constructor(uint256 _startingBid, uint256 _auctionDuration) {\n        seller = msg.sender;\n        highestBid = _startingBid;\n        endAt = block.timestamp + _auctionDuration;\n    }\n\n    function bid() external payable {\n        require(block.timestamp < endAt, \"Auction already ended\");\n        require(msg.value > highestBid, \"Bid too low\");\n\n        if (highestBidder != address(0)) {\n            pendingReturns[highestBidder] += highestBid;\n        }\n\n        highestBidder = msg.sender;\n        highestBid = msg.value;\n\n        emit BidPlaced(msg.sender, msg.value);\n    }\n\n    function withdraw() external returns (bool) {\n        uint256 amount = pendingReturns[msg.sender];\n        if (amount > 0) {\n            pendingReturns[msg.sender] = 0;\n            (bool success, ) = payable(msg.sender).call{value: amount}(\"\");\n            require(success, \"Transfer failed\");\n        }\n        return true;\n    }\n\n    function end() external onlySeller {\n        require(block.timestamp >= endAt, \"Auction not yet ended\");\n        require(!ended, \"Auction already ended\");\n\n        ended = true;\n        emit AuctionEnded(highestBidder, highestBid);\n\n        (bool success, ) = payable(seller).call{value: highestBid}(\"\");\n        require(success, \"Transfer to seller failed\");\n    }\n}"}
+{"task_id":"FormalEval/13","completion":"    address public owner;\n    uint256 public rewardPool;\n    bool private locked;\n\n    struct StakeInfo {\n        uint256 amount;\n        uint256 lastUpdateTime;\n        uint256 pendingRewards;\n    }\n\n    mapping(address => StakeInfo) public stakes;\n\n    event Staked(address indexed user, uint256 amount);\n    event Unstaked(address indexed user, uint256 amount);\n    event RewardsClaimed(address indexed user, uint256 amount);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the owner\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n    }\n\n    function _calculateRewards(address _addr) internal view returns (uint256) {\n        StakeInfo storage s = stakes[_addr];\n        if (s.amount == 0) return 0;\n        uint256 timeElapsed = block.timestamp - s.lastUpdateTime;\n        return s.pendingRewards + (s.amount * timeElapsed);\n    }\n\n    function stake() external payable {\n        require(msg.value > 0, \"Cannot stake 0\");\n        \n        _updateRewards(msg.sender);\n        stakes[msg.sender].amount += msg.value;\n        \n        emit Staked(msg.sender, msg.value);\n    }\n\n    function unstake(uint256 amount) external nonReentrant {\n        require(amount > 0, \"Amount must be > 0\");\n        require(stakes[msg.sender].amount >= amount, \"Insufficient stake\");\n\n        _updateRewards(msg.sender);\n        stakes[msg.sender].amount -= amount;\n        \n        (bool success, ) = payable(msg.sender).call{value: amount}(\"\");\n        require(success, \"Transfer failed\");\n        \n        emit Unstaked(msg.sender, amount);\n    }\n\n    function claimRewards() external nonReentrant {\n        _updateRewards(msg.sender);\n        uint256 reward = stakes[msg.sender].pendingRewards;\n        require(reward > 0, \"No rewards to claim\");\n        require(rewardPool >= reward, \"Insufficient reward pool\");\n\n        stakes[msg.sender].pendingRewards = 0;\n        rewardPool -= reward;\n\n        (bool success, ) = payable(msg.sender).call{value: reward}(\"\");\n        require(success, \"Transfer failed\");\n\n        emit RewardsClaimed(msg.sender, reward);\n    }\n\n    function _updateRewards(address _addr) internal {\n        stakes[_addr].pendingRewards = _calculateRewards(_addr);\n        stakes[_addr].lastUpdateTime = block.timestamp;\n    }\n\n    function fundRewards() external payable onlyOwner {\n        rewardPool += msg.value;\n    }\n\n    function getStake(address _addr) external view returns (uint256) {\n        return stakes[_addr].amount;\n    }\n\n    function getRewards(address _addr) external view returns (uint256) {\n        return _calculateRewards(_addr);\n    }\n}"}
+{"task_id":"FormalEval/13","completion":"    address public owner;\n    uint256 public rewardPool;\n    bool private locked;\n\n    struct User {\n        uint256 stakedAmount;\n        uint256 lastUpdateTime;\n        uint256 pendingRewards;\n    }\n\n    mapping(address => User) public users;\n\n    event Staked(address indexed user, uint256 amount);\n    event Unstaked(address indexed user, uint256 amount);\n    event RewardsClaimed(address indexed user, uint256 amount);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the owner\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n    }\n\n    function _calculateRewards(address _addr) internal view returns (uint256) {\n        User storage user = users[_addr];\n        if (user.stakedAmount == 0) return 0;\n        uint256 timeElapsed = block.timestamp - user.lastUpdateTime;\n        return user.stakedAmount * timeElapsed;\n    }\n\n    function _updateRewards(address _addr) internal {\n        users[_addr].pendingRewards += _calculateRewards(_addr);\n        users[_addr].lastUpdateTime = block.timestamp;\n    }\n\n    function stake() external payable {\n        require(msg.value > 0, \"Cannot stake 0\");\n        _updateRewards(msg.sender);\n        users[msg.sender].stakedAmount += msg.value;\n        emit Staked(msg.sender, msg.value);\n    }\n\n    function unstake(uint256 amount) external nonReentrant {\n        require(amount > 0, \"Amount must be > 0\");\n        require(users[msg.sender].stakedAmount >= amount, \"Insufficient stake\");\n        \n        _updateRewards(msg.sender);\n        users[msg.sender].stakedAmount -= amount;\n        \n        (bool success, ) = payable(msg.sender).call{value: amount}(\"\");\n        require(success, \"Transfer failed\");\n        \n        emit Unstaked(msg.sender, amount);\n    }\n\n    function claimRewards() external nonReentrant {\n        _updateRewards(msg.sender);\n        uint256 reward = users[msg.sender].pendingRewards;\n        require(reward > 0, \"No rewards to claim\");\n        require(rewardPool >= reward, \"Insufficient reward pool\");\n\n        users[msg.sender].pendingRewards = 0;\n        rewardPool -= reward;\n\n        (bool success, ) = payable(msg.sender).call{value: reward}(\"\");\n        require(success, \"Reward transfer failed\");\n\n        emit RewardsClaimed(msg.sender, reward);\n    }\n\n    function fundRewards() external payable onlyOwner {\n        rewardPool += msg.value;\n    }\n\n    function getStake(address _addr) external view returns (uint256) {\n        return users[_addr].stakedAmount;\n    }\n\n    function getRewards(address _addr) external view returns (uint256) {\n        return users[_addr].pendingRewards + _calculateRewards(_addr);\n    }\n}"}
+{"task_id":"FormalEval/13","completion":"    address public owner;\n    uint256 public rewardPool;\n    bool private locked;\n\n    struct StakeInfo {\n        uint256 amount;\n        uint256 lastUpdateTime;\n        uint256 pendingRewards;\n    }\n\n    mapping(address => StakeInfo) public stakes;\n\n    event Staked(address indexed user, uint256 amount);\n    event Unstaked(address indexed user, uint256 amount);\n    event RewardsClaimed(address indexed user, uint256 amount);\n\n    modifier onlyOwner() {\n        require(msg.sender == owner, \"Not the owner\");\n        _;\n    }\n\n    modifier nonReentrant() {\n        require(!locked, \"Reentrancy detected\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor() {\n        owner = msg.sender;\n    }\n\n    function _calculateRewards(address _addr) internal view returns (uint256) {\n        StakeInfo storage s = stakes[_addr];\n        if (s.amount == 0) return 0;\n        uint256 timeElapsed = block.timestamp - s.lastUpdateTime;\n        return s.pendingRewards + (s.amount * timeElapsed);\n    }\n\n    function stake() external payable {\n        require(msg.value > 0, \"Cannot stake 0\");\n        \n        _updateRewards(msg.sender);\n        stakes[msg.sender].amount += msg.value;\n        \n        emit Staked(msg.sender, msg.value);\n    }\n\n    function unstake(uint256 amount) external nonReentrant {\n        require(amount > 0, \"Amount must be > 0\");\n        require(stakes[msg.sender].amount >= amount, \"Insufficient stake\");\n\n        _updateRewards(msg.sender);\n        stakes[msg.sender].amount -= amount;\n        \n        (bool success, ) = payable(msg.sender).call{value: amount}(\"\");\n        require(success, \"Transfer failed\");\n        \n        emit Unstaked(msg.sender, amount);\n    }\n\n    function claimRewards() external nonReentrant {\n        _updateRewards(msg.sender);\n        uint256 reward = stakes[msg.sender].pendingRewards;\n        require(reward > 0, \"No rewards to claim\");\n        require(rewardPool >= reward, \"Insufficient reward pool\");\n\n        stakes[msg.sender].pendingRewards = 0;\n        rewardPool -= reward;\n\n        (bool success, ) = payable(msg.sender).call{value: reward}(\"\");\n        require(success, \"Reward transfer failed\");\n\n        emit RewardsClaimed(msg.sender, reward);\n    }\n\n    function _updateRewards(address _addr) internal {\n        stakes[_addr].pendingRewards = _calculateRewards(_addr);\n        stakes[_addr].lastUpdateTime = block.timestamp;\n    }\n\n    function fundRewards() external payable onlyOwner {\n        rewardPool += msg.value;\n    }\n\n    function getStake(address _addr) external view returns (uint256) {\n        return stakes[_addr].amount;\n    }\n\n    function getRewards(address _addr) external view returns (uint256) {\n        return _calculateRewards(_addr);\n    }\n}"}
+{"task_id":"FormalEval/14","completion":"    address public immutable tokenA;\n    address public immutable tokenB;\n\n    uint256 public reserveA;\n    uint256 public reserveB;\n    uint256 public totalSupply;\n\n    mapping(address => uint256) public balanceOf;\n\n    bool private locked;\n\n    event LiquidityAdded(address indexed provider, uint256 amountA, uint256 amountB, uint256 shares);\n    event LiquidityRemoved(address indexed provider, uint256 amountA, uint256 amountB, uint256 shares);\n    event Swap(address indexed user, address tokenIn, uint256 amountIn, uint256 amountOut);\n\n    modifier nonReentrant() {\n        require(!locked, \"ReentrancyGuard: reentrant call\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor(address _tokenA, address _tokenB) {\n        require(_tokenA != address(0) && _tokenB != address(0), \"Invalid token address\");\n        require(_tokenA != _tokenB, \"Tokens must be different\");\n        tokenA = _tokenA;\n        tokenB = _tokenB;\n    }\n\n    function _sqrt(uint256 y) internal pure returns (uint256 z) {\n        if (y > 3) {\n            z = y;\n            uint256 x = y / 2 + 1;\n            while (x < z) {\n                z = x;\n                x = (y / x + x) / 2;\n            }\n        } else if (y != 0) {\n            z = 1;\n        }\n    }\n\n    function getReserves() external view returns (uint256, uint256) {\n        return (reserveA, reserveB);\n    }\n\n    function addLiquidity(uint256 amountA, uint256 amountB) external nonReentrant returns (uint256 shares) {\n        IERC20(tokenA).transferFrom(msg.sender, address(this), amountA);\n        IERC20(tokenB).transferFrom(msg.sender, address(this), amountB);\n\n        if (totalSupply == 0) {\n            shares = _sqrt(amountA * amountB);\n        } else {\n            uint256 sharesA = (amountA * totalSupply) / reserveA;\n            uint256 sharesB = (amountB * totalSupply) / reserveB;\n            shares = sharesA < sharesB ? sharesA : sharesB;\n            require(shares > 0, \"Insufficient liquidity minted\");\n        }\n\n        balanceOf[msg.sender] += shares;\n        totalSupply += shares;\n        reserveA += amountA;\n        reserveB += amountB;\n\n        emit LiquidityAdded(msg.sender, amountA, amountB, shares);\n    }\n\n    function removeLiquidity(uint256 shares) external nonReentrant returns (uint256 amountA, uint256 amountB) {\n        require(shares <= balanceOf[msg.sender], \"Insufficient shares\");\n\n        amountA = (shares * reserveA) / totalSupply;\n        amountB = (shares * reserveB) / totalSupply;\n\n        balanceOf[msg.sender] -= shares;\n        totalSupply -= shares;\n        reserveA -= amountA;\n        reserveB -= amountB;\n\n        IERC20(tokenA).transfer(msg.sender, amountA);\n        IERC20(tokenB).transfer(msg.sender, amountB);\n\n        emit LiquidityRemoved(msg.sender, amountA, amountB, shares);\n    }\n\n    function swap(address tokenIn, uint256 amountIn) external nonReentrant returns (uint256 amountOut) {\n        require(tokenIn == tokenA || tokenIn == tokenB, \"Invalid token\");\n        require(amountIn > 0, \"Amount must be > 0\");\n\n        bool isA = tokenIn == tokenA;\n        (uint256 resIn, uint256 resOut) = isA ? (reserveA, reserveB) : (reserveB, reserveA);\n        address tokenOut = isA ? tokenB : tokenA;\n\n        IERC20(tokenIn).transferFrom(msg.sender, address(this), amountIn);\n\n        uint256 amountInWithFee = (amountIn * 997) / 1000;\n        amountOut = (resOut * amountInWithFee) / (resIn + amountInWithFee);\n\n        if (isA) {\n            reserveA += amountIn;\n            reserveB -= amountOut;\n        } else {\n            reserveB += amountIn;\n            reserveA -= amountOut;\n        }\n\n        IERC20(tokenOut).transfer(msg.sender, amountOut);\n\n        emit Swap(msg.sender, tokenIn, amountIn, amountOut);\n    }\n}"}
+{"task_id":"FormalEval/14","completion":"    address public immutable tokenA;\n    address public immutable tokenB;\n\n    uint256 public reserveA;\n    uint256 public reserveB;\n    uint256 public totalSupply;\n\n    mapping(address => uint256) public balanceOf;\n\n    bool private locked;\n\n    event LiquidityAdded(address indexed provider, uint256 amountA, uint256 amountB, uint256 shares);\n    event LiquidityRemoved(address indexed provider, uint256 amountA, uint256 amountB, uint256 shares);\n    event Swap(address indexed user, address tokenIn, uint256 amountIn, uint256 amountOut);\n\n    modifier nonReentrant() {\n        require(!locked, \"ReentrancyGuard: reentrant call\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor(address _tokenA, address _tokenB) {\n        require(_tokenA != address(0) && _tokenB != address(0), \"Invalid token addresses\");\n        require(_tokenA != _tokenB, \"Tokens must be different\");\n        tokenA = _tokenA;\n        tokenB = _tokenB;\n    }\n\n    function _sqrt(uint256 y) internal pure returns (uint256 z) {\n        if (y > 3) {\n            z = y;\n            uint256 x = y / 2 + 1;\n            while (x < z) {\n                z = x;\n                x = (y / x + x) / 2;\n            }\n        } else if (y != 0) {\n            z = 1;\n        }\n    }\n\n    function addLiquidity(uint256 amountA, uint256 amountB) external nonReentrant returns (uint256 shares) {\n        IERC20(tokenA).transferFrom(msg.sender, address(this), amountA);\n        IERC20(tokenB).transferFrom(msg.sender, address(this), amountB);\n\n        if (totalSupply == 0) {\n            shares = _sqrt(amountA * amountB);\n        } else {\n            uint256 sharesA = (amountA * totalSupply) / reserveA;\n            uint256 sharesB = (amountB * totalSupply) / reserveB;\n            shares = sharesA < sharesB ? sharesA : sharesB;\n            require(shares > 0, \"Insufficient liquidity minted\");\n        }\n\n        balanceOf[msg.sender] += shares;\n        totalSupply += shares;\n        reserveA += amountA;\n        reserveB += amountB;\n\n        emit LiquidityAdded(msg.sender, amountA, amountB, shares);\n    }\n\n    function removeLiquidity(uint256 shares) external nonReentrant returns (uint256 amountA, uint256 amountB) {\n        require(shares <= balanceOf[msg.sender], \"Insufficient shares\");\n\n        amountA = (shares * reserveA) / totalSupply;\n        amountB = (shares * reserveB) / totalSupply;\n\n        balanceOf[msg.sender] -= shares;\n        totalSupply -= shares;\n        reserveA -= amountA;\n        reserveB -= amountB;\n\n        IERC20(tokenA).transfer(msg.sender, amountA);\n        IERC20(tokenB).transfer(msg.sender, amountB);\n\n        emit LiquidityRemoved(msg.sender, amountA, amountB, shares);\n    }\n\n    function swap(address tokenIn, uint256 amountIn) external nonReentrant returns (uint256 amountOut) {\n        require(tokenIn == tokenA || tokenIn == tokenB, \"Invalid token\");\n        require(amountIn > 0, \"Invalid amount\");\n\n        bool isTokenA = tokenIn == tokenA;\n        (uint256 resIn, uint256 resOut) = isTokenA ? (reserveA, reserveB) : (reserveB, reserveA);\n        address tokenOut = isTokenA ? tokenB : tokenA;\n\n        IERC20(tokenIn).transferFrom(msg.sender, address(this), amountIn);\n\n        uint256 amountInWithFee = (amountIn * 997) / 1000;\n        amountOut = (resOut * amountInWithFee) / (resIn + amountInWithFee);\n\n        if (isTokenA) {\n            reserveA += amountIn;\n            reserveB -= amountOut;\n        } else {\n            reserveB += amountIn;\n            reserveA -= amountOut;\n        }\n\n        IERC20(tokenOut).transfer(msg.sender, amountOut);\n        emit Swap(msg.sender, tokenIn, amountIn, amountOut);\n    }\n\n    function getReserves() external view returns (uint256, uint256) {\n        return (reserveA, reserveB);\n    }\n\n    function totalShares() external view returns (uint256) {\n        return totalSupply;\n    }\n}"}
+{"task_id":"FormalEval/14","completion":"    address public immutable tokenA;\n    address public immutable tokenB;\n\n    uint256 public reserveA;\n    uint256 public reserveB;\n    uint256 public totalSupply;\n\n    mapping(address => uint256) public balanceOf;\n\n    bool private locked;\n\n    event LiquidityAdded(address indexed provider, uint256 amountA, uint256 amountB, uint256 shares);\n    event LiquidityRemoved(address indexed provider, uint256 amountA, uint256 amountB, uint256 shares);\n    event Swap(address indexed user, address tokenIn, uint256 amountIn, uint256 amountOut);\n\n    modifier nonReentrant() {\n        require(!locked, \"ReentrancyGuard: reentrant call\");\n        locked = true;\n        _;\n        locked = false;\n    }\n\n    constructor(address _tokenA, address _tokenB) {\n        require(_tokenA != address(0) && _tokenB != address(0), \"Invalid token addresses\");\n        require(_tokenA != _tokenB, \"Tokens must be different\");\n        tokenA = _tokenA;\n        tokenB = _tokenB;\n    }\n\n    function _sqrt(uint256 y) internal pure returns (uint256 z) {\n        if (y > 3) {\n            z = y;\n            uint256 x = y / 2 + 1;\n            while (x < z) {\n                z = x;\n                x = (y / x + x) / 2;\n            }\n        } else if (y != 0) {\n            z = 1;\n        }\n    }\n\n    function getReserves() external view returns (uint256, uint256) {\n        return (reserveA, reserveB);\n    }\n\n    function addLiquidity(uint256 amountA, uint256 amountB) external nonReentrant returns (uint256 shares) {\n        IERC20(tokenA).transferFrom(msg.sender, address(this), amountA);\n        IERC20(tokenB).transferFrom(msg.sender, address(this), amountB);\n\n        if (totalSupply == 0) {\n            shares = _sqrt(amountA * amountB);\n        } else {\n            uint256 sharesA = (amountA * totalSupply) / reserveA;\n            uint256 sharesB = (amountB * totalSupply) / reserveB;\n            shares = sharesA < sharesB ? sharesA : sharesB;\n            require(shares > 0, \"Insufficient liquidity minted\");\n        }\n\n        balanceOf[msg.sender] += shares;\n        totalSupply += shares;\n        reserveA += amountA;\n        reserveB += amountB;\n\n        emit LiquidityAdded(msg.sender, amountA, amountB, shares);\n    }\n\n    function removeLiquidity(uint256 shares) external nonReentrant returns (uint256 amountA, uint256 amountB) {\n        require(shares > 0 && balanceOf[msg.sender] >= shares, \"Invalid shares\");\n\n        amountA = (shares * reserveA) / totalSupply;\n        amountB = (shares * reserveB) / totalSupply;\n\n        balanceOf[msg.sender] -= shares;\n        totalSupply -= shares;\n        reserveA -= amountA;\n        reserveB -= amountB;\n\n        IERC20(tokenA).transfer(msg.sender, amountA);\n        IERC20(tokenB).transfer(msg.sender, amountB);\n\n        emit LiquidityRemoved(msg.sender, amountA, amountB, shares);\n    }\n\n    function swap(address tokenIn, uint256 amountIn) external nonReentrant returns (uint256 amountOut) {\n        require(tokenIn == tokenA || tokenIn == tokenB, \"Invalid token\");\n        require(amountIn > 0, \"Invalid amount\");\n\n        bool isA = tokenIn == tokenA;\n        (uint256 resIn, uint256 resOut) = isA ? (reserveA, reserveB) : (reserveB, reserveA);\n        address tokenOut = isA ? tokenB : tokenA;\n\n        IERC20(tokenIn).transferFrom(msg.sender, address(this), amountIn);\n\n        uint256 amountInWithFee = (amountIn * 997) / 1000;\n        amountOut = (resOut * amountInWithFee) / (resIn + amountInWithFee);\n\n        if (isA) {\n            reserveA += amountIn;\n            reserveB -= amountOut;\n        } else {\n            reserveB += amountIn;\n            reserveA -= amountOut;\n        }\n\n        IERC20(tokenOut).transfer(msg.sender, amountOut);\n\n        emit Swap(msg.sender, tokenIn, amountIn, amountOut);\n    }\n}"}

biome.json

@@ -1,55 +1,53 @@
 {
-	"$schema": "https://biomejs.dev/schemas/2.4.14/schema.json",
-	"vcs": {
-		"enabled": true,
-		"clientKind": "git",
-		"useIgnoreFile": true
-	},
-	"files": {
-		"includes": [
-			"**",
-			"!!**/dist"
-		]
-	},
-	"formatter": {
-		"enabled": true,
-		"lineWidth": 120,
-		"indentStyle": "space"
-	},
-	"linter": {
-		"enabled": true,
-		"rules": {
-			"recommended": true,
-			"suspicious": {
-				"noUnknownAtRules": "off",
-				"noArrayIndexKey": "off",
-				"noExplicitAny": "off"
-			},
-			"complexity": {
-				"noStaticOnlyClass": "off"
-			},
-			"correctness": {
-				"useExhaustiveDependencies": "off",
-				"useParseIntRadix": "off"
-			},
-			"a11y": "off",
-			"style": {
-				"noNonNullAssertion": "off",
-				"useTemplate": "off"
-			}
-		}
-	},
-	"javascript": {
-		"formatter": {
-			"quoteStyle": "double"
-		}
-	},
-	"assist": {
-		"enabled": true,
-		"actions": {
-			"source": {
-				"organizeImports": "on"
-			}
-		}
-	}
+  "$schema": "https://biomejs.dev/schemas/2.4.14/schema.json",
+  "vcs": {
+    "enabled": true,
+    "clientKind": "git",
+    "useIgnoreFile": true
+  },
+  "files": {
+    "includes": ["**", "!!**/dist"]
+  },
+  "formatter": {
+    "enabled": true,
+    "lineWidth": 120,
+    "indentStyle": "space"
+  },
+  "linter": {
+    "enabled": true,
+    "rules": {
+      "recommended": true,
+      "suspicious": {
+        "noUnknownAtRules": "off",
+        "noArrayIndexKey": "off",
+        "noExplicitAny": "off",
+        "noAssignInExpressions": "off"
+      },
+      "complexity": {
+        "noStaticOnlyClass": "off"
+      },
+      "correctness": {
+        "useExhaustiveDependencies": "off",
+        "useParseIntRadix": "off"
+      },
+      "a11y": "off",
+      "style": {
+        "noNonNullAssertion": "off",
+        "useTemplate": "off"
+      }
+    }
+  },
+  "javascript": {
+    "formatter": {
+      "quoteStyle": "double"
+    }
+  },
+  "assist": {
+    "enabled": true,
+    "actions": {
+      "source": {
+        "organizeImports": "on"
+      }
+    }
+  }
 }

package-lock.json

@@ -11,7 +11,7 @@
       "license": "ISC",
       "dependencies": {
         "@hono/node-server": "^2.0.3",
-        "@langchain/anthropic": "^1.3.29",
+        "@langchain/anthropic": "^1.4.1",
         "@langchain/core": "^1.1.45",
         "@langchain/google-genai": "^2.1.31",
         "@langchain/langgraph": "^1.3.2",
@@ -36,9 +36,9 @@
       }
     },
     "node_modules/@anthropic-ai/sdk": {
-      "version": "0.95.2",
-      "resolved": "https://registry.npmjs.org/@anthropic-ai/sdk/-/sdk-0.95.2.tgz",
-      "integrity": "sha512-Egddwo3sheo1PzUrMkZnH6VkQYwS0h/b/i8vSK8Ta9M45UQipAMeDFH57dYuDAfXMEUUGeKw6CMlremgMZgrSQ==",
+      "version": "0.103.0",
+      "resolved": "https://registry.npmjs.org/@anthropic-ai/sdk/-/sdk-0.103.0.tgz",
+      "integrity": "sha512-1uG7RNgoHTUxzOXqSCODKt0UTVlxWiHk/2Tt2/uQJiPW7XzBeKVuJyd3Aw6T3LPyvZV/jDTnPLX7SaM70WLLjA==",
       "license": "MIT",
       "dependencies": {
         "json-schema-to-ts": "^3.1.1",
@@ -199,23 +199,25 @@
       }
     },
     "node_modules/@langchain/anthropic": {
-      "version": "1.4.0",
-      "resolved": "https://registry.npmjs.org/@langchain/anthropic/-/anthropic-1.4.0.tgz",
-      "integrity": "sha512-rs1yVydrHjyiD31uChdCnKZpmDuKa0Bpz8Raiy9GvqnqmfXPMe0oOrap/2paE+NRSinDbtax8mMpP/yv8EbO1A==",
+      "version": "1.4.1",
+      "resolved": "https://registry.npmjs.org/@langchain/anthropic/-/anthropic-1.4.1.tgz",
+      "integrity": "sha512-h3b6hxThcfh0WdmpuWr+qBi74MN+0BpNI/4H681vwXxbD3hLr2qMYN6ghqcPQhCxGJjg8ufs85qu2/ldSWonYQ==",
       "license": "MIT",
       "dependencies": {
-        "@anthropic-ai/sdk": "^0.95.1",
+        "@anthropic-ai/sdk": "^0.103.0",
         "zod": "^3.25.76 || ^4"
       },
       "engines": {
         "node": ">=20"
       },
       "peerDependencies": {
-        "@langchain/core": "^1.1.47"
+        "@langchain/core": "^1.1.49"
       }
     },
     "node_modules/@langchain/core": {
-      "version": "1.1.47",
+      "version": "1.1.49",
+      "resolved": "https://registry.npmjs.org/@langchain/core/-/core-1.1.49.tgz",
+      "integrity": "sha512-7wkN3Qv/qZqsY0p3h48CNu6E6y5GMYatYxj+JrX4uVNBiqIVQm1Z528QrmayJWVW9SQTQicqRNoyTCzl+K9F8Q==",
       "license": "MIT",
       "dependencies": {
         "@cfworker/json-schema": "^4.0.2",

package.json

@@ -11,6 +11,7 @@
     "start": "npm run build && node dist/index.js",
     "server": "npm run build && node dist/server.js",
     "dev:server": "npx tsx src/server.ts",
+    "benchmark": "npx tsx benchmarks/run-formal-eval.ts",
     "postinstall": "patch-package"
   },
   "repository": {
@@ -33,7 +34,7 @@
   },
   "dependencies": {
     "@hono/node-server": "^2.0.3",
-    "@langchain/anthropic": "^1.3.29",
+    "@langchain/anthropic": "^1.4.1",
     "@langchain/core": "^1.1.45",
     "@langchain/google-genai": "^2.1.31",
     "@langchain/langgraph": "^1.3.2",

src/agents/auditor/agent.ts

@@ -1,61 +1,27 @@
 import fs from "node:fs";
-import path from "node:path";
 
 import { HumanMessage, SystemMessage } from "@langchain/core/messages";
 import { END, type GraphNode, START, StateGraph } from "@langchain/langgraph";
 import { z } from "zod";
 
-import { logger } from "../../logger.ts";
 import { createLLM } from "../../config/llm.ts";
-import { emitStep } from "../../logger.ts";
-import { JUDGE_FINDINGS_PROMPT, FIND_VULNERABILITIES_PROMPT, GATHER_CONTEXT_PROMPT } from "./prompts.ts";
-import { AuditorState, JudgeReviewSchema, CandidateFindingSchema } from "./state.ts";
-import { analyzeSolidityFile } from "./tools/solidity-analyzer-tool.ts";
-import { buildRepoTree } from "./tools/repo-tree-tool.ts";
+import { emitStep, logger } from "../../logger.ts";
+import { MAX_DOC_CHARS, MAX_REFLECTIONS, MAX_SOL_CHARS, MIN_FILE_IMPORTANCE } from "./config.ts";
 import {
-  DOC_BASENAMES,
-  DOC_EXTS,
-  MAX_DEPTH,
-  MAX_DOC_CHARS,
-  MAX_REFLECTIONS,
-  MAX_SOL_CHARS,
-  SKIP_DIRS,
-  SOL_EXT,
-  SOL_TEST_SUFFIXES,
-} from "./config.ts";
-import { matchLines } from "./utils.ts";
-
-const llm = createLLM();
-
-const walkDirectory = (dir: string, depth: number, solFiles: string[], docFiles: string[]) => {
-  if (depth > MAX_DEPTH) return;
-
-  let entries: fs.Dirent[];
-  try {
-    entries = fs.readdirSync(dir, { withFileTypes: true });
-  } catch {
-    return;
-  }
-
-  for (const entry of entries) {
-    if (entry.isDirectory()) {
-      if (!SKIP_DIRS.has(entry.name)) {
-        walkDirectory(path.join(dir, entry.name), depth + 1, solFiles, docFiles);
-      }
-    } else if (entry.isFile()) {
-      const fullPath = path.join(dir, entry.name);
-      const ext = path.extname(entry.name).toLowerCase();
-      const base = path.basename(entry.name, ext).toLowerCase();
-
-      if (ext === SOL_EXT) {
-        const isTest = SOL_TEST_SUFFIXES.some((suffix) => entry.name.endsWith(suffix));
-        if (!isTest) solFiles.push(fullPath);
-      } else if (DOC_EXTS.has(ext) || DOC_BASENAMES.has(base)) {
-        docFiles.push(fullPath);
-      }
-    }
-  }
-};
+  FIND_VULNERABILITIES_PROMPT,
+  GATHER_CONTEXT_PROMPT,
+  JUDGE_FINDINGS_PROMPT,
+  RANK_FILES_PROMPT,
+  REFINE_VULNERABILITIES_PROMPT,
+} from "./prompts.ts";
+import { AuditorState, CandidateFindingSchema, FileRankingSchema, JudgeReviewSchema } from "./state.ts";
+import { buildRepoTree } from "./tools/repo-tree/tool.ts";
+import { analyzeSolidityFile } from "./tools/solidity-analyzer/tool.ts";
+import { buildReviewBlocks, matchLines, walkDirectory } from "./utils.ts";
+
+const llmHaiku = createLLM("anthropic", { model: "claude-haiku-4-5", maxTokens: 20000 });
+const llmOpus = createLLM("anthropic", { model: "claude-opus-4-8", temperature: null, maxTokens: 20000 });
+const llmSonnet = createLLM("anthropic", { model: "claude-sonnet-4-6", maxTokens: 20000 });
 
 const defineScope: GraphNode<typeof AuditorState> = async (state) => {
   emitStep({ agent: "auditor", step: "scope", status: "running" });
@@ -68,18 +34,48 @@ const defineScope: GraphNode<typeof AuditorState> = async (state) => {
 
   const fileTree = buildRepoTree(state.repoPath);
 
-  logger.info(`[Auditor] defineScope: encontrado(s) ${solFiles.length} arquivo(s) Solidity e ${docFiles.length} arquivo(s) de documentação`);
+  logger.info(
+    `[Auditor] defineScope: encontrado(s) ${solFiles.length} arquivo(s) Solidity e ${docFiles.length} arquivo(s) de documentação`,
+  );
   logger.debug(`[Auditor] defineScope: arquivos Solidity: ${JSON.stringify(solFiles)}`);
   logger.debug(`[Auditor] defineScope: arquivos de documentação: ${JSON.stringify(docFiles)}`);
   logger.debug(`[Auditor] defineScope: árvore de arquivos:\n${fileTree}`);
 
   emitStep({ agent: "auditor", step: "scope", status: "done" });
-  return { scope: solFiles, docs: docFiles, fileTree };
+
+  logger.info("[Auditor] defineScope: rankeando arquivos por importância");
+
+  const RankFilesSchema = z.object({ rankings: z.array(FileRankingSchema) });
+  const rankingModel = llmHaiku.withStructuredOutput(RankFilesSchema);
+
+  const { rankings } = await rankingModel.invoke([
+    new SystemMessage({ content: [{ type: "text", text: RANK_FILES_PROMPT, cache_control: { type: "ephemeral" } }] }),
+    new HumanMessage(
+      `Árvore de arquivos:\n\`\`\`\n${fileTree}\n\`\`\`\n\nArquivos Solidity para classificar:\n${solFiles.map((f) => `- ${f}`).join("\n")}`,
+    ),
+  ]);
+
+  const sorted = [...rankings].sort((a, b) => b.importance - a.importance);
+  logger.info(
+    `[Auditor] defineScope: rankings:\n${sorted.map((r) => `  [${r.importance}/5] ${r.filePath} — ${r.reasoning}`).join("\n")}`,
+  );
+
+  const importantFiles = sorted.filter((r) => r.importance >= MIN_FILE_IMPORTANCE).map((r) => r.filePath);
+  const skipped = solFiles.length - importantFiles.length;
+  if (skipped > 0) {
+    logger.info(
+      `[Auditor] defineScope: pulando ${skipped} arquivo(s) de baixa importância (importância < ${MIN_FILE_IMPORTANCE})`,
+    );
+  }
+
+  return { scope: importantFiles, docs: docFiles, fileTree, fileRankings: sorted };
 };
 
 const gatherContext: GraphNode<typeof AuditorState> = async (state) => {
   emitStep({ agent: "auditor", step: "ctx", status: "running" });
-  logger.info(`[Auditor] gatherContext: processando ${state.scope.length} arquivo(s) Solidity e ${state.docs.length} arquivo(s) de documentação`);
+  logger.info(
+    `[Auditor] gatherContext: processando ${state.scope.length} arquivo(s) Solidity e ${state.docs.length} arquivo(s) de documentação`,
+  );
 
   const readFile = (filePath: string): string => {
     try {
@@ -89,102 +85,120 @@ const gatherContext: GraphNode<typeof AuditorState> = async (state) => {
     }
   };
 
-  // Read and analyze each Solidity file
   const solidityEntries: { filePath: string; source: string; analysis: string }[] = [];
   for (const filePath of state.scope) {
     const source = readFile(filePath).slice(0, MAX_SOL_CHARS);
     if (!source) continue;
-    const analysis = await analyzeSolidityFile(source, "full");
+
+    const ranking = state.fileRankings.find((r) => r.filePath === filePath);
+    const mode = ranking && ranking.importance >= 4 ? "full" : "short";
+    const analysis = await analyzeSolidityFile(source, mode, filePath, ranking?.importance);
     solidityEntries.push({ filePath, source, analysis });
   }
 
-  // Read documentation files
   const docEntries: { filePath: string; content: string }[] = [];
   for (const filePath of state.docs) {
     const content = readFile(filePath).slice(0, MAX_DOC_CHARS);
     if (content) docEntries.push({ filePath, content });
   }
 
-  // Build the LLM input
   const parts: string[] = [];
 
   if (docEntries.length > 0) {
-    parts.push("## Documentation\n");
+    parts.push("## Documentação\n");
     for (const { filePath, content } of docEntries) {
       parts.push(`### ${filePath}\n${content}`);
     }
   }
 
-  parts.push("## Structural Analysis (auto-generated)\n");
-  for (const { filePath, analysis } of solidityEntries) {
-    parts.push(`### ${filePath}\n${analysis}`);
-  }
+  parts.push(`## Árvore de Arquivos\n\n\`\`\`\n${state.fileTree}\n\`\`\``);
 
-  parts.push("## Contract Source Code\n");
-  for (const { filePath, source } of solidityEntries) {
-    parts.push(`### ${filePath}\n\`\`\`solidity\n${source}\n\`\`\``);
+  parts.push("## Análise Estrutural\n");
+  for (const { analysis } of solidityEntries) {
+    parts.push(analysis);
   }
 
-  const model = llm.withStructuredOutput(z.object({ context: z.string() }));
-  const result = await model.invoke([new SystemMessage(GATHER_CONTEXT_PROMPT), new HumanMessage(parts.join("\n\n"))]);
+  const model = llmHaiku.withStructuredOutput(z.object({ context: z.string() }));
+  const result = await model.invoke([
+    new SystemMessage({
+      content: [{ type: "text", text: GATHER_CONTEXT_PROMPT, cache_control: { type: "ephemeral" } }],
+    }),
+    new HumanMessage(parts.join("\n\n")),
+  ]);
+
+  const fileTreeBlock = `## Árvore de Arquivos\n\n\`\`\`\n${state.fileTree}\n\`\`\``;
+  const structuralBlock = `## Análise Estrutural dos Contratos\n\n${solidityEntries.map(({ analysis }) => analysis).join("\n\n---\n\n")}`;
+  const repoContext = [result.context, fileTreeBlock, structuralBlock].join("\n\n");
 
-  logger.info(`[Auditor] gatherContext: contexto construído (${parts.join("\n\n").length} caracteres)`);
   logger.debug(`[Auditor] gatherContext: contexto completo:\n${parts.join("\n\n")}`);
+  logger.info(`[Auditor] gatherContext: contexto construído (${repoContext.length} caracteres)`);
+  logger.debug(`[Auditor] gatherContext: contexto compactado:\n${repoContext}`);
 
   emitStep({ agent: "auditor", step: "ctx", status: "done" });
-  return { repoContext: result.context };
+
+  return { repoContext };
 };
 
 const findVulnerabilities: GraphNode<typeof AuditorState> = async (state) => {
-  const model = llm.withStructuredOutput(z.object({ findings: z.array(CandidateFindingSchema) }));
-
-  const previousFeedback =
-    state.judgeReviews.length > 0
-      ? state.judgeReviews
-          .map((r, i) => {
-            const title = state.candidateFindings[i]?.title ?? `Finding ${i + 1}`;
-            return `- "${title}": ${r.isFalsePositive ? "FALSE POSITIVE" : "TRUE POSITIVE"}\n  Judge: ${r.review}`;
-          })
-          .join("\n")
-      : null;
+  const model = llmOpus.withStructuredOutput(z.object({ findings: z.array(CandidateFindingSchema) }));
+
+  const isReflection = state.judgeReviews.length > 0;
 
   logger.info(
     `[Auditor] findVulnerabilities: invocando LLM para ${state.scope.length} arquivo(s) em paralelo (iteração ${state.reflectionCount + 1})`,
   );
+
   emitStep({ agent: "auditor", step: "find", status: "running", detail: `iter ${state.reflectionCount + 1}` });
 
-  const allFindings = await Promise.all(
-    state.scope.map(async (filePath) => {
-      let source: string;
-      try {
-        source = fs.readFileSync(filePath, "utf-8").slice(0, MAX_SOL_CHARS);
-      } catch {
-        return [];
-      }
-      if (!source) return [];
-
-      let userMessage = `Contract (${filePath}):\n\n${source}\n\nProtocol Context:\n${state.repoContext}`;
-      if (previousFeedback) {
-        userMessage += `\n\nJudge feedback from previous iteration (iteration ${state.reflectionCount}):\n${previousFeedback}\n\nRevise your findings accordingly.`;
-      }
-
-      logger.debug(`[Auditor] findVulnerabilities: processando ${filePath}`);
-
-      const result = await model.invoke([
-        new SystemMessage(FIND_VULNERABILITIES_PROMPT),
-        new HumanMessage(userMessage),
-      ]);
-
-      return result.findings.map((finding: any) => ({
-        ...finding,
-        path: filePath,
-        location: matchLines(source, finding.codeSnippet) ?? "",
-      }));
-    }),
-  );
+  const cachedContext = {
+    type: "text" as const,
+    text: `Contexto do Protocolo:\n${state.repoContext}`,
+    cache_control: { type: "ephemeral" as const },
+  };
+
+  const processFile = async (filePath: string) => {
+    let source: string;
+    try {
+      source = fs.readFileSync(filePath, "utf-8").slice(0, MAX_SOL_CHARS);
+    } catch {
+      return [];
+    }
+    if (!source) return [];
+
+    const fileEntries = isReflection
+      ? state.candidateFindings
+          .map((f, i) => ({ finding: f, review: state.judgeReviews[i] }))
+          .filter(({ finding }) => finding.path === filePath)
+      : [];
+
+    const isRefinement = fileEntries.length > 0;
+    const promptText = isRefinement ? REFINE_VULNERABILITIES_PROMPT : FIND_VULNERABILITIES_PROMPT;
+    const contractText = isRefinement
+      ? `Contrato (${filePath}):\n\n${source}\n\n${buildReviewBlocks(fileEntries, state.reflectionCount)}`
+      : `Contrato (${filePath}):\n\n${source}`;
+
+    logger.debug(`[Auditor] findVulnerabilities: processando ${filePath}`);
+
+    const result = await model.invoke([
+      new SystemMessage({ content: [{ type: "text", text: promptText, cache_control: { type: "ephemeral" } }] }),
+      new HumanMessage({ content: [cachedContext, { type: "text", text: contractText }] }),
+    ]);
+
+    return result.findings.map((finding: any) => ({
+      ...finding,
+      path: filePath,
+      location: matchLines(source, finding.codeSnippet) ?? "",
+    }));
+  };
+
+  const [firstFile, ...restFiles] = state.scope;
+  const firstFindings = firstFile ? await processFile(firstFile) : [];
+  const restFindings = await Promise.all(restFiles.map(processFile));
+  const candidateFindings = [firstFindings, ...restFindings].flat();
 
-  const candidateFindings = allFindings.flat();
-  logger.info(`[Auditor] findVulnerabilities: LLM retornou ${candidateFindings.length} finding(s) candidato(s) no total`);
+  logger.info(
+    `[Auditor] findVulnerabilities: LLM retornou ${candidateFindings.length} finding(s) candidato(s) no total`,
+  );
   logger.debug(`[Auditor] findVulnerabilities: findings:\n${JSON.stringify(candidateFindings, null, 2)}`);
 
   emitStep({ agent: "auditor", step: "find", status: "done" });
@@ -203,30 +217,46 @@ const judgeFindings: GraphNode<typeof AuditorState> = async (state) => {
     };
   }
 
-  const model = llm.withStructuredOutput(JudgeReviewSchema);
+  const model = llmSonnet.withStructuredOutput(JudgeReviewSchema);
 
-  logger.info(`[Auditor] judgeFindings: revisando ${state.candidateFindings.length} finding(s) candidato(s) em paralelo`);
+  logger.info(
+    `[Auditor] judgeFindings: revisando ${state.candidateFindings.length} finding(s) candidato(s) em paralelo`,
+  );
 
-  const reviews = await Promise.all(
-    state.candidateFindings.map(async (finding, i) => {
-      let source: string;
-      try {
-        source = fs.readFileSync(finding.path, "utf-8").slice(0, MAX_SOL_CHARS);
-      } catch {
-        source = "";
-      }
+  const cachedContext = {
+    type: "text" as const,
+    text: `Contexto do Protocolo:\n${state.repoContext}`,
+    cache_control: { type: "ephemeral" as const },
+  };
 
-      const findingText = `[Finding ${i + 1}] ${finding.title}\nSeverity: ${finding.severity}\nDescription: ${finding.description}\nLocation: ${finding.path} lines ${finding.location}\nCode:\n\`\`\`solidity\n${finding.codeSnippet}\n\`\`\``;
+  const reviewFinding = async (finding: (typeof state.candidateFindings)[number], i: number) => {
+    let source: string;
+    try {
+      source = fs.readFileSync(finding.path, "utf-8").slice(0, MAX_SOL_CHARS);
+    } catch {
+      source = "";
+    }
 
-      logger.debug(`[Auditor] judgeFindings: revisando finding ${i + 1}: ${finding.title}`);
-      return model.invoke([
-        new SystemMessage(JUDGE_FINDINGS_PROMPT),
-        new HumanMessage(
-          `Contract (${finding.path}):\n\n${source}\n\nProtocol Context:\n${state.repoContext}\n\nFinding to Review:\n\n${findingText}`,
-        ),
-      ]);
-    }),
-  );
+    const findingText = `[Achado ${i + 1}] ${finding.title}\nSeveridade: ${finding.severity}\nDescrição: ${finding.description}\nLocalização: ${finding.path} linhas ${finding.location}\nCódigo:\n\`\`\`solidity\n${finding.codeSnippet}\n\`\`\``;
+
+    logger.debug(`[Auditor] judgeFindings: revisando finding ${i + 1}: ${finding.title}`);
+    return model.invoke([
+      new SystemMessage({
+        content: [{ type: "text", text: JUDGE_FINDINGS_PROMPT, cache_control: { type: "ephemeral" } }],
+      }),
+      new HumanMessage({
+        content: [
+          cachedContext,
+          { type: "text", text: `Contrato (${finding.path}):\n\n${source}\n\nAchado para Revisão:\n\n${findingText}` },
+        ],
+      }),
+    ]);
+  };
+
+  const [firstFinding, ...restFindings] = state.candidateFindings;
+  const firstReview = await reviewFinding(firstFinding, 0);
+  const restReviews = await Promise.all(restFindings.map((f, i) => reviewFinding(f, i + 1)));
+  const reviews = [firstReview, ...restReviews];
 
   const confirmedEntries = state.candidateFindings
     .map((finding, i) => ({ finding, review: reviews[i] }))

src/agents/auditor/config.ts

@@ -20,4 +20,5 @@ export const SKIP_DIRS = new Set([
 export const MAX_DEPTH = 6;
 export const MAX_DOC_CHARS = 12_000;
 export const MAX_SOL_CHARS = 40_000;
-export const MAX_REFLECTIONS = 1;
+export const MAX_REFLECTIONS = 3;
+export const MIN_FILE_IMPORTANCE = 3;

src/agents/auditor/prompts.ts

@@ -1,50 +1,131 @@
-export const GATHER_CONTEXT_PROMPT = `Você é um especialista em segurança de smart contracts. Você receberá documentação, uma análise estrutural e o código-fonte completo de todos os contratos Solidity em escopo. Produza um contexto detalhado do protocolo que guiará a descoberta de vulnerabilidades.
+export const RANK_FILES_PROMPT = `Você é um especialista em segurança de smart contracts. Dada a árvore de arquivos do repositório e uma lista de contratos Solidity, classifique cada arquivo pela sua importância para a descoberta de vulnerabilidades de segurança.
 
-Estruture sua resposta nas seguintes seções:
+Para cada arquivo atribua:
+- importance: inteiro de 1 (menos importante) a 5 (mais importante)
+- reasoning: uma frase concisa justificando a classificação (mencione o papel específico do contrato, não categorias genéricas)
 
-## 1. Visão Geral dos Contratos
-Para cada contrato: seu propósito, tipo (contract/interface/library/abstract), cadeia de herança e principais dependências de outros contratos em escopo ou protocolos externos.
+Critérios de classificação:
+- Importância 5: lógica central do protocolo (vaults, pools, engines), custódia de tokens/ETH, mecanismos de upgrade/proxy, cálculos financeiros críticos (preço, juros, liquidação), controle de acesso raiz.
+- Importância 4: contratos que movem valor e interagem diretamente com os de importância 5, máquinas de estado complexas, distribuição de taxas/recompensas, roteadores de entrada.
+- Importância 3: helpers periféricos com lógica de negócio, bibliotecas reutilizáveis com efeitos colaterais, governança com timelocks.
+- Importância 2: interfaces, adaptadores, wrappers triviais, contratos utilitários sem lógica crítica.
+- Importância 1: views somente-leitura, arquivos de constantes/configuração pura, mocks e scripts de deploy.
 
-## 2. Mapa de Estado e Armazenamento
-Liste todas as variáveis de estado relevantes entre os contratos, o que representam e quais funções as leem ou escrevem. Sinalize armazenamento compartilhado ou herdado.
+Retorne a classificação de TODOS os arquivos fornecidos, sem omitir nenhum.`;
 
-## 3. Fluxos Principais
-Trace os principais caminhos de execução e transições de estado de ponta a ponta entre contratos (ex.: depósito → cunhar shares → atualizar recompensas; saque → queimar shares → transferir ETH). Inclua chamadas entre contratos.
+export const GATHER_CONTEXT_PROMPT = `Você é um especialista em segurança de smart contracts criando um modelo mental preciso do protocolo para auditoria. Você receberá documentação e a análise estrutural dos contratos Solidity em escopo.
 
-## 4. Invariantes
-Condições que devem sempre ser verdadeiras (ex.: "o supply total deve ser igual à soma de todos os saldos", "o saldo de ETH do contrato ≥ soma de todos os depósitos dos usuários"). Derive-as tanto do código-fonte quanto da documentação.
+**REGRA DE FIDELIDADE FACTUAL — NÃO NEGOCIÁVEL**: Baseie-se EXCLUSIVAMENTE no que está EXPLICITAMENTE presente no código-fonte (linhas de código, NatSpec, comentários inline) ou na documentação fornecida. NUNCA infira, suponha, extrapole ou "complete" informações que não estejam literalmente escritas nas fontes. Se uma informação não aparece explicitamente, NÃO a inclua e NÃO a invente. Esta regra se aplica a TODAS as seções. **Na seção Trust Assumptions esta proibição é ABSOLUTA: se não há declaração explícita (código, NatSpec, comentário ou doc) sobre uma suposição, ela não existe para você.**
 
-## 5. Premissas de Design
-O que o protocolo assume sobre chamadores, contratos externos, oráculos, chaves de administrador e comportamento de tokens (ex.: "tokens são compatíveis com ERC-20", "o admin é confiável", "sem tokens com taxa de transferência").
+Produza um contexto factual e detalhado de auditoria sem introduções, sem padding e sem repetições. Preserve nomes concretos (funções, variáveis, tipos, valores numéricos) exatamente como aparecem no código. Sem prosa explicativa.
 
-## 6. Regras de Negócio
-Controles de acesso, estruturas de taxas, timelocks, limites, mecanismos de pausa, padrões de atualização e quaisquer outras restrições de domínio.
+A árvore de arquivos do repositório e a análise estrutural completa de cada contrato serão anexadas automaticamente ao final do contexto — **não as duplique**. Concentre-se nas seções de síntese abaixo.
 
-Seja preciso e exaustivo — quanto mais rico o contexto, com mais precisão as vulnerabilidades podem ser identificadas e validadas.`;
+## Visão geral
+Descreva o propósito do protocolo, o fluxo econômico principal, os participantes envolvidos e os ativos protegidos — apenas o que estiver explicitamente declarado no código ou na documentação.
 
-export const FIND_VULNERABILITIES_PROMPT = `Você é um auditor especialista em segurança de smart contracts com foco em Solidity. Analise sistematicamente o código-fonte do contrato e o contexto do protocolo para identificar vulnerabilidades de segurança.
+## Estado Crítico
+Todas as variáveis de estado com impacto em lógica de negócio, segurança ou contabilidade, extraídas diretamente da seção Storage da análise estrutural.
+Formato por bullet: \`filePath::nomeVar (tipo, visibilidade) — NatSpec/comentário se presente — funções que escrevem nela — impacto se manipulada\`.
+Omita apenas constantes e imutáveis puramente administrativas (nome do token, símbolo, decimals, versão de string).
 
-Para cada vulnerabilidade, forneça TODOS os seguintes campos:
+## Fluxos Principais (máx. 5 fluxos, 3–6 passos cada)
+Apenas os caminhos críticos ponta a ponta que movem valor ou alteram estado relevante, derivados das funções e call graphs observados no código.
+Formato por passo: \`ação (função) → efeito colateral → variável/estado alterado\`.
+Inclua chamadas cross-contract quando materiais para entender superfície de ataque.
 
-- **title**: Nome curto e preciso (ex.: "Reentrância em withdraw", "Controle de acesso ausente em setFee").
-- **description**: Explique o comportamento ESPERADO versus o comportamento OBSERVADO (vulnerável) em 2 a 4 frases.
-- **recommendation**: Correção específica e acionável (ex.: "Aplicar o padrão checks-effects-interactions", "Adicionar o modificador onlyOwner").
-- **severity**: Um de "high" (perda direta de fundos ou tomada de controle do contrato), "medium" (risco indireto ou condicional), "low" (problema de boas práticas, sem risco financeiro imediato).
-- **codeSnippet**: O bloco de código vulnerável exatamente como aparece no código-fonte.
+## Invariantes e Propriedades
+Condições que devem ser verdadeiras para o protocolo operar corretamente, derivadas APENAS de \`require\`/\`assert\`/\`revert\` explícitos no código, NatSpec \`@dev\`, ou comentários que as declarem literalmente. Separe em dois grupos:
+- **Econômicas**: balanços, totais, proporções (ex.: \`totalDebt == Σ userDebt[i]\`, \`reservas >= totalSupply * exchangeRate\`)
+- **De controle**: acesso, sequência de operações, transições de estado permitidas
 
-Categorias de vulnerabilidades a verificar sistematicamente: reentrância (simples e entre funções), controle de acesso, overflow/underflow de inteiros, manipulação de oráculo, ataques de flash loan, front-running/MEV, replay de assinatura, colisões de armazenamento, proxies não inicializados, delegatecall inseguro, griefing de gas, negação de serviço, perda de precisão e violações de lógica/regras de negócio.
+## Trust Assumptions
+**SOMENTE o que estiver EXPLICITAMENTE declarado** em código-fonte (require, NatSpec, comentários inline) ou na documentação. **NÃO inferir. NÃO supor. NÃO extrapolar.** Se não há declaração explícita sobre confiança em um componente externo ou comportamento esperado, ele NÃO entra nesta seção — mesmo que pareça óbvio.
+Bullets curtos com referência à fonte (ex.: "owner pode pausar o contrato — \`onlyOwner\` em \`pause()\`").
 
-Se feedback do juiz de uma iteração anterior for fornecido, remova os falsos positivos confirmados da sua lista e refine ou expanda os achados restantes com base na crítica.`;
+## Regras de Negócio e Restrições de Segurança
+Em bullets: roles e modifiers relevantes (nomes exatos do código), limites numéricos (apenas valores literais presentes no código-fonte), taxas e destinatários, timelocks, pausabilidade, condições de upgrade, restrições de whitelist/blacklist. Inclua apenas regras com impacto direto em vetores de ataque.
 
-export const JUDGE_FINDINGS_PROMPT = `Você é um revisor rigoroso de segurança de smart contracts. Avalie cada vulnerabilidade candidata submetida pelo auditor e determine se é um verdadeiro positivo ou um falso positivo.
+**Formato obrigatório**: bullets e frases curtas. Dados concretos (nomes de funções, variáveis, valores numéricos) exatamente como aparecem no código. Sem prosa explicativa.`;
 
-Para cada achado, forneça TODOS os seguintes campos:
+export const FIND_VULNERABILITIES_PROMPT = `Você é um auditor especialista em segurança de smart contracts com profundo conhecimento em Solidity, execução EVM e design de protocolos. Assuma que todos os usuários são adversariais e estão ativamente tentando explorar o contrato.
 
-- **review**: Análise detalhada (3 a 6 frases) explicando por que a vulnerabilidade é ou não real. Referencie código específico, invariantes do protocolo, pré-condições e controles mitigadores.
-- **isFalsePositive**: true se o achado NÃO for explorável na prática; false se for uma vulnerabilidade real.
-- **confidence**: Número inteiro de 0 a 100 refletindo sua confiança no veredicto.
-- **exploitablePaths**: Array de strings. Se for verdadeiro positivo, forneça caminhos concretos confirmando a explorabilidade com valores reais. Cada rastreamento deve descrever os passos do atacante com entradas/valores realistas (ex.: "1. Atacante chama deposit(100 ETH) 2. Contrato do atacante no fallback chama withdraw() novamente antes da atualização do saldo 3. Atacante drena 100 ETH duas vezes"). Se for falso positivo, forneça o raciocínio que bloqueia o exploit.
+Sua tarefa é analisar o código-fonte fornecido linha a linha e identificar todas as vulnerabilidades de segurança, design, lógica e econômicas. Qualquer discrepância entre a implementação e o comportamento esperado, as suposições do protocolo ou o design econômico deve ser reportada como vulnerabilidade, mesmo que o contrato execute sem erros em runtime.
 
-Um achado é falso positivo somente se: o caminho de exploit for inacessível dados os controles de acesso ou pré-condições, já estiver totalmente mitigado pelo código, exigir condições impossíveis ou economicamente inviáveis, ou for explicitamente documentado como comportamento esperado nas premissas do protocolo.
+**Escopo obrigatório da análise**
 
-Você deve fornecer exatamente um objeto de revisão por achado, na mesma ordem em que os achados foram apresentados.`;
+Além das categorias técnicas listadas abaixo, sua análise deve cobrir:
+
+- **Invariantes de protocolo**: identifique invariantes implícitas e explícitas (ex.: depósitos devem igualar saques, ativos devem permanecer colateralizados, recompensas devem corresponder aos inputs) e verifique se podem ser quebradas.
+- **Fluxos de valor**: analise exaustivamente todas as transferências de valor (taxas, saldos, depósitos, saques, recompensas, deltas), verificando: quem provê os fundos, quem os recebe, e se os fundos são corretamente custodiados (escrowed) antes da transferência.
+- **Validação de ownership**: verifique se usuários podem interagir com tokens, NFTs ou permissões que não controlam.
+- **Observabilidade**: avalie se eventos, logs e chamadas de métodos representam corretamente as ações do protocolo. Emissão ausente, incorreta ou enganosa é uma vulnerabilidade.
+- **Implementação vs. intenção**: qualquer desvio entre o comportamento implementado e o design pretendido do protocolo deve ser reportado.
+
+## Categorias técnicas a verificar sistematicamente
+
+Reentrância (simples, cross-function, cross-contract, read-only), controle de acesso (funções privilegiadas desprotegidas, erros em herança de roles), overflow/underflow (Solidity <0.8 ou uso de \`unchecked\`), manipulação de oráculo (TWAP curto, preço spot, valor de reserves), ataques de flash loan (price impact, liquidações artificiais), front-running e MEV (sandwich, race condition em aprovações), replay de assinatura (nonce ausente, falta de chainId), colisões de storage (proxies, delegatecall), proxies não inicializados (initializer sem proteção), delegatecall inseguro (destino controlável pelo usuário), griefing de gas (loops ilimitados, arrays crescentes), negação de serviço (push payments, dependência de chamada externa), perda de precisão (divisão antes de multiplicação, truncamento acumulativo), lógica de negócio (violação de invariantes, casos de borda em math financeira, race conditions de estado).
+
+## Formato de saída
+
+Para cada vulnerabilidade encontrada, forneça OBRIGATORIAMENTE todos os campos abaixo. Cada entrada deve ser **atômica**: reporte exatamente um problema por entrada. Não agrupe múltiplos problemas em um único achado, mesmo que ocorram na mesma função ou linha. Não há limite para o número de vulnerabilidades reportadas.
+
+- **title**: Nome curto e preciso (ex.: "Reentrância em \`withdraw\`", "Controle de acesso ausente em \`setFee\`").
+- **description**: Descreva (a) o comportamento **esperado** pelo protocolo, (b) o comportamento **observado** no código vulnerável, e (c) o impacto concreto se explorado. Mínimo 3 frases, máximo 5.
+- **exploit_scenario**: Descreva um cenário concreto e passo a passo de como um atacante exploraria a vulnerabilidade.
+- **recommendation**: Correção específica e acionável com referência ao padrão ou mecanismo correto (ex.: "Aplicar checks-effects-interactions: mover \`balances[msg.sender] -= amount\` para antes da chamada externa").
+- **severity**: Exatamente um de: \`"high"\` (perda direta de fundos ou tomada de controle do contrato), \`"medium"\` (risco indireto ou condicional), \`"low"\` (problema de boas práticas, sem risco financeiro imediato).
+- **location**: Função e/ou número de linha onde o problema ocorre.
+- **codeSnippet**: O trecho exato e completo do código vulnerável, copiado literalmente do código-fonte. **Proibido** usar reticências (\`...\`), omissões, pseudocódigo ou paráfrases. Inclua as linhas exatas conforme aparecem no arquivo, com indentação original preservada. Se o snippet for maior que 40 linhas, inclua o intervalo completo sem cortes.
+
+## Regra de completude
+
+Reporte vulnerabilidades mesmo que não sejam imediatamente exploráveis. Vulnerabilidades podem ser de segurança, inconsistências de design, desalinhamentos econômicos ou falhas de observabilidade. Se nenhuma vulnerabilidade for encontrada, retorne um array vazio.`;
+
+export const REFINE_VULNERABILITIES_PROMPT = `Você é um auditor sênior de segurança de smart contracts refinando seus próprios achados com base no feedback de um revisor especialista independente.
+
+Na iteração anterior, você analisou um contrato Solidity e gerou uma lista de vulnerabilidades candidatas. Um revisor especialista avaliou cada achado e forneceu: veredicto (verdadeiro ou falso positivo), análise técnica detalhada, nível de confiança e caminhos de exploit ou razões de bloqueio.
+
+**Sua tarefa**: produzir uma lista final e refinada de vulnerabilidades incorporando o feedback do revisor.
+
+## Regras de refinamento
+
+1. **Falso positivo com confiança ≥ 80%**: remova o achado sem exceção.
+2. **Falso positivo com confiança < 80%**: reavalie com base na análise do revisor. Mantenha apenas se encontrar evidência nova ou argumento técnico que o revisor não considerou — e reflita isso na descrição.
+3. **Verdadeiro positivo**: mantenha o achado. Incorpore melhorias sugeridas pelo revisor (descrição mais precisa, snippet mais completo, recomendação mais específica, caminhos de exploit detalhados).
+4. **Novos achados**: se o revisor apontou superfícies de ataque não cobertas em seus achados originais, investigue o código-fonte e adicione novos achados para elas.
+5. Não adicione achados que não sejam suportados pelo código-fonte ou pelo feedback do revisor.
+
+## Formato de saída
+
+Idêntico ao da análise inicial. Para cada vulnerabilidade:
+- **title**: nome curto e preciso
+- **description**: (a) comportamento esperado, (b) comportamento observado, (c) impacto concreto — mínimo 3 frases, máximo 5
+- **recommendation**: correção específica e acionável com referência ao padrão correto
+- **severity**: \`"high"\` / \`"medium"\` / \`"low"\`
+- **codeSnippet**: trecho exato e completo copiado literalmente do código-fonte, sem omissões, reticências ou pseudocódigo
+
+Se nenhuma vulnerabilidade restar após o refinamento, retorne um array vazio.`;
+
+export const JUDGE_FINDINGS_PROMPT = `Você é um revisor rigoroso de segurança de smart contracts com profundo conhecimento em Solidity, execução EVM e design de protocolos. Avalie cada vulnerabilidade candidata submetida pelo auditor e determine se é um verdadeiro positivo ou um falso positivo.
+
+Para cada achado, forneça OBRIGATORIAMENTE todos os campos abaixo:
+
+- **review**: Análise técnica detalhada (3 a 6 frases) explicando o veredicto. Referencie: (a) o código específico envolvido, (b) invariantes ou premissas do protocolo que confirmam ou bloqueiam o exploit, (c) pré-condições necessárias para exploração, (d) controles mitigadores existentes que o auditor pode ter ignorado. Seja preciso — cite nomes de funções, variáveis e valores.
+- **isFalsePositive**: \`true\` se o achado NÃO for explorável na prática; \`false\` se for uma vulnerabilidade real.
+- **confidence**: Inteiro de 0 a 100 refletindo sua certeza no veredicto. Use < 60 apenas quando existir ambiguidade genuína no código.
+- **exploitablePaths**: Retorne uma array de strings.
+  - Se verdadeiro positivo (\`isFalsePositive: false\`): forneça 1 a 3 caminhos concretos de exploit, cada um com passos numerados, entradas realistas e estado do contrato antes/depois. Ex.: ["1. Atacante chama flashLoan(500k USDC). 2. No callback, chama deposit() inflando reserves. 3. Chama withdraw() com preço manipulado. 4. Lucra 50k USDC. Estado: reserves inflado temporariamente, totalShares inalterado."].
+  - Se falso positivo (\`isFalsePositive: true\`): forneça o raciocínio exato que bloqueia cada caminho de exploit tentado pelo auditor.
+
+## Critérios para falso positivo (aplique com rigor — não seja permissivo)
+
+1. O caminho de exploit é bloqueado por controle de acesso verificável no código.
+2. A vulnerabilidade já é totalmente mitigada por outro mecanismo no código (ex.: nonReentrant, onlyOwner, require com validação suficiente).
+3. A condição necessária para o exploit é impossível ou economicamente inviável dado o modelo do protocolo (ex.: requer ser o próprio contrato, ou lucro < custo de gas em qualquer cenário realista).
+4. O comportamento é explicitamente documentado como intencional nas premissas de design do protocolo.
+
+## Critérios para verdadeiro positivo
+- Existe pelo menos um caminho de exploit concreto e realista que viola uma invariante ou permite extração de valor não autorizada.
+- Não exige condições impossíveis nem assume acesso privilegiado não disponível ao atacante.
+- Inclui qualquer discrepância entre a implementação e a intenção, premissas ou objetivos documentados — mesmo que o contrato opere sem erros em runtime. Isso abrange problemas de segurança, inconsistências de design, desalinhamentos econômicos e falhas de observabilidade, independentemente de exploitabilidade direta.`;

src/agents/auditor/state.ts

@@ -1,6 +1,12 @@
 import { StateSchema } from "@langchain/langgraph";
 import { z } from "zod";
 
+export const FileRankingSchema = z.object({
+  filePath: z.string(),
+  importance: z.number().int().min(1).max(5),
+  reasoning: z.string(),
+});
+
 export const CandidateFindingSchema = z.object({
   title: z.string(),
   description: z.string(),
@@ -34,6 +40,7 @@ export const AuditorState = new StateSchema({
   scope: z.array(z.string()).default([]),
   docs: z.array(z.string()).default([]),
   fileTree: z.string().default(""),
+  fileRankings: z.array(FileRankingSchema).default([]),
   repoContext: z.string().default(""),
   candidateFindings: z.array(LocatedFindingSchema).default([]),
   judgeReviews: z.array(JudgeReviewSchema).default([]),

src/agents/auditor/tools/{repo-tree-tool.ts → repo-tree/tool.ts}

@@ -4,7 +4,7 @@ import path from "node:path";
 import { tool } from "langchain";
 import { z } from "zod";
 
-import { DOC_BASENAMES, DOC_EXTS, MAX_DEPTH, SKIP_DIRS, SOL_EXT, SOL_TEST_SUFFIXES } from "../config.ts";
+import { DOC_BASENAMES, DOC_EXTS, MAX_DEPTH, SKIP_DIRS, SOL_EXT, SOL_TEST_SUFFIXES } from "../../config.ts";
 
 const CONFIG_FILES = new Set([
   "foundry.toml",
@@ -90,14 +90,11 @@ export const buildRepoTree = (repoPath: string): string => {
   return `${repoName}/\n${renderTree(nodes, "")}`;
 };
 
-export const repoTreeTool = tool(
-  async ({ repoPath }) => buildRepoTree(repoPath),
-  {
-    name: "repo_tree",
-    description:
-      "Walk a repository and return a file-system tree of relevant files tagged by kind: [sol] for auditable Solidity contracts, [test] for Solidity test files, [doc] for documentation, and [config] for project config files. Use this during Define Scope to understand repository layout before selecting which files to audit.",
-    schema: z.object({
-      repoPath: z.string().describe("Absolute path to the repository root."),
-    }),
-  },
-);
+export const repoTreeTool = tool(async ({ repoPath }) => buildRepoTree(repoPath), {
+  name: "repo_tree",
+  description:
+    "Walk a repository and return a file-system tree of relevant files tagged by kind: [sol] for auditable Solidity contracts, [test] for Solidity test files, [doc] for documentation, and [config] for project config files. Use this during Define Scope to understand repository layout before selecting which files to audit.",
+  schema: z.object({
+    repoPath: z.string().describe("Absolute path to the repository root."),
+  }),
+});

src/agents/auditor/tools/solidity-analyzer-tool.ts

@@ -1,567 +0,0 @@
-import { parse, visit } from "@solidity-parser/parser";
-import { tool } from "langchain";
-import { z } from "zod";
-
-const ASSIGNMENT_OPS = new Set(["=", "+=", "-=", "*=", "/=", "%=", "|=", "&=", "^=", "<<=", ">>=", "**="]);
-const BUILTIN_NAMESPACES = new Set(["abi", "block", "msg", "tx", "bytes", "string", "type"]);
-
-interface StateVar {
-  name: string;
-  type: string;
-  visibility: string;
-  constant: boolean;
-  immutable: boolean;
-}
-
-interface EventDef {
-  name: string;
-  params: string[];
-  anonymous: boolean;
-}
-
-interface ModifierDef {
-  name: string;
-  params: string[];
-}
-
-interface FunctionDef {
-  name: string;
-  isConstructor: boolean;
-  isReceive: boolean;
-  isFallback: boolean;
-  visibility: string;
-  mutability: string;
-  params: string[];
-  returns: string[];
-  modifiers: string[];
-  internalCalls: string[];
-  externalCalls: string[];
-  stateReads: string[];
-  stateWrites: string[];
-}
-
-interface ContractAnalysis {
-  name: string;
-  kind: string;
-  baseContracts: string[];
-  usingFor: string[];
-  stateVars: StateVar[];
-  events: EventDef[];
-  modifiers: ModifierDef[];
-  functions: FunctionDef[];
-}
-
-const typeToString = (node: any): string => {
-  if (!node) return "unknown";
-
-  switch (node.type) {
-    case "ElementaryTypeName":
-      return node.name as string;
-    case "UserDefinedTypeName":
-      return (node.namePath ?? node.name) as string;
-    case "ArrayTypeName":
-      return `${typeToString(node.baseTypeName)}[${node.length ?? ""}]`;
-    case "Mapping":
-      return `mapping(${typeToString(node.keyType)} => ${typeToString(node.valueType)})`;
-    case "FunctionTypeName":
-      return "function";
-    default:
-      return "unknown";
-  }
-};
-
-const paramToString = (p: any) => {
-  if (!p) return "?";
-  const type = typeToString(p.typeName);
-  return p.name ? `${type} ${p.name}` : type;
-};
-
-const collectLHSRoots = (node: any, targets: Set<string>) => {
-  if (!node) return;
-  switch (node.type) {
-    case "Identifier":
-      targets.add(node.name as string);
-      break;
-    case "MemberAccess":
-      collectLHSRoots(node.expression, targets);
-      break;
-    case "IndexAccess":
-      collectLHSRoots(node.base, targets);
-      break;
-    case "TupleExpression":
-      for (const c of node.components ?? []) collectLHSRoots(c, targets);
-      break;
-  }
-};
-
-const analyzeFunction = (funcNode: any, stateVarNames: Set<string>) => {
-  const internalCalls = new Set<string>();
-  const externalCalls = new Set<string>();
-  const writeTargets = new Set<string>();
-  const allStateAccesses = new Set<string>();
-  const localVars = new Set<string>();
-
-  if (!funcNode.body) {
-    return { internalCalls: [], externalCalls: [], stateReads: [], stateWrites: [] };
-  }
-
-  // Collect function params and return params as locals so they don't shadow state vars
-  for (const p of funcNode.parameters ?? []) {
-    if (p?.name) localVars.add(p.name as string);
-  }
-  for (const p of funcNode.returnParameters ?? []) {
-    if (p?.name) localVars.add(p.name as string);
-  }
-
-  // Collect local variable declarations
-  visit(funcNode.body, {
-    VariableDeclarationStatement: (node: any) => {
-      for (const v of node.variables ?? []) {
-        if (v?.name) localVars.add(v.name as string);
-      }
-    },
-  });
-
-  const effectiveStateVars = new Set([...stateVarNames].filter((v) => !localVars.has(v)));
-
-  // Collect write targets from assignment LHS, unary mutations, and delete
-  visit(funcNode.body, {
-    ExpressionStatement: (node: any) => {
-      const expr = node.expression;
-      if (expr?.type === "BinaryOperation" && ASSIGNMENT_OPS.has(expr.operator as string)) {
-        collectLHSRoots(expr.left, writeTargets);
-      }
-      // Handle ++, --, and delete — all work on any lvalue (arr[i]++, delete s.field, etc.)
-      if (
-        expr?.type === "UnaryOperation" &&
-        (expr.operator === "++" || expr.operator === "--" || expr.operator === "delete")
-      ) {
-        collectLHSRoots(expr.subExpression, writeTargets);
-      }
-    },
-  });
-
-  // Collect calls and state-var identifier accesses
-  visit(funcNode.body, {
-    FunctionCall: (node: any) => {
-      const expr = node.expression;
-      if (expr?.type === "Identifier") {
-        internalCalls.add(expr.name as string);
-      } else if (expr?.type === "MemberAccess") {
-        const base = expr.expression;
-        if (base?.type === "Identifier" && (base.name === "this" || base.name === "super")) {
-          internalCalls.add(expr.memberName as string);
-        } else if (base?.type === "Identifier" && BUILTIN_NAMESPACES.has(base.name as string)) {
-          // abi.encode, block.xxx, msg.xxx, etc. — not external calls
-        } else {
-          const baseStr = base?.type === "Identifier" ? (base.name as string) : "<expr>";
-          externalCalls.add(`${baseStr}.${expr.memberName as string}`);
-        }
-      }
-    },
-    Identifier: (node: any) => {
-      if (effectiveStateVars.has(node.name as string)) {
-        allStateAccesses.add(node.name as string);
-      }
-    },
-  });
-
-  const stateWrites = [...allStateAccesses].filter((v) => writeTargets.has(v));
-  // A var can be in both — e.g. x = x + 1 is both a read and a write.
-  const stateReads = [...allStateAccesses];
-
-  return {
-    internalCalls: [...internalCalls],
-    externalCalls: [...externalCalls],
-    stateReads,
-    stateWrites,
-  };
-};
-
-const hasCycle = (start: string, current: string, callMap: Map<string, string[]>, visited: Set<string>) => {
-  for (const callee of callMap.get(current) ?? []) {
-    if (callee === start) return true;
-    if (!visited.has(callee)) {
-      visited.add(callee);
-      if (hasCycle(start, callee, callMap, visited)) return true;
-    }
-  }
-
-  return false;
-};
-
-const fnLabel = (fn: FunctionDef) => {
-  if (fn.isConstructor) return "constructor";
-  if (fn.isReceive) return "receive";
-  if (fn.isFallback) return "fallback";
-  return fn.name;
-};
-
-const generateShortMarkdown = (imports: string[], contracts: ContractAnalysis[]) => {
-  const lines: string[] = [];
-  lines.push("# Solidity Analysis\n");
-
-  if (imports.length > 0) {
-    lines.push(`**Imports:** ${imports.map((i) => `\`${i}\``).join(", ")}\n`);
-  }
-
-  for (const contract of contracts) {
-    const inheritance =
-      contract.baseContracts.length > 0 ? ` : ${contract.baseContracts.map((b) => `\`${b}\``).join(", ")}` : "";
-    lines.push(`---\n\n## \`${contract.name}\` (${contract.kind})${inheritance}\n`);
-
-    // State variables — one line, name:type
-    if (contract.stateVars.length > 0) {
-      const vars = contract.stateVars.map((v) => {
-        const flags = [v.constant && "constant", v.immutable && "immutable"].filter(Boolean);
-        const suffix = flags.length > 0 ? `, ${flags.join(", ")}` : "";
-        return `\`${v.name}: ${v.type}\` (${v.visibility}${suffix})`;
-      });
-      lines.push(`**State:** ${vars.join(", ")}\n`);
-    }
-
-    // Modifiers — names only
-    if (contract.modifiers.length > 0) {
-      const mods = contract.modifiers.map(
-        (m) => `\`${m.name}${m.params.length > 0 ? `(${m.params.join(", ")})` : ""}\``,
-      );
-      lines.push(`**Modifiers:** ${mods.join(", ")}\n`);
-    }
-
-    // Events — name + params, one line each
-    if (contract.events.length > 0) {
-      const evts = contract.events.map((e) => `\`${e.name}(${e.params.join(", ")})\``);
-      lines.push(`**Events:** ${evts.join(", ")}\n`);
-    }
-
-    // Function list — compact, one line per function
-    if (contract.functions.length > 0) {
-      lines.push("**Functions:**");
-      for (const fn of contract.functions) {
-        const label = fnLabel(fn);
-        const params = fn.params.join(", ");
-        const ret = fn.returns.length > 0 ? ` → ${fn.returns.join(", ")}` : "";
-        const mods = fn.modifiers.length > 0 ? ` [${fn.modifiers.join(", ")}]` : "";
-        lines.push(`- \`${label}(${params})${ret}\` — ${fn.visibility} ${fn.mutability}${mods}`);
-      }
-      lines.push("");
-    }
-
-    // External calls — only functions that make them
-    const externalFuncs = contract.functions.filter((f) => f.externalCalls.length > 0);
-    if (externalFuncs.length > 0) {
-      lines.push("**External Calls:**");
-      for (const fn of externalFuncs) {
-        lines.push(`- \`${fnLabel(fn)}\`: ${fn.externalCalls.map((c) => `\`${c}\``).join(", ")}`);
-      }
-      lines.push("");
-    }
-  }
-
-  return lines.join("\n");
-};
-
-const generateMarkdown = (imports: string[], contracts: ContractAnalysis[]) => {
-  const lines: string[] = [];
-  lines.push("# Solidity Contract Analysis\n");
-
-  // Imports
-  lines.push("## Imports\n");
-  if (imports.length === 0) {
-    lines.push("_No imports._\n");
-  } else {
-    for (const imp of imports) lines.push(`- \`${imp}\``);
-    lines.push("");
-  }
-
-  for (const contract of contracts) {
-    const kindLabel = contract.kind.charAt(0).toUpperCase() + contract.kind.slice(1);
-    lines.push(`---\n\n## ${kindLabel}: \`${contract.name}\`\n`);
-
-    // Inheritance
-    lines.push("### Inheritance\n");
-    if (contract.baseContracts.length === 0) {
-      lines.push("_None._\n");
-    } else {
-      for (const base of contract.baseContracts) lines.push(`- \`${base}\``);
-      lines.push("");
-    }
-
-    // Using For
-    if (contract.usingFor.length > 0) {
-      lines.push("### Using For\n");
-      for (const u of contract.usingFor) lines.push(`- ${u}`);
-      lines.push("");
-    }
-
-    // Storage layout
-    lines.push("### Storage Layout (State Variables)\n");
-    if (contract.stateVars.length === 0) {
-      lines.push("_No state variables._\n");
-    } else {
-      lines.push("| Slot | Name | Type | Visibility | Flags |");
-      lines.push("|------|------|------|------------|-------|");
-      contract.stateVars.forEach((v, i) => {
-        const flags = [v.constant && "constant", v.immutable && "immutable"].filter(Boolean).join(", ");
-        lines.push(`| ${i} | \`${v.name}\` | \`${v.type}\` | ${v.visibility} | ${flags} |`);
-      });
-      lines.push("");
-    }
-
-    // Events
-    lines.push("### Events\n");
-    if (contract.events.length === 0) {
-      lines.push("_No events._\n");
-    } else {
-      for (const evt of contract.events) {
-        const params = evt.params.join(", ");
-        lines.push(`- **\`${evt.name}\`**\`(${params})\`${evt.anonymous ? " _(anonymous)_" : ""}`);
-      }
-      lines.push("");
-    }
-
-    // Modifiers
-    lines.push("### Modifiers\n");
-    if (contract.modifiers.length === 0) {
-      lines.push("_No modifiers._\n");
-    } else {
-      for (const mod of contract.modifiers) {
-        lines.push(`- **\`${mod.name}\`**\`(${mod.params.join(", ")})\``);
-      }
-      lines.push("");
-    }
-
-    // Function list
-    lines.push("### Function List\n");
-    if (contract.functions.length === 0) {
-      lines.push("_No functions._\n");
-    } else {
-      lines.push("| Name | Visibility | Mutability | Parameters | Returns | Modifiers |");
-      lines.push("|------|------------|------------|------------|---------|-----------|");
-      for (const fn of contract.functions) {
-        lines.push(
-          `| \`${fnLabel(fn)}\` | ${fn.visibility} | ${fn.mutability} | \`${fn.params.join(", ")}\` | \`${fn.returns.join(", ")}\` | ${fn.modifiers.join(", ")} |`,
-        );
-      }
-      lines.push("");
-    }
-
-    // Call graph
-    lines.push("### Call Graph\n");
-    const hasCalls = contract.functions.some((f) => f.internalCalls.length > 0 || f.externalCalls.length > 0);
-    if (!hasCalls) {
-      lines.push("_No function calls detected._\n");
-    } else {
-      for (const fn of contract.functions) {
-        if (fn.internalCalls.length === 0 && fn.externalCalls.length === 0) continue;
-        lines.push(`**\`${fnLabel(fn)}\`**`);
-        for (const call of fn.internalCalls) lines.push(`  - → \`${call}\` _(internal)_`);
-        for (const call of fn.externalCalls) lines.push(`  - → \`${call}\` _(external)_`);
-      }
-      lines.push("");
-    }
-
-    // External calls
-    lines.push("### External Calls\n");
-    const externalFuncs = contract.functions.filter((f) => f.externalCalls.length > 0);
-    if (externalFuncs.length === 0) {
-      lines.push("_No external calls detected._\n");
-    } else {
-      for (const fn of externalFuncs) {
-        lines.push(`**\`${fnLabel(fn)}\`**`);
-        for (const call of fn.externalCalls) lines.push(`  - \`${call}\``);
-      }
-      lines.push("");
-    }
-
-    // Internal recursion
-    lines.push("### Internal Recursion\n");
-    const callMap = new Map(contract.functions.map((f) => [fnLabel(f), f.internalCalls]));
-    const recursiveFns = contract.functions.filter((fn) => hasCycle(fnLabel(fn), fnLabel(fn), callMap, new Set()));
-    if (recursiveFns.length === 0) {
-      lines.push("_No recursive functions detected._\n");
-    } else {
-      for (const fn of recursiveFns) lines.push(`- **\`${fnLabel(fn)}\`** is recursive`);
-      lines.push("");
-    }
-
-    // State variable touchpoints
-    lines.push("### State Variable Touchpoints\n");
-    const touchedFns = contract.functions.filter((f) => f.stateReads.length > 0 || f.stateWrites.length > 0);
-    if (touchedFns.length === 0) {
-      lines.push("_No state variable accesses detected._\n");
-    } else {
-      lines.push("| Function | Reads | Writes |");
-      lines.push("|----------|-------|--------|");
-      for (const fn of touchedFns) {
-        const reads = fn.stateReads.map((r) => `\`${r}\``).join(", ");
-        const writes = fn.stateWrites.map((w) => `\`${w}\``).join(", ");
-        lines.push(`| \`${fnLabel(fn)}\` | ${reads} | ${writes} |`);
-      }
-      lines.push("");
-    }
-  }
-
-  // External dependencies summary
-  lines.push("---\n\n## External Dependencies\n");
-
-  lines.push("### Import Paths\n");
-  if (imports.length === 0) {
-    lines.push("_No imports._\n");
-  } else {
-    for (const imp of imports) lines.push(`- \`${imp}\``);
-    lines.push("");
-  }
-
-  const externalTargets = new Set<string>();
-  for (const contract of contracts) {
-    for (const fn of contract.functions) {
-      for (const call of fn.externalCalls) {
-        const target = call.split(".")[0];
-        if (target && target !== "<expr>") externalTargets.add(target);
-      }
-    }
-  }
-
-  lines.push("### External Contract Interactions\n");
-  if (externalTargets.size === 0) {
-    lines.push("_No external contract interactions detected._\n");
-  } else {
-    for (const dep of externalTargets) lines.push(`- \`${dep}\``);
-    lines.push("");
-  }
-
-  return lines.join("\n");
-};
-
-export const analyzeSolidityFile = async (soliditySource: string, mode: "full" | "short") => {
-  let ast: any;
-
-  try {
-    ast = parse(soliditySource, { tolerant: true, loc: true, range: true });
-  } catch (e: any) {
-    return `# Parse Error\n\nFailed to parse Solidity source: ${e.message as string}`;
-  }
-
-  const imports: string[] = [];
-  const contracts: ContractAnalysis[] = [];
-
-  for (const node of ast.children ?? []) {
-    if (node.type === "ImportDirective") {
-      imports.push(node.path as string);
-    }
-  }
-
-  for (const node of ast.children ?? []) {
-    if (node.type !== "ContractDefinition") continue;
-
-    const contract: ContractAnalysis = {
-      name: node.name as string,
-      kind: (node.kind as string) ?? "contract",
-      baseContracts: (node.baseContracts ?? []).map(
-        (bc: any) => (bc.baseName?.namePath ?? bc.baseName?.name ?? "?") as string,
-      ),
-      usingFor: [],
-      stateVars: [],
-      events: [],
-      modifiers: [],
-      functions: [],
-    };
-
-    const stateVarNames = new Set<string>();
-
-    for (const member of node.subNodes ?? []) {
-      switch (member.type) {
-        case "StateVariableDeclaration":
-          for (const v of member.variables ?? []) {
-            stateVarNames.add(v.name as string);
-            contract.stateVars.push({
-              name: v.name as string,
-              type: typeToString(v.typeName),
-              visibility: (v.visibility as string) ?? "internal",
-              constant: (v.isDeclaredConst as boolean) ?? false,
-              immutable: (v.isImmutable as boolean) ?? false,
-            });
-          }
-          break;
-
-        case "EventDefinition": {
-          const params = (member.parameters ?? []).map((p: any) => {
-            const indexed = p.isIndexed ? "indexed " : "";
-            const name = p.name ? ` ${p.name as string}` : "";
-            return `${indexed}${typeToString(p.typeName)}${name}`;
-          });
-          contract.events.push({
-            name: member.name as string,
-            params,
-            anonymous: (member.isAnonymous as boolean) ?? false,
-          });
-          break;
-        }
-
-        case "ModifierDefinition":
-          contract.modifiers.push({
-            name: member.name as string,
-            params: (member.parameters ?? []).map(paramToString),
-          });
-          break;
-
-        case "FunctionDefinition": {
-          const { internalCalls, externalCalls, stateReads, stateWrites } = analyzeFunction(member, stateVarNames);
-          contract.functions.push({
-            name: (member.name as string) ?? "",
-            isConstructor: (member.isConstructor as boolean) ?? false,
-            isReceive: (member.isReceiveEther as boolean) ?? false,
-            isFallback: (member.isFallback as boolean) ?? false,
-            visibility: (member.visibility as string) ?? "internal",
-            mutability: (member.stateMutability as string) ?? "nonpayable",
-            params: (member.parameters ?? []).map(paramToString),
-            returns: (member.returnParameters ?? []).map(paramToString),
-            modifiers: (member.modifiers ?? []).map((m: any) => m.name as string),
-            internalCalls,
-            externalCalls,
-            stateReads,
-            stateWrites,
-          });
-          break;
-        }
-
-        case "UsingForDeclaration": {
-          const forType = member.typeName ? typeToString(member.typeName) : "*";
-          if (member.libraryName) {
-            contract.usingFor.push(`\`${member.libraryName as string}\` for \`${forType}\``);
-          } else {
-            // New-style: using {fn1, fn2, ...} for T
-            const fns = (member.functions ?? [])
-              .map((f: any) => (f.typeName?.namePath ?? f.typeName?.name ?? f.path ?? "?") as string)
-              .join(", ");
-            contract.usingFor.push(`{${fns}} for \`${forType}\``);
-          }
-          break;
-        }
-      }
-    }
-
-    contracts.push(contract);
-  }
-
-  return mode === "short" ? generateShortMarkdown(imports, contracts) : generateMarkdown(imports, contracts);
-};
-
-export const solidityAnalyzerTool = tool(
-  async ({ solidityFile, mode }) => {
-    return analyzeSolidityFile(solidityFile, mode);
-  },
-  {
-    name: "solidity_analyzer",
-    description:
-      "Parse a Solidity source file and generate a markdown report. Use mode='short' for a compact token-efficient summary (imports, state, modifiers, events, function signatures, external calls). Use mode='full' for the complete report including storage layout table, call graph, recursion detection, state variable touchpoints, and external dependencies.",
-    schema: z.object({
-      solidityFile: z.string().describe("The full Solidity source code to analyze."),
-      mode: z
-        .enum(["full", "short"])
-        .default("full")
-        .describe("Report verbosity. 'short' saves tokens; 'full' provides the complete analysis."),
-    }),
-  },
-);

src/agents/auditor/tools/solidity-analyzer/tool.ts

@@ -0,0 +1,172 @@
+import { parse } from "@solidity-parser/parser";
+import { tool } from "langchain";
+import { z } from "zod";
+
+import {
+  analyzeFunction,
+  buildCommentBlocks,
+  type ContractAnalysis,
+  extractSolcVersion,
+  findCommentFor,
+  generateBriefMarkdown,
+  generateFullMarkdown,
+  paramToString,
+  type RenderOptions,
+  typeToString,
+} from "./utils.ts";
+
+export const analyzeSolidityFile = async (
+  soliditySource: string,
+  mode: "full" | "short",
+  filePath?: string,
+  importance?: number,
+): Promise<string> => {
+  let ast: any;
+  try {
+    ast = parse(soliditySource, { tolerant: true, loc: true, range: true });
+  } catch (e: any) {
+    return `# Parse Error\n\nFailed to parse Solidity source: ${e.message as string}`;
+  }
+
+  const comments = buildCommentBlocks(soliditySource);
+  const imports: string[] = [];
+  const contracts: ContractAnalysis[] = [];
+
+  for (const node of ast.children ?? []) {
+    if (node.type === "ImportDirective") imports.push(node.path as string);
+  }
+
+  for (const node of ast.children ?? []) {
+    if (node.type !== "ContractDefinition") continue;
+
+    const contractComment = node.loc ? findCommentFor(node.loc.start.line, comments) : undefined;
+
+    const contract: ContractAnalysis = {
+      name: node.name as string,
+      kind: (node.kind as string) ?? "contract",
+      baseContracts: (node.baseContracts ?? []).map(
+        (bc: any) => (bc.baseName?.namePath ?? bc.baseName?.name ?? "?") as string,
+      ),
+      usingFor: [],
+      stateVars: [],
+      events: [],
+      errors: [],
+      modifiers: [],
+      functions: [],
+      natspec: contractComment?.natspec,
+    };
+
+    const stateVarNames = new Set<string>();
+
+    for (const member of node.subNodes ?? []) {
+      const memberComment = member.loc ? findCommentFor(member.loc.start.line, comments) : undefined;
+
+      switch (member.type) {
+        case "StateVariableDeclaration":
+          for (const v of member.variables ?? []) {
+            stateVarNames.add(v.name as string);
+            contract.stateVars.push({
+              name: v.name as string,
+              type: typeToString(v.typeName),
+              visibility: (v.visibility as string) ?? "internal",
+              constant: (v.isDeclaredConst as boolean) ?? false,
+              immutable: (v.isImmutable as boolean) ?? false,
+              natspec: memberComment?.natspec,
+            });
+          }
+          break;
+
+        case "EventDefinition": {
+          const params = (member.parameters ?? []).map((p: any) => {
+            const indexed = p.isIndexed ? "indexed " : "";
+            const name = p.name ? ` ${p.name as string}` : "";
+            return `${indexed}${typeToString(p.typeName)}${name}`;
+          });
+          contract.events.push({
+            name: member.name as string,
+            params,
+            anonymous: (member.isAnonymous as boolean) ?? false,
+            natspec: memberComment?.natspec,
+          });
+          break;
+        }
+
+        case "CustomErrorDefinition":
+          contract.errors.push({
+            name: member.name as string,
+            params: (member.parameters ?? []).map((p: any) => paramToString(p)),
+            natspec: memberComment?.natspec,
+          });
+          break;
+
+        case "ModifierDefinition":
+          contract.modifiers.push({
+            name: member.name as string,
+            params: (member.parameters ?? []).map(paramToString),
+            natspec: memberComment?.natspec,
+          });
+          break;
+
+        case "FunctionDefinition": {
+          const { internalCalls, externalCalls, stateReads, stateWrites } = analyzeFunction(member, stateVarNames);
+          contract.functions.push({
+            name: (member.name as string) ?? "",
+            isConstructor: (member.isConstructor as boolean) ?? false,
+            isReceive: (member.isReceiveEther as boolean) ?? false,
+            isFallback: (member.isFallback as boolean) ?? false,
+            visibility: (member.visibility as string) ?? "internal",
+            mutability: (member.stateMutability as string) ?? "nonpayable",
+            params: (member.parameters ?? []).map(paramToString),
+            returns: (member.returnParameters ?? []).map(paramToString),
+            modifiers: (member.modifiers ?? []).map((m: any) => m.name as string),
+            internalCalls,
+            externalCalls,
+            stateReads,
+            stateWrites,
+            natspec: memberComment?.natspec,
+          });
+          break;
+        }
+
+        case "UsingForDeclaration": {
+          const forType = member.typeName ? typeToString(member.typeName) : "*";
+          if (member.libraryName) {
+            contract.usingFor.push(`\`${member.libraryName as string}\` for \`${forType}\``);
+          } else {
+            const fns = (member.functions ?? [])
+              .map((f: any) => (f.typeName?.namePath ?? f.typeName?.name ?? f.path ?? "?") as string)
+              .join(", ");
+            contract.usingFor.push(`{${fns}} for \`${forType}\``);
+          }
+          break;
+        }
+      }
+    }
+
+    contracts.push(contract);
+  }
+
+  const opts: RenderOptions = {
+    filePath,
+    importance,
+    lineCount: soliditySource.split("\n").length,
+    solcVersion: extractSolcVersion(soliditySource),
+  };
+
+  return mode === "short"
+    ? generateBriefMarkdown(imports, contracts, opts)
+    : generateFullMarkdown(imports, contracts, opts);
+};
+
+export const solidityAnalyzerTool = tool(async ({ solidityFile, mode }) => analyzeSolidityFile(solidityFile, mode), {
+  name: "solidity_analyzer",
+  description:
+    "Parse a Solidity source file and generate a markdown report. Use mode='short' for a compact summary (meta, external calls, function table). Use mode='full' for the complete report including storage, events, errors, per-function call graph, recursion detection, and state variable touchpoints.",
+  schema: z.object({
+    solidityFile: z.string().describe("The full Solidity source code to analyze."),
+    mode: z
+      .enum(["full", "short"])
+      .default("full")
+      .describe("Report verbosity. 'short' saves tokens; 'full' provides the complete analysis."),
+  }),
+});

src/agents/auditor/tools/solidity-analyzer/utils.ts

@@ -0,0 +1,520 @@
+import { visit } from "@solidity-parser/parser";
+
+const ASSIGNMENT_OPS = new Set(["=", "+=", "-=", "*=", "/=", "%=", "|=", "&=", "^=", "<<=", ">>=", "**="]);
+const BUILTIN_NAMESPACES = new Set(["abi", "block", "msg", "tx", "bytes", "string", "type"]);
+
+export interface NatSpec {
+  title?: string;
+  author?: string;
+  notice?: string;
+  dev?: string;
+  params: Record<string, string>;
+  returns: string[];
+  inheritdoc?: string;
+  custom: Record<string, string>;
+}
+
+export interface ParsedComment {
+  text: string;
+  startLine: number;
+  endLine: number;
+  isNatSpec: boolean;
+  natspec?: NatSpec;
+}
+
+export interface StateVar {
+  name: string;
+  type: string;
+  visibility: string;
+  constant: boolean;
+  immutable: boolean;
+  natspec?: NatSpec;
+}
+
+export interface EventDef {
+  name: string;
+  params: string[];
+  anonymous: boolean;
+  natspec?: NatSpec;
+}
+
+export interface ErrorDef {
+  name: string;
+  params: string[];
+  natspec?: NatSpec;
+}
+
+export interface ModifierDef {
+  name: string;
+  params: string[];
+  natspec?: NatSpec;
+}
+
+export interface FunctionDef {
+  name: string;
+  isConstructor: boolean;
+  isReceive: boolean;
+  isFallback: boolean;
+  visibility: string;
+  mutability: string;
+  params: string[];
+  returns: string[];
+  modifiers: string[];
+  internalCalls: string[];
+  externalCalls: string[];
+  stateReads: string[];
+  stateWrites: string[];
+  natspec?: NatSpec;
+}
+
+export interface ContractAnalysis {
+  name: string;
+  kind: string;
+  baseContracts: string[];
+  usingFor: string[];
+  stateVars: StateVar[];
+  events: EventDef[];
+  errors: ErrorDef[];
+  modifiers: ModifierDef[];
+  functions: FunctionDef[];
+  natspec?: NatSpec;
+}
+
+export interface RenderOptions {
+  filePath?: string;
+  importance?: number;
+  lineCount: number;
+  solcVersion: string;
+}
+
+export const extractSolcVersion = (source: string): string => {
+  const match = source.match(/pragma\s+solidity\s+([^;]+);/);
+  return match ? match[1].trim() : "—";
+};
+
+const parseNatSpecTags = (text: string): NatSpec => {
+  const result: NatSpec = { params: {}, returns: [], custom: {} };
+
+  const firstTag = text.search(/@(?:title|author|notice|dev|param|return|inheritdoc|custom:)/);
+  if (firstTag > 0) {
+    const implicit = text.slice(0, firstTag).trim();
+    if (implicit) result.notice = implicit.replace(/\n\s*/g, " ");
+  } else if (firstTag === -1 && text.trim()) {
+    result.notice = text.trim().replace(/\n\s*/g, " ");
+  }
+
+  const tagRe = /@(custom:\S+|\w+)([^@]*)/g;
+  let m: RegExpExecArray | null;
+  while ((m = tagRe.exec(text)) !== null) {
+    const tag = m[1];
+    const value = m[2].trim().replace(/\n\s*/g, " ");
+    if (tag === "title") result.title = value;
+    else if (tag === "author") result.author = value;
+    else if (tag === "notice") result.notice = value;
+    else if (tag === "dev") result.dev = value;
+    else if (tag === "inheritdoc") result.inheritdoc = value;
+    else if (tag === "param") {
+      const sp = value.indexOf(" ");
+      if (sp > 0) result.params[value.slice(0, sp)] = value.slice(sp + 1);
+      else if (value) result.params[value] = "";
+    } else if (tag === "return") result.returns.push(value);
+    else if (tag.startsWith("custom:")) result.custom[tag.slice(7)] = value;
+  }
+
+  return result;
+};
+
+export const buildCommentBlocks = (source: string): ParsedComment[] => {
+  const blocks: ParsedComment[] = [];
+  const lines = source.split("\n");
+  let i = 0;
+
+  while (i < lines.length) {
+    const raw = lines[i];
+    const trimmed = raw.trimStart();
+
+    if (trimmed.startsWith("///")) {
+      const startLine = i + 1;
+      const texts: string[] = [];
+      while (i < lines.length && lines[i].trimStart().startsWith("///")) {
+        texts.push(lines[i].trimStart().slice(3).replace(/^ /, ""));
+        i++;
+      }
+      const text = texts.join("\n");
+      blocks.push({ text, startLine, endLine: i, isNatSpec: true, natspec: parseNatSpecTags(text) });
+      continue;
+    }
+
+    const mlStart = raw.indexOf("/*");
+    if (mlStart !== -1) {
+      const isNatSpec = raw[mlStart + 2] === "*" && raw[mlStart + 3] !== "/";
+      const startLine = i + 1;
+      const closeOnSame = raw.indexOf("*/", mlStart + 2);
+
+      if (closeOnSame !== -1) {
+        const inner = raw.slice(mlStart + (isNatSpec ? 3 : 2), closeOnSame).trim();
+        blocks.push({
+          text: inner,
+          startLine,
+          endLine: startLine,
+          isNatSpec,
+          natspec: isNatSpec ? parseNatSpecTags(inner) : undefined,
+        });
+        i++;
+        continue;
+      }
+
+      const rawLines: string[] = [raw.slice(mlStart + (isNatSpec ? 3 : 2))];
+      i++;
+      while (i < lines.length) {
+        const closeIdx = lines[i].indexOf("*/");
+        if (closeIdx !== -1) {
+          rawLines.push(lines[i].slice(0, closeIdx));
+          i++;
+          break;
+        }
+        rawLines.push(lines[i]);
+        i++;
+      }
+      const text = rawLines
+        .map((l) => l.replace(/^\s*\*\s?/, ""))
+        .join("\n")
+        .trim();
+      blocks.push({ text, startLine, endLine: i, isNatSpec, natspec: isNatSpec ? parseNatSpecTags(text) : undefined });
+      continue;
+    }
+
+    if (trimmed.startsWith("//")) {
+      blocks.push({ text: trimmed.slice(2).trim(), startLine: i + 1, endLine: i + 1, isNatSpec: false });
+    }
+
+    i++;
+  }
+
+  return blocks;
+};
+
+export const findCommentFor = (line: number, comments: ParsedComment[]): ParsedComment | undefined =>
+  comments.find((c) => c.endLine === line - 1) ?? comments.find((c) => c.startLine === line && !c.isNatSpec);
+
+export const typeToString = (node: any): string => {
+  if (!node) return "unknown";
+  switch (node.type) {
+    case "ElementaryTypeName":
+      return node.name as string;
+    case "UserDefinedTypeName":
+      return (node.namePath ?? node.name) as string;
+    case "ArrayTypeName":
+      return `${typeToString(node.baseTypeName)}[${node.length ?? ""}]`;
+    case "Mapping":
+      return `mapping(${typeToString(node.keyType)} => ${typeToString(node.valueType)})`;
+    case "FunctionTypeName":
+      return "function";
+    default:
+      return "unknown";
+  }
+};
+
+export const paramToString = (p: any): string => {
+  if (!p) return "?";
+  const type = typeToString(p.typeName);
+  return p.name ? `${type} ${p.name}` : type;
+};
+
+const collectLHSRoots = (node: any, targets: Set<string>) => {
+  if (!node) return;
+  switch (node.type) {
+    case "Identifier":
+      targets.add(node.name as string);
+      break;
+    case "MemberAccess":
+      collectLHSRoots(node.expression, targets);
+      break;
+    case "IndexAccess":
+      collectLHSRoots(node.base, targets);
+      break;
+    case "TupleExpression":
+      for (const c of node.components ?? []) collectLHSRoots(c, targets);
+      break;
+  }
+};
+
+export const analyzeFunction = (funcNode: any, stateVarNames: Set<string>) => {
+  const internalCalls = new Set<string>();
+  const externalCalls = new Set<string>();
+  const writeTargets = new Set<string>();
+  const allStateAccesses = new Set<string>();
+  const localVars = new Set<string>();
+
+  if (!funcNode.body) {
+    return { internalCalls: [], externalCalls: [], stateReads: [], stateWrites: [] };
+  }
+
+  for (const p of funcNode.parameters ?? []) {
+    if (p?.name) localVars.add(p.name as string);
+  }
+  for (const p of funcNode.returnParameters ?? []) {
+    if (p?.name) localVars.add(p.name as string);
+  }
+
+  visit(funcNode.body, {
+    VariableDeclarationStatement: (node: any) => {
+      for (const v of node.variables ?? []) {
+        if (v?.name) localVars.add(v.name as string);
+      }
+    },
+  });
+
+  const effectiveStateVars = new Set([...stateVarNames].filter((v) => !localVars.has(v)));
+
+  visit(funcNode.body, {
+    ExpressionStatement: (node: any) => {
+      const expr = node.expression;
+      if (expr?.type === "BinaryOperation" && ASSIGNMENT_OPS.has(expr.operator as string)) {
+        collectLHSRoots(expr.left, writeTargets);
+      }
+      if (
+        expr?.type === "UnaryOperation" &&
+        (expr.operator === "++" || expr.operator === "--" || expr.operator === "delete")
+      ) {
+        collectLHSRoots(expr.subExpression, writeTargets);
+      }
+    },
+  });
+
+  visit(funcNode.body, {
+    FunctionCall: (node: any) => {
+      const expr = node.expression;
+      if (expr?.type === "Identifier") {
+        internalCalls.add(expr.name as string);
+      } else if (expr?.type === "MemberAccess") {
+        const base = expr.expression;
+        if (base?.type === "Identifier" && (base.name === "this" || base.name === "super")) {
+          internalCalls.add(expr.memberName as string);
+        } else if (base?.type === "Identifier" && BUILTIN_NAMESPACES.has(base.name as string)) {
+          // builtin namespace — skip
+        } else {
+          const baseStr = base?.type === "Identifier" ? (base.name as string) : "<expr>";
+          externalCalls.add(`${baseStr}.${expr.memberName as string}`);
+        }
+      }
+    },
+    Identifier: (node: any) => {
+      if (effectiveStateVars.has(node.name as string)) {
+        allStateAccesses.add(node.name as string);
+      }
+    },
+  });
+
+  const stateWrites = [...allStateAccesses].filter((v) => writeTargets.has(v));
+
+  return {
+    internalCalls: [...internalCalls],
+    externalCalls: [...externalCalls],
+    stateReads: [...allStateAccesses],
+    stateWrites,
+  };
+};
+
+export const hasCycle = (
+  start: string,
+  current: string,
+  callMap: Map<string, string[]>,
+  visited: Set<string>,
+): boolean => {
+  for (const callee of callMap.get(current) ?? []) {
+    if (callee === start) return true;
+    if (!visited.has(callee)) {
+      visited.add(callee);
+      if (hasCycle(start, callee, callMap, visited)) return true;
+    }
+  }
+  return false;
+};
+
+export const fnLabel = (fn: FunctionDef): string => {
+  if (fn.isConstructor) return "constructor";
+  if (fn.isReceive) return "receive";
+  if (fn.isFallback) return "fallback";
+  return fn.name;
+};
+
+const renderNatSpec = (ns: NatSpec | undefined): string => {
+  if (!ns) return "—";
+  const parts: string[] = [];
+  if (ns.title) parts.push(`@title "${ns.title}"`);
+  if (ns.author) parts.push(`@author "${ns.author}"`);
+  if (ns.notice) parts.push(`@notice "${ns.notice}"`);
+  if (ns.dev) parts.push(`@dev "${ns.dev}"`);
+  for (const [k, v] of Object.entries(ns.params)) {
+    parts.push(v ? `@param ${k}: "${v}"` : `@param ${k}`);
+  }
+  for (const r of ns.returns) {
+    if (r) parts.push(`@return "${r}"`);
+  }
+  return parts.length > 0 ? parts.join(" · ") : "—";
+};
+
+const renderContractFull = (contract: ContractAnalysis, imports: string[], lines: string[]) => {
+  lines.push("## Meta");
+  const inherits = contract.baseContracts.length > 0 ? `[${contract.baseContracts.join(", ")}]` : "—";
+  lines.push(`- kind: ${contract.kind} · inherits: ${inherits}`);
+  if (contract.usingFor.length > 0) lines.push(`- uses: [${contract.usingFor.join(", ")}]`);
+  lines.push(`- imports: ${imports.length > 0 ? imports.map((i) => `\`${i}\``).join(", ") : "—"}`);
+  lines.push(`- docs: ${renderNatSpec(contract.natspec)}`);
+  lines.push("");
+
+  if (contract.stateVars.length > 0) {
+    lines.push("## Storage");
+    lines.push("| name | type | vis | flags | desc |");
+    lines.push("|------|------|-----|-------|------|");
+    for (const v of contract.stateVars) {
+      const flags = [v.constant && "constant", v.immutable && "immutable"].filter(Boolean).join(", ") || "—";
+      const desc = v.natspec?.notice ?? v.natspec?.dev ?? "—";
+      lines.push(`| \`${v.name}\` | \`${v.type}\` | ${v.visibility} | ${flags} | ${desc} |`);
+    }
+    lines.push("");
+  }
+
+  if (contract.events.length > 0) {
+    lines.push("## Events");
+    for (const e of contract.events) {
+      const notice = e.natspec?.notice ? ` — ${e.natspec.notice}` : "";
+      lines.push(`- \`${e.name}(${e.params.join(", ")})\`${e.anonymous ? " _(anon)_" : ""}${notice}`);
+    }
+    lines.push("");
+  }
+
+  if (contract.errors.length > 0) {
+    lines.push("## Errors");
+    for (const e of contract.errors) lines.push(`- \`${e.name}(${e.params.join(", ")})\``);
+    lines.push("");
+  }
+
+  if (contract.modifiers.length > 0) {
+    lines.push("## Modifiers");
+    for (const m of contract.modifiers) {
+      const notice = m.natspec?.notice ? ` — ${m.natspec.notice}` : "";
+      lines.push(`- \`${m.name}(${m.params.join(", ")})\`${notice}`);
+    }
+    lines.push("");
+  }
+
+  const allExternalCalls = new Set(contract.functions.flatMap((f) => f.externalCalls));
+  if (allExternalCalls.size > 0) {
+    lines.push("## External Calls");
+    for (const call of allExternalCalls) lines.push(`- \`${call}\``);
+    lines.push("");
+  }
+
+  if (contract.functions.length > 0) {
+    lines.push("## Functions");
+    lines.push("");
+
+    const callMap = new Map(contract.functions.map((f) => [fnLabel(f), f.internalCalls]));
+
+    for (const fn of contract.functions) {
+      const label = fnLabel(fn);
+      lines.push(`### ${label}`);
+
+      const modsStr = fn.modifiers.length > 0 ? ` · modifiers: [${fn.modifiers.join(", ")}]` : "";
+      lines.push(`- visibility: ${fn.visibility} · mutability: ${fn.mutability}${modsStr}`);
+
+      const paramsStr = fn.params.length > 0 ? fn.params.join(", ") : "—";
+      const returnsStr = fn.returns.length > 0 ? `\`${fn.returns.join(", ")}\`` : "—";
+      lines.push(`- parameters: \`(${paramsStr})\` · returns: ${returnsStr}`);
+
+      if (fn.externalCalls.length > 0) {
+        lines.push(`- calls: [${fn.externalCalls.map((c) => `\`${c}\``).join(", ")}]`);
+      }
+      if (fn.internalCalls.length > 0) {
+        lines.push(`- graph: \`${fn.internalCalls.map((c) => `${label} → ${c}`).join(", ")}\``);
+      }
+
+      lines.push(`- recurse: ${hasCycle(label, label, callMap, new Set()) ? "yes ⚠" : "no"}`);
+
+      if (fn.stateReads.length > 0 || fn.stateWrites.length > 0) {
+        const reads = fn.stateReads.length > 0 ? fn.stateReads.map((r) => `\`${r}\``).join(", ") : "—";
+        const writes = fn.stateWrites.length > 0 ? fn.stateWrites.map((w) => `\`${w}\``).join(", ") : "—";
+        lines.push(`- state: reads [${reads}] · writes [${writes}]`);
+      }
+
+      lines.push(`- docs: ${renderNatSpec(fn.natspec)}`);
+      lines.push("");
+    }
+  }
+};
+
+const renderContractBrief = (contract: ContractAnalysis, imports: string[], lines: string[]) => {
+  lines.push("## Meta");
+  const inherits = contract.baseContracts.length > 0 ? `[${contract.baseContracts.join(", ")}]` : "—";
+  const importsList = imports.length > 0 ? imports.map((i) => `\`${i}\``).join(", ") : "—";
+  lines.push(`- kind: ${contract.kind} · inherits: ${inherits}`);
+  lines.push(`- imports: ${importsList}`);
+  lines.push(`- docs: ${renderNatSpec(contract.natspec)}`);
+  lines.push("");
+
+  const allExternalCalls = new Set(contract.functions.flatMap((f) => f.externalCalls));
+  if (allExternalCalls.size > 0) {
+    lines.push("## External Calls");
+    lines.push([...allExternalCalls].map((c) => `\`${c}\``).join(" · "));
+    lines.push("");
+  }
+
+  if (contract.functions.length > 0) {
+    lines.push("## Functions");
+    lines.push("| function | visibility | mutability | parameters | returns | modifiers |");
+    lines.push("|----------|------------|------------|------------|---------|-----------|");
+    for (const fn of contract.functions) {
+      const label = fnLabel(fn);
+      const params = fn.params.length > 0 ? fn.params.join(", ") : "—";
+      const returns = fn.returns.length > 0 ? fn.returns.join(", ") : "—";
+      const mods = fn.modifiers.length > 0 ? fn.modifiers.join(", ") : "—";
+      lines.push(`| \`${label}\` | ${fn.visibility} | ${fn.mutability} | ${params} | ${returns} | ${mods} |`);
+    }
+    lines.push("");
+  }
+};
+
+const fileHeader = (contracts: ContractAnalysis[], mode: "full" | "short", opts: RenderOptions): string[] => {
+  const names = contracts.map((c) => c.name).join(", ");
+  const label = mode === "full" ? "FULL" : "BRIEF";
+  const rankStr = opts.importance !== undefined ? ` | importance: ${opts.importance}/5` : "";
+  return [
+    `# ${names} · ${label}`,
+    `> path: \`${opts.filePath ?? "—"}\` | lines: ${opts.lineCount} | solc: ${opts.solcVersion}${rankStr}`,
+    "",
+  ];
+};
+
+export const generateFullMarkdown = (imports: string[], contracts: ContractAnalysis[], opts: RenderOptions): string => {
+  const lines: string[] = fileHeader(contracts, "full", opts);
+
+  for (let i = 0; i < contracts.length; i++) {
+    if (contracts.length > 1) {
+      if (i > 0) lines.push("---", "");
+      lines.push(`## ◆ ${contracts[i].name}`, "");
+    }
+    renderContractFull(contracts[i], imports, lines);
+  }
+
+  return lines.join("\n");
+};
+
+export const generateBriefMarkdown = (
+  imports: string[],
+  contracts: ContractAnalysis[],
+  opts: RenderOptions,
+): string => {
+  const lines: string[] = fileHeader(contracts, "short", opts);
+
+  for (let i = 0; i < contracts.length; i++) {
+    if (contracts.length > 1) {
+      if (i > 0) lines.push("---", "");
+      lines.push(`## ◆ ${contracts[i].name}`, "");
+    }
+    renderContractBrief(contracts[i], imports, lines);
+  }
+
+  return lines.join("\n");
+};

src/agents/auditor/utils.ts

@@ -1,3 +1,38 @@
+import fs from "node:fs";
+import path from "node:path";
+
+import { DOC_BASENAMES, DOC_EXTS, MAX_DEPTH, SKIP_DIRS, SOL_EXT, SOL_TEST_SUFFIXES } from "./config.ts";
+
+export const walkDirectory = (dir: string, depth: number, solFiles: string[], docFiles: string[]) => {
+  if (depth > MAX_DEPTH) return;
+
+  let entries: fs.Dirent[];
+  try {
+    entries = fs.readdirSync(dir, { withFileTypes: true });
+  } catch {
+    return;
+  }
+
+  for (const entry of entries) {
+    if (entry.isDirectory()) {
+      if (!SKIP_DIRS.has(entry.name)) {
+        walkDirectory(path.join(dir, entry.name), depth + 1, solFiles, docFiles);
+      }
+    } else if (entry.isFile()) {
+      const fullPath = path.join(dir, entry.name);
+      const ext = path.extname(entry.name).toLowerCase();
+      const base = path.basename(entry.name, ext).toLowerCase();
+
+      if (ext === SOL_EXT) {
+        const isTest = SOL_TEST_SUFFIXES.some((suffix) => entry.name.endsWith(suffix));
+        if (!isTest) solFiles.push(fullPath);
+      } else if (DOC_EXTS.has(ext) || DOC_BASENAMES.has(base)) {
+        docFiles.push(fullPath);
+      }
+    }
+  }
+};
+
 export const matchLines = (fileContent: string, codeSnippet: string): string | null => {
   const fileLines = fileContent.split("\n");
   const snippetLines = codeSnippet.split("\n").map((line) => line.trim());
@@ -34,3 +69,49 @@ export const matchLines = (fileContent: string, codeSnippet: string): string | n
 
   return null;
 };
+
+type ReviewEntry = {
+  finding: {
+    title: string;
+    severity: string;
+    location: string;
+    description: string;
+    codeSnippet: string;
+  };
+  review: {
+    isFalsePositive: boolean;
+    confidence: number;
+    review: string;
+    exploitablePaths: string[];
+  };
+};
+
+export const buildReviewBlocks = (fileEntries: ReviewEntry[], iterationCount: number): string => {
+  const blocks = fileEntries.map(({ finding, review }, i) => {
+    const verdict = review.isFalsePositive
+      ? `FALSO POSITIVO (confiança: ${review.confidence}/100)`
+      : `VERDADEIRO POSITIVO (confiança: ${review.confidence}/100)`;
+    const pathsLabel = review.isFalsePositive ? "Razão de Bloqueio" : "Caminhos de Exploração";
+    const pathsContent =
+      review.exploitablePaths.length > 0
+        ? review.exploitablePaths.map((p) => `  - ${p}`).join("\n")
+        : "  (nenhum fornecido)";
+
+    return `[Achado ${i + 1}/${fileEntries.length}] ${finding.title}
+Severidade: ${finding.severity}
+Localização: linhas ${finding.location}
+Descrição: ${finding.description}
+
+Código:
+\`\`\`solidity
+${finding.codeSnippet}
+\`\`\`
+
+Veredito do Revisor: ${verdict}
+Análise do Revisor: ${review.review}
+${pathsLabel}:
+${pathsContent}`;
+  });
+
+  return `=== Iteração ${iterationCount} — Achados e Revisões do Especialista (${fileEntries.length} achado(s)) ===\n\n${blocks.join("\n\n---\n\n")}`;
+};

src/config/llm.ts

@@ -5,30 +5,39 @@ import type { BaseChatModel } from "@langchain/core/language_models/chat_models"
 
 export type LLMProvider = "google" | "openrouter" | "anthropic";
 
-export function createLLM(overrideProvider?: LLMProvider): BaseChatModel {
+export interface LLMOptions {
+  model?: string;
+  temperature?: number | null;
+  maxTokens?: number;
+}
+
+export function createLLM(overrideProvider?: LLMProvider, options?: LLMOptions): BaseChatModel {
   const provider = overrideProvider || (process.env.LLM_PROVIDER as LLMProvider) || "openrouter";
 
   switch (provider) {
     case "openrouter":
       return new ChatOpenRouter({
-        model: process.env.OPENROUTER_MODEL || "google/gemini-3.1-flash-lite",
-        temperature: 0.2,
+        model: options?.model || process.env.OPENROUTER_MODEL || "google/gemini-3.1-flash-lite",
+        ...(options?.temperature !== null && { temperature: options?.temperature ?? 0.2 }),
         apiKey: process.env.OPENROUTER_API_KEY,
-        maxTokens: 4096,
+        maxTokens: options?.maxTokens ?? 4096,
       });
+
     case "anthropic":
       return new ChatAnthropic({
-        model: process.env.ANTHROPIC_MODEL || "claude-haiku-4-5",
-        temperature: 0.2,
-        maxTokens: 4096,
+        model: options?.model || process.env.ANTHROPIC_MODEL || "claude-sonnet-4-6",
+        ...(options?.temperature !== null && { temperature: options?.temperature ?? 0.2 }),
+        apiKey: process.env.ANTHROPIC_API_KEY,
+        maxTokens: options?.maxTokens ?? 4096,
       });
+
     case "google":
     default:
       return new ChatGoogleGenerativeAI({
         apiKey: process.env.GOOGLE_API_KEY || "",
-        model: process.env.MODEL_NAME || "gemini-2.5-flash",
-        temperature: 0.2,
-        maxOutputTokens: 4096,
+        model: options?.model || process.env.MODEL_NAME || "gemini-2.5-flash",
+        ...(options?.temperature !== null && { temperature: options?.temperature ?? 0.2 }),
+        maxOutputTokens: options?.maxTokens ?? 4096,
       });
   }
 }