feat: Implement two-sided verification check with check modes#487

Merged

MikaelMayer merged 203 commits intomainfrom

feat/two-sided-verification-check

Mar 12, 2026

Commits on Feb 26, 2026

feat(verifier): Implement two-sided verification check
MikaelMayer
committed
feat(cli): Add --check-mode flag and update emoji symbols
MikaelMayer
committed
feat(verifier): Add per-statement check mode annotations
MikaelMayer
committed
test: Add comprehensive VCOutcome tests and fix SMTEncoder tests
MikaelMayer
committed
test: Add comprehensive VCOutcome tests and fix SMTEncoder tests
MikaelMayer
committed
test: Add comprehensive VCOutcome tests and fix SMTEncoder tests
MikaelMayer
committed
docs: Update implementation summary with completed features
MikaelMayer
committed
fix: Update StrataVerify and StrataMain for VCOutcome API changes
MikaelMayer
committed
fix: Remove trailing whitespace in SMTUtils.lean
MikaelMayer
committed
fix: Remove all trailing whitespace in SMTUtils.lean
MikaelMayer
committed
fix: Map old reachCheck metadata to fullCheck for backward compatibility
MikaelMayer
committed
feat: Add isAlwaysFalseIfReachable alias for isRefuted
MikaelMayer
committed
refactor: Rename predicates for consistency and add cross-cutting filters
MikaelMayer
committed
chore: Remove implementation tracking document
MikaelMayer
committed
refactor: Make isPass conservative (validity only) and add specific variants
MikaelMayer
committed
refactor: Consistent naming with reachability at end, isSatisfiable covers all sat cases
MikaelMayer
committed
refactor: Separate base cases (no 'is' prefix) from derived predicates
MikaelMayer
committed
feat: Add VerificationMode to outcomeToLevel for context-aware severity
MikaelMayer
committed
refactor: Simplify outcomeToLevel - no warnings in deductive mode, use isAlwaysFalse
MikaelMayer
committed
refactor: Rename refutedAndReachable to alwaysFalseAndReachable, unreachable is warning in deductive
MikaelMayer
committed
refactor: Use only base case predicates in outcomeToLevel
MikaelMayer
committed
refactor: Make outcome messages neutral and context-independent
MikaelMayer
committed
fix: Handle models correctly for alwaysFalseReachabilityUnknown and unknown outcomes
MikaelMayer
committed
fix: Remove incorrect model handling for alwaysFalseReachabilityUnknown
MikaelMayer
committed
refactor: Pattern match directly on satisfiability and validity properties
MikaelMayer
committed
fix: Remove trailing whitespace in SarifOutput.lean
MikaelMayer
committed
test: Add comprehensive SARIF output tests for all nine outcomes
MikaelMayer
committed
fix: Update dischargeObligation call signature in test
MikaelMayer
committed
refactor: Consolidate VCOutcome tests to one eval per case
MikaelMayer
committed
feat: Add --error-level CLI option for SARIF severity mapping
MikaelMayer
committed
fix: Update StrataMain for VCOutcome changes and clarify bugFinding comment
MikaelMayer
committed
fix: Update bugFinding SARIF severity levels per review
MikaelMayer
committed
fix: Remove trailing whitespace from Verifier.lean
MikaelMayer
committed
refactor: Add helper function and improve SARIF output labels in tests
MikaelMayer
committed
refactor: Improve VCOutcome tests with comprehensive predicate checking
MikaelMayer
committed
feat: Add derived predicate testing to VCOutcome tests
MikaelMayer
committed
refactor: Remove unnecessary section comments from VCOutcome tests
MikaelMayer
committed
refactor: Redesign verification flags for orthogonal error mode and diagnostic level
MikaelMayer
committed
refactor: Rename flags to --check-mode and --check-amount, simplify annotations
MikaelMayer
committed
Merge remote-tracking branch 'origin/main' into feat/two-sided-verification-check
MikaelMayer
committed
fix: use assert + check-sat for single checks to match pre-PR behavior
MikaelMayer
committed

Commits on Feb 27, 2026

Commits on Mar 2, 2026

Commits on Mar 3, 2026

Commits on Mar 4, 2026

Commits on Mar 5, 2026

Commits on Mar 6, 2026

Commits on Mar 9, 2026

Commits on Mar 10, 2026

Commits on Mar 12, 2026