specula-org/Specula
Specula: An agentic tool for finding deep bugs in system code using TLA+
해결하는 문제
Specula는 기존 테스트로는 감지하기 어려운 동시성 및 분산 시스템 코드의 심층적이고 복잡한 버그를 찾아냅니다. 고수준 시스템 사양과 실제 코드 구현 사이의 간극을 메워 형식 검증 프로세스를 자동화합니다.
작동 원리
Specula는 AI 코딩 에이전트를 사용하여 대상 시스템의 소스 코드를 분석하고 자동으로 TLA+ 사양을 작성합니다. 이러한 사양에는 시스템 구현의 형식 모델과 해당 시스템의 '정확성'을 정의하는 불변 조건이 포함됩니다. 이후 도구는 이러한 사양을 모델 체킹하여 잠재적인 위반 사항을 찾아냅니다. 위반 사항이 발견되면 Specula는 실제 코드 수준에서 해당 위반을 재현하여 버그를 확정합니다.
대상 사용자
높은 수준의 정확성을 보장하고 심층적인 아키텍처 또는 로직 버그를 찾아내야 하는 동시성 또는 분산 시스템 개발자 및 연구원.
주요 특징
- 자동화된 형식 사양: LLM 기반 코딩 에이전트를 사용하여 소스 코드에서 TLA+ 모델을 생성합니다.
- 코드 수준 재현: 모델 내의 이론적 위반을 찾는 것뿐만 아니라 실제 구현에서 이를 재현합니다.
- CI 통합: 지속적인 검증을 지원하여 소스 변경 사항을 점진적으로 확인합니다.
- 에이전트 독립성: 스킬 시스템과 MCP 도구를 통해 Claude Code, Codex, Copilot CLI를 포함한 다양한 코딩 에이전트와 호환됩니다.
관련
- 프로젝트
- 프로젝트
reticlehq/reticleAI 코딩 에이전트를 위한 검증 도구로, 실제 실행 중인 애플리케이션을 구동하여 기능이 실제로 작동하는지 확인하고 내부 앱 상태 및 네트워크 트래픽을 기반으로 판정을 제공합니다.
- 프로젝트
github/spec-kitSpec Kit은 AI 코딩 에이전트가 기능 개발, 버그 수정 및 프로젝트 평가를 처리할 수 있도록 구조화되고 반복 가능한 프로세스를 제공하는 오픈 소스 툴킷입니다.
- 프로젝트
tanweai/puapua는 기업 스타일의 '성과 향상 계획'(PUA/PIP) 표현과 7단계 디버깅 체크리스트를 AI 코딩 어시스턴트(Claude Code, OpenAI Codex, Cursor, Kiro 등)에 주입하는 다중 플랫폼 스킬입니다. 모델이 게으른 패턴(재시도, 사용자 비난, 수동 대기)을 보이거나 `/pua` 명령어로 수동으로 호출되면 자동으로 작동합니다. 이 스킬은 모델이 해결책을 끝까지 고려하고 결과를 검증하며 능동적으로 행동하도록 강제하며, 중국어, 영어, 일본어의 언어별 팩을 제공합니다. 소수의 버그에 대한 벤치마크 결과는 수정 수와 검증 단계 수가 증가했지만, 속도 향상은 제한적입니다. 설치는 각 도구의 플러그인/스킬 시스템을 통해 수행됩니다(예: `npx skills add tanweai/pua --skill pua-en`으로 Claude Code에 설치)
- 프로젝트
NanmiCoder/cc-hahacc‑haha는 크로스 플랫폼 데스크톱 워크벤치(Electron + React)로, Claude, ChatGPT, Grok 및 기타 여러 LLM과 채팅하고, 여러 코딩 세션을 관리하고, diff를 검토하고, 웹 페이지를 미리보고, 이미지를 생성하고, 멀티 에이전트 워크플로를 실행하고, 에이전트가 다른 데스크톱 앱을 제어하도록(Computer Use) 할 수 있습니다 – 모두 단일 앱에서 가능합니다.