Como verificamos os resultados do Stabileo, e quais são os limites

Um programa de cálculo estrutural pode dar um número errado sem nenhum sinal visível. Nas últimas semanas testamos cada parte do Stabileo de várias maneiras independentes, encontramos dezenas de defeitos reais, muitos contra a segurança, e corrigimos a maioria. Cada um é avaliado e, se pode ter afetado resultados já usados, é publicado como aviso, com o que fazer enquanto isso; alguns ainda estão em avaliação. Este texto conta como procuramos esses defeitos, o que provam os certificados que acompanham os resultados e, com a mesma clareza, o que fica fora de qualquer verificação.

Um só motor de cálculo

O solver é escrito em Rust e compilado para WebAssembly: roda no computador de quem o usa, sem instalação e sem enviar o modelo a nenhum servidor. É o mesmo código testado na integração contínua. Em outubro de 2026 removemos os cálculos paralelos em TypeScript que substituíam o motor em silêncio quando ele não estava disponível: agora a aplicação avisa, em vez de calcular com uma cópia não verificada.

Cinco maneiras de procurar erros

Nenhum teste encontra todos os erros, então usamos vários que falham de maneiras diferentes:

• Comparação com outros programas. Os mesmos modelos, fixos e gerados ao acaso toda noite, são resolvidos com OpenSees, Code_Aster, Frame3DD, PyNite, MYSTRAN, Kratos e CalculiX. Cada diferença é investigada até saber se o erro é nosso ou se os dois programas modelam o caso de forma diferente.
• Referências publicadas. Um conjunto de casos de aceitação com resultados publicados pelos autores, não por outro programa comercial, com tolerâncias definidas pela precisão impressa na fonte. As verificações de projeto são comparadas com exemplos resolvidos publicados (INTI-CIRSOC, AISC e outros).
• Invariantes físicos. Girar, espelhar ou renumerar um modelo, ou trocar suas unidades, tem que mudar a resposta exatamente como diz a física; a superposição, a reciprocidade e o balanço de energia têm que valer. Esses testes não precisam de nenhum valor de referência.
• Derivações. As matrizes das barras são derivadas simbolicamente a partir dos princípios e comparadas termo a termo com as do código; para os demais elementos há derivações escritas para que outro engenheiro possa revisá-las.
• Fuzzing e testes de mutação. Milhões de entradas geradas automaticamente procuram falhas e resultados não finitos, e erros são introduzidos de propósito no código para conferir que os testes os detectam.

Certificados: um resultado com limite de erro

Para os resultados que o admitem, o Stabileo tenta também, em segundo plano, um certificado: um limite, calculado com aritmética de intervalos, que contém a solução exata do sistema que resolveu. Se não consegue, o resultado fica marcado como não certificado, com o motivo. O limite é do erro numérico, não do erro de discretização da malha ou do passo de tempo. Para a análise linear, as combinações, a modal e o colapso plástico, a matemática central desse limite está demonstrada em Lean, um assistente de provas em que o computador confere cada passo; alguns passos (as restrições, uma condição da modal) ainda não estão formalizados. O P-Delta, a espectral, a harmônica e a dinâmica também têm certificados, mas sua matemática ainda não está formalizada em Lean. A integração contínua rejeita qualquer prova incompleta ou axioma acrescentado, e para alguns tipos de certificado o verificador que roda é o próprio código Lean sobre o qual estão as provas.

O que os certificados não dizem

• Um certificado limita o erro de resolver o sistema tal como foi montado. Não prova que esse sistema represente o modelo: a montagem da matriz de rigidez e das cargas é testada das formas acima, mas não certificada. Quando faltava a flambagem torcional (SA-2026-007), o certificado certificava o problema errado. Desde a 0.3.0, os certificados de ponta a ponta remontam o sistema de forma independente para pórticos e treliças e verificam o resultado contra o próprio modelo; cascas, sólidos e conectores ainda não estão cobertos.
• Lean demonstra a matemática; que o código Rust implemente exatamente esse algoritmo não está demonstrado, exceto nos verificadores que são código Lean.
• As verificações certificadas das normas avaliam suas fórmulas com aritmética de intervalos, mas as fórmulas em si não estão formalizadas: são comparadas com exemplos resolvidos publicados onde existem, e a cobertura de cada norma (quais cláusulas, quais exemplos) está na matriz de maturidade. Alvenaria, ligações, fundações e serviço não são certificadas.
• Nenhuma verificação do programa verifica o modelo. As cargas, os apoios e a idealização são decisões do engenheiro; a revisão do modelo avisa de erros comuns, mas não substitui o critério.
• Ainda não houve uma revisão independente por um engenheiro estrutural habilitado. Os resultados de CIRSOC 301 continuam marcados como experimentais.

A IA redige e revisa; não calcula

O assistente de IA monta rascunhos de modelos a partir de uma descrição e revisa modelos existentes, mas não calcula resultados: os números vêm do solver e dos módulos de verificação da aplicação. Suas explicações são texto de um modelo de linguagem e podem errar; os valores que valem são os dos resultados. Antes de aplicar uma mudança, ele mostra o que vai modificar, e ela pode ser desfeita num passo. As funções de IA enviam a descrição e o modelo a um servidor que consulta um modelo de linguagem; o solver, os resultados e as verificações não precisam dele e funcionam sem conexão.

Quando algo falha

Os defeitos que podem ter afetado resultados já usados são publicados como avisos de segurança, com como reconhecer um modelo afetado e o que fazer enquanto isso; outros defeitos de segurança estão em avaliação e são acrescentados quando cabe. Os avisos abertos são fechados quando a correção está publicada em stabileo.com.