Mathematically proven code.
Free to start.

The full verification pipeline is open source under AGPL. Commercial licenses available for teams that need a clean IP boundary.

Open Source
$0/ forever

The full Nightjar verification pipeline, free for individuals, startups, and open source projects under AGPL.

Get started
  • ·Full 6-stage verification pipeline
  • ·Dafny formal proof (Stage 4)
  • ·Property-based testing (Stage 3)
  • ·Schema validation (Stage 2)
  • ·CEGIS repair loop
  • ·Immune system trace mining
  • ·MCP server (3 tools)
  • ·Textual TUI dashboard
  • ·All CLI commands
  • ·Community support (GitHub Issues)
  • ·AGPL-3.0 license
Most popular
Teams
$2,400/ per year

Built for engineering teams that ship AI-generated code to production. Adds SLA, private audit logs, and priority support.

Start free trial
  • ·Everything in Open Source
  • ·Commercial license (no AGPL copyleft)
  • ·Private audit log retention (90 days)
  • ·Team dashboard with proof certificates
  • ·GitHub Actions integration (official)
  • ·Slack / Discord alerts on verification failure
  • ·Priority support (8-hour response)
  • ·Unlimited modules and specs
  • ·Up to 20 seats
  • ·SSO via Google / GitHub
  • ·Monthly verification reports
Enterprise
$12,000/ per year

For organisations with compliance requirements, custom deployment needs, or large engineering teams.

Contact us
  • ·Everything in Teams
  • ·Unlimited seats
  • ·On-premise or VPC deployment
  • ·Custom Dafny rule libraries
  • ·SAML / SCIM provisioning
  • ·SOC 2 Type II report available
  • ·Audit log export (SIEM integration)
  • ·SLA: 4-hour critical response
  • ·Dedicated customer success manager
  • ·Custom integrations (Jira, ServiceNow)
  • ·Annual security review

Full Feature Comparison

FeatureOpen SourceTeamsEnterprise
Verification pipeline (all 6 stages)YESYESYES
Dafny formal proofYESYESYES
CEGIS repair loopYESYESYES
Commercial license—YESYES
Team dashboard—YESYES
Private audit logs—90 daysUnlimited
GitHub Actions (official)—YESYES
Priority support—8hr4hr
SSO (Google / GitHub)—YESYES
SAML / SCIM——YES
On-premise deployment——YES
SOC 2 Type II——YES
SeatsUnlimited*Up to 20Unlimited

* Unlimited seats for internal use. See AGPL FAQ below.

AGPL License FAQ

What does AGPL mean for my code?

AGPL-3.0 requires that if you distribute software that incorporates Nightjar — or run it as a network service — you must make your application's source code available under AGPL. If you use Nightjar only internally as a development tool (running it locally, in CI, on your own servers), AGPL does not require you to open-source your product code.

Do I need a commercial license?

You need a commercial license (Teams or Enterprise) if: (1) you want to distribute a product that includes or links Nightjar, (2) you offer Nightjar as a service to others, or (3) your organisation's legal policy prohibits AGPL dependencies. Most engineering teams using Nightjar internally as a verification tool do not need a commercial license.

Can I use the free version in a commercial project?

Yes. Using Nightjar as a development and verification tool in a commercial project is permitted under AGPL without needing a paid license, as long as you do not distribute Nightjar itself or use it to provide a service to third parties. When in doubt, consult your legal team or email us.

What happens if I contribute to Nightjar?

Contributions to the AGPL core are welcome. Contributors retain copyright and license their contributions under AGPL. The codebase uses a contributor license agreement (CLA) to allow us to offer the commercial license alongside the open-source one.

Need a custom quote or evaluation?

We offer 30-day enterprise evaluations with full support.

Contact enterprise →