# Analyzing Teleport RBAC with Z3: Regexes, queries and formal methods

DevFeed: [Analyzing Teleport RBAC with Z3: Regexes, queries and formal methods](<https://devfeed.tech/articles/analyzing-teleport-rbac-with-z3-regexes-queries-and-formal-methods-29983.md>)

Original publisher: [Read original article](<https://goteleport.com/blog/z3-rbac/>)

Author: info@goteleport.com (Andrew Helwer)

Published: 2022-01-19T00:00:00Z

Content type: tutorial

Language: en

Sources: [Teleport](<https://devfeed.tech/sources/teleport.md>)

Topics: [Formal methods](<https://devfeed.tech/topics/formal-methods.md>), [Access Control](<https://devfeed.tech/topics/access-control.md>), [Python](<https://devfeed.tech/topics/python.md>), [Software](<https://devfeed.tech/topics/software.md>), [Open Source](<https://devfeed.tech/topics/open-source.md>), [Software Engineering](<https://devfeed.tech/topics/software-engineering.md>)

Tags: [access-control](<https://devfeed.tech/tags/access-control.md>), [formal-methods](<https://devfeed.tech/tags/formal-methods.md>), [library](<https://devfeed.tech/tags/library.md>), [open-source](<https://devfeed.tech/tags/open-source.md>), [python](<https://devfeed.tech/tags/python.md>), [regex](<https://devfeed.tech/tags/regex.md>), [regular-expressions](<https://devfeed.tech/tags/regular-expressions.md>), [security](<https://devfeed.tech/tags/security.md>), [syntax](<https://devfeed.tech/tags/syntax.md>)

## AI overview

This tutorial explains how to use the Z3 theorem prover to analyze Teleport's role-based access control system. It covers checking whether roles admit the same users to the same nodes and handling constraints involving string equality, regular expressions, interpolation, and basic string functions.

## Source excerpt

Learn how to use Z3 to ask questions about our RBAC system. Are two roles the same?