5-minute guide

Quickstart

Install Nightjar, write your first spec, and get a formal proof of correctness in under 5 minutes.

Verification Pipeline

0 Preflight→1 Deps→2 Schema→2.5 Negation→3 PBT→4 Formal

Install Nightjar

Nightjar requires Python 3.11+ and Dafny 4.x for formal verification. Install the package with pip, then verify the CLI is available.

bash

pip install nightjar-verify

# Verify the install
nightjar --version

Note: Dafny 4.x is required for Stage 4 (formal proof). If you just want schema + PBT verification, you can skip it — use --fast to skip Dafny.

Write a spec (.card.md)

Specs live in .card/ at the root of your project. Each .card.md file defines the invariants your code must satisfy. Nightjar generates and verifies code to match the spec — never the other way around.

bash

nightjar init payment

# This creates .card/payment.card.md
# Open it and fill in your contracts:

02b

Your first spec

A spec defines preconditions, postconditions, and invariants. Nightjar's pipeline reads these to generate and verify code.

markdown

# .card/payment.card.md

## Module: payment

### Function: process_payment

**Preconditions:**
- amount > 0
- currency in ["USD", "EUR", "GBP"]
- card_token is a non-empty string

**Postconditions:**
- Returns a PaymentResult with status "success" or "declined"
- If status == "success", transaction_id is a non-empty string
- If status == "declined", transaction_id is None

**Invariants:**
- total_charged >= 0
- No amount is charged on declined transactions

Generate verified code

Nightjar's generator runs three agents in sequence: Analyst (reads spec), Formalizer (converts to Dafny contracts), Coder (produces Python). The pipeline then verifies the output through 6 stages before accepting it.

bash

# Set your LLM model
export NIGHTJAR_MODEL=claude-sonnet-4-6

# Generate code from your spec
nightjar generate

# Output:
# ✓ Analyst extracted 3 preconditions, 2 postconditions
# ✓ Formalizer produced Dafny contracts
# ✓ Coder generated payment.py
# ✓ Stage 0 (Preflight): PASS
# ✓ Stage 1 (Deps): PASS
# ✓ Stage 2 (Schema): PASS
# ✓ Stage 3 (PBT): PASS — 1000 cases
# ✓ Stage 4 (Formal): PASS — proof complete

Verify your existing code

Already have code? Point Nightjar at it with a spec. The verify command runs the full 6-stage pipeline against your existing implementation.

bash

# Verify all modules (full pipeline)
nightjar verify

# Fast check — skip Dafny (schema + PBT only)
nightjar verify --fast

# Verify a specific module
nightjar verify --module payment

# Launch the TUI dashboard
nightjar verify --tui

Scan a GitHub repo

Nightjar can scan any public Python repository directly. Paste a GitHub URL into the scanner on the homepage to get a full verification report.

bash

# Or use the CLI directly:
nightjar scan https://github.com/your-org/your-repo

# The scanner:
# 1. Clones the repo
# 2. Extracts function signatures and docstrings
# 3. Generates specs automatically
# 4. Runs the full verification pipeline
# 5. Returns a structured report

Note: Public repos only for the hosted scanner. For private repos, run Nightjar locally.

Next Steps

Browse bug reports

74 confirmed bugs found by Nightjar

Compare tools

Nightjar vs. Semgrep, Snyk, CrossHair

Pricing

Open source, Teams, Enterprise