Segurança &
Confiabilidade
O lean-ctx é projetado para uso em produção. Toda a compressão roda localmente, erros degradam graciosamente e seu código nunca sai da sua máquina.
Construído para Produção
Cada decisão arquitetural prioriza a segurança. O lean-ctx processa tudo localmente, degrada graciosamente em caso de erros e nunca modifica seus arquivos sem permissão explícita.
Processamento 100% Local
Toda compressão, cache e análise rodam na sua máquina. O lean-ctx é um servidor MCP local - seu código nunca toca servidores externos.
Degradação Graciosa
Se o lean-ctx encontrar um erro, ele passa o conteúdo original sem alterações. Seu workflow nunca é bloqueado por uma falha do lean-ctx.
Somente Leitura por Padrão
O lean-ctx só lê arquivos para compressão. A única operação de escrita é ctx_edit, que requer invocação explícita do usuário.
Defesa em Cada Camada
Da proteção contra path traversal à execução em sandbox, o lean-ctx implementa múltiplas barreiras de segurança para proteger sua base de código.
$ ctx_read("../../etc/passwd") ERROR: Path traversal blocked ├─ Requested: ../../etc/passwd ├─ Resolved: /etc/passwd └─ Allowed: /home/user/project/** $ ctx_read("src/main.rs") ✓ Reading src/main.rs (mode: auto) → 42 lines, 1.2 KB → compressed to 18 tokens
Proteção contra Path Traversal
Todos os caminhos de arquivos são validados por um ponto de controle de segurança. Requisições fora da raiz do projeto são rejeitadas.
Execução em Sandbox
Comandos shell rodam com timeouts configuráveis e limites de recursos. Sem eval() ou execução de código dinâmico.
Sem Rede sem Opt-In
O único recurso de rede é uma verificação de versão diária opcional (desativada por padrão). Sem telemetria, sem phone-home.
Testado & Verificado
Cada release é validada por uma suíte de testes abrangente, análise estática rigorosa e CI multiplataforma - sem atalhos.
Mais de 1.400 Testes Automatizados
Cada release passa por mais de 1.400 testes unitários e de integração cobrindo compressão, cache, proteções de segurança e casos extremos.
Clippy Pedantic
Zero avisos com o linter mais rigoroso do Rust. O modo pedantic detecta bugs sutis, problemas de performance e defeitos de design de API.
CI Abrangente
GitHub Actions roda testes no Linux, macOS e Windows. cargo-deny audita dependências quanto a vulnerabilidades e conformidade de licenças.
Nada quebra. O lean-ctx passa o conteúdo original sem alterações. Seu workflow nunca é bloqueado - a IA simplesmente recebe o contexto sem compressão.
Totalmente Open Source
Cada linha de código é publicamente auditável. Sem ofuscação, sem blobs binários, sem telemetria por padrão.
$ lean-ctx --version lean-ctx 3.4.3 ├─ License: Apache-2.0 ├─ Source: github.com/yvgude/lean-ctx ├─ Network calls: 0 (default) ├─ Telemetry: disabled └─ Data collection: none
Totalmente Open Source
Cada linha de código é publicamente auditável no GitHub. Sem ofuscação, sem blobs binários, sem componentes de código fechado.
Zero Telemetria por Padrão
O lean-ctx não coleta nada por padrão. Estatísticas anônimas opcionais requerem opt-in explícito e não contêm código ou nomes de arquivos.
Verificação de saída
Cada saída comprimida é automaticamente verificada para integridade.
ctx_read src/auth.rs ✓ VERIFY PASS ├─ Paths checked: 12/12 preserved ├─ Identifiers: 8/8 preserved ├─ Structure: balanced └─ Info loss score: 0.0%
Ancoragem de caminhos
Caminhos de arquivo são verificados para preservação na saída comprimida.
Verificação de identificadores
Nomes de funções e estruturas são rastreados através da compressão.
Integridade estrutural
O equilíbrio de chaves é verificado para detectar blocos truncados.
Matematicamente Comprovado
Invariantes de política, propriedades de compressão e segurança de transferência de agentes são formalmente verificados em Lean4 — o mesmo assistente de prova utilizado pelo Amazon Cedar e Mathlib. 82 teoremas verificados por máquina com zero lemas não provados.
$ lake build Build completed successfully. 82 theorems verified 0 sorry (unproven lemmas) 0 warnings $ ctx_proof --format v2 ContextProofV2 · 8 claims extracted ├─ PathJail: proved (Lean4) · Q4 ├─ Budget: proved (Lean4) · Q4 ├─ Scope: proved (Lean4) · Q4 ├─ TerseQuality: proved (Lean4) · Q4 ├─ TerseEngine: proved (Lean4) · Q4 ├─ Compression: preserved · Q3 ├─ Secrets: passed · Q2 └─ Quality Level: 4 (Formally Verified)
Invariantes de política
Prevenção de escape PathJail, isolamento de escopo, aplicação de orçamento e regras de governança de contexto — todos comprovados como corretos em Lean4.
Preservação de compressão
O modo Signatures preserva todos os exports, o modo Map preserva imports, o modo Aggressive garante zero vazamento de segredos — matematicamente comprovado.
Segurança de transferência
A máquina de estados de transferência de agentes é formalmente verificada: estados terminais são sumidouros, a ordenação do ciclo de vida é monótona, envelopes inválidos são rejeitados.
Pronto para Experimentar?
Instale o lean-ctx em menos de um minuto e veja como ele protege seu workflow enquanto reduz drasticamente o uso de tokens.