VERIFAI

Inspiration

AI coding tools can propose changes, but a confident explanation is not proof that software works. VERIFAI separates model-generated hypotheses from observed runtime evidence.

What it does

VERIFAI is a bounded, evidence-first software verification lab. Its supported local workflow clones a small public GitHub repository, performs an AI-assisted source review using Strands and Amazon Bedrock, executes one policy-approved command in an isolated Docker container, captures output, exit status and timing, and cleans up run resources.

Findings use explicit confidence states: Confirmed, Unconfirmed, Unknown and Incomplete. Model hypotheses remain Unconfirmed without sufficient reproduction evidence. A completed check proves only the executed command outcome, not the entire application correctness or security.

How it is built

VERIFAI uses TypeScript and Node.js, a lightweight web interface, Strands Agents SDK, Amazon Bedrock and Docker. The selected command runs with bounded resources, no network access and a non-root container context. Source review and clone operations occur in the backend. Provider failures, missing prerequisites and incomplete execution remain visible rather than producing synthetic passes.

The repository also includes AgentCore worker contracts, AWS infrastructure definitions and deployment/smoke-test workflows. These are not evidence of a fully accepted live cloud deployment; real AWS acceptance is still pending according to the current README.

Engineering challenges

The design separates model opinions from executed evidence, restricts admissible commands, and makes cleanup part of the run lifecycle. Optional repair replay is command-scoped rather than proof of complete regression coverage. Pull-request creation remains human-controlled, with no automatic merge.

Current scope and next steps

The current MVP supports small public repositories and narrowly scoped checks. Broader verification coverage, independently validated regression checks and live cloud acceptance are future work. Alexa+ eligibility requires an implemented and demonstrated qualifying experience; the current repository does not establish that integration.