Semkon: semantika kontrolilo (semantic checker)
Semkon uses LLMs to check the correctness of proofs written as comments in your codebase.
Features:
- automatically finds property+proof blocks in your code
- see example
- recognizes stated "axioms"
- configurable file exclusion
- can execute Python code (off by default)
Requires OpenAI API key. Costs can be unpredictable so to be fully safe, use a project API key with a project budget limit.
Run: semkon --help
Install for development: pip install -e ".[dev]"
Alternatives:
- AI code review tools may be able to check some proofs
- CodeRabbit was able to check some simple proofs with no customizations
- you may be able to explicitly add proof checking as a custom "style rule" if necessary