Paste a public GitHub repository. A server worker pins one full commit, streams its archive and screens all eligible supported text within hosted caps: 2,000 files, 1 MiB per file and 20 MiB total. No repository code, builds, scripts or installs are run. Results are review candidates, not confirmed vulnerabilities.
Hosted service time is limited to 20 seconds plus a bounded 3-second fenced save. Slower repositories can stop with a terminal runtime-budget failure and no report; that failure is not automatically retried.
Recorded preview validation · pinned Signal eligible-text assessment
Signal at b2a5c30f3245c1bcad04b27b1e752a38321c793d: 1,569 of 1,569 eligible files analyzed, 14,637,105 bytes; 220 exclusions listed. Passive review only, not verification. These downloads remain historical preview Node captures, not published-runtime validation. Separate corrected production acceptance is recorded in hosted-validation/runtime-budget-2026-10-23. New runs are queued and executed by the active server dispatcher.
Bounded public-source review. Repository code is not executed.
Review scope
64 KiB/file · 512 KiB source total · 2 concurrent · 12,000 tree entries. Unauthenticated public GitHub REST only; no credentials requested. The public quota is normally 60 requests/hour/IP. Selection prioritizes policy, CI, manifests, then crypto/agent paths. Oversized and sensitive filenames are excluded. This browser inspection does not use hosted workers or create recurring reviews.
No repository assessment yet
No seeded findings, vulnerability counts or proof claims. Choose public source or import a forge-assurance/1 report. Source stays transient and is omitted from exports; imported tool results are not independently checked.
What should this software guarantee?
Choose a behavior that matters. You write and freeze the requirement; checkers that are not connected stay marked as not run.
New here? See a complete failing → repaired → checked trail on a small bundled C function.
The worked example is separate from any connected repository; its result never applies to it.
Recorded repository verification · not passive scanning
Kani checks of two Signal functions
Fresh Kani 0.68.0 (CBMC 6.11.0) proofs ran in the build sandbox on code mechanically extracted from signalapp/libsignal at b2a5c30f3245c1bcad04b27b1e752a38321c793d. Each proof is paired with a mutant that must fail an assertion. These are recorded build-sandbox Kani results, not live runs; the web app has no hosted Kani checker. These fixed-source contracts are independent of the selected repository. Kani has not run on other repositories here; hosted passive assessments are separate. A narrow property of two small items is not a proof of Signal or phone-number conformance.
DeviceId range contract
Checking pinned capture…
Source
rust/core/src/address.rs @ b2a5c30f3245
Property
For every symbolic u32, i32 and u8, DeviceId construction succeeds iff the value is in 1..=127, and the stored value is preserved through each conversion.
Scope
Contiguous DeviceId items (lines 673–751) extracted mechanically; Display, ProtocolAddress and the rest of the crate are not checked.
Recorded correction v2: the frozen bridge failed to compile under Kani's edition-2015 standalone mode (TryInto not in prelude). Only `use std::convert::TryInto;` was added; harness, assertions, extraction and mutation are unchanged. Original v1 inputs and compile-failure JSON are preserved as historical/incomplete; the original raw failure log is unavailable. This fresh run uses unchanged v2.
For every u64, nonzero values encode to the network-byte-order 8 bytes and decode back; for every [u8; 8], decoding succeeds iff the big-endian value is nonzero and re-encodes to the same bytes.
Scope
Representation only — not phone-number conformance, parsing rules, or any other Signal behavior. cfg(test) module and a derive_more::Into marker removed.
Mutation control
to_be_bytes → to_le_bytes in E164::to_be_bytes. Mutant mis-orders bytes for value 0x8000000000000000 (concrete playback).
Historical captures are incomplete: original raw logs are unavailable. Fresh evidence supersedes that packaging gap; it does not reconstruct the old logs.
Trust: an operator-selected local checker; captures are hash-pinned for integrity, not an authenticated tool attestation. Source identity is a local hash match to the pinned file, not an upstream signature. The official Kani bundle needed a launcher adding two system libraries (zlib, libstdc++) in this sandbox; see the toolchain record.
Version string explainer
Ask Lovable AI whether a version string is one immutable release or a selector. The AI answer is advisory; the OSV lookup only uses the built-in rule shown alongside.