Extending Sector9

Understand the test harness, translation pipeline, and trusted base. Start here when changing Sector9 itself.

Adding New Tests

This guide walks through creating verification tests for Sector9, from writing the test file to integrating with the test suite.

This guide explains how Sector9 transforms Sector9 source code into verified programs, walking through each stage of the verification pipeline.

When extending Sector9, understanding what the verifier trusts without proof is essential for maintaining soundness.